SVA challenges in creating, debugging and verifying assertions

During our SVA class today there were frequent questions/comments on:

 

• How to write assertions easily without becoming a language guru?
• How to ensure that the assertions we write are correct to start with? (Not syntax wise, rather functionally)
• How to visualize assertions/attempts/threads easily?
• Can we create assertions automatically from a timing diagram/dump file?
• How to debug assertions? What sort of automation is available?
• Given a dump file, can we explore a set of assertions about that design (without having to rerun the simulations)?
• Can we verify assertions in isolation – i.e. even before RTL and/or TB is ready?

Sure a boatload of questions, some answers are available some are not as of today. CVC will address some of these in a seminar in one of the coming weeks. (Stay tuned to this site for that news).

Here are some answers:

Q: How to write assertions easily without becoming a language guru?

• Leverage on assertion libraries such as OVL, VMM SVA lib, QVL, IAL etc.

Q: How to ensure that the assertions we write are correct to start with? (Not syntax wise, rather functionally)

• Not an easy thing, but again use pre-verified assertion lib elements (see prev Q)

Q: How to visualize assertions/attempts/threads easily?

• Know your tools: Springsoft (formerly Novas) has a great product called Verdi that can present a “Temporal Flow View” and thread view. It is so amazing and intuitive that you will stay locked with it for long long time to come, really speaking. The idea of temporal annotation is not new, we spoke about it in our PSL book, see below a snapshot:

 

 

The core idea is to annotate the values of signals at “appropriate time” and not just based on current time (the latter is what most of debuggers do, except for Verdi AFAIK).

 

Consider a code like:

 

mul_attempts : assert property (@posedge clk) start |=> s1;

sequence s1;

a ##1 b ##2 c;

endsequence

 

Below is a screenshot of how Verdi can display it.

 

 

2 key/novel ideas here to appreciate:

 

1. The threads are nicely displayed with “horizontal lines” – this is exactly how our PPT in training explains threads BTW!

2. The Temporal annotation of the sequence/property with values & time stamps. For the failure at 350 ns (assume 20 ns clock period), it shows value of: (a ##1 b ##2 c;)

• “c” @350ns
• “b” @310 ns
• “a” @290
• “start” @270ns

This is simply superb, hats off to Verdi!

Q: How to debug assertions? What sort of automation is available?

• Refer to prev Q, almost every vendor provides some automation.

Q: Can we create assertions automatically from a timing diagram/dump file?

• Yes, there have been few attempts at this. OneSpin claims this feature and also a new start-up http://solidoaktech.com/TD2Assert.html We will investigate more and update here soon.

 

Q: Given a dump file, can we explore a set of assertions about that design (without having to rerun the simulations)?

• VCS can do this
• Springsoft/Verdi can do this
• Veritools can do this too!

Q: Can we verify assertions in isolation – i.e. even before RTL and/or TB is ready?

• Strictly speaking this is ideal job for formal verification tools. We believe some tools such as Magellan (Synopsys) already do this. We will update more here, stay tuned (for the 3rd time in this post…)