DAC 2010: What's interesting?

vhdlcohen

As many of us will be going to DAC, I would like to hear your comments about what is/was interesting. I'll start by mentioning a few tool that I find useful and interesting. Srini wrote about this topic in http://www.cvcblr.com/blog/?p=170 I believe that this year we'll see many enhancements in the field of formal verification. In this post I do not intend to do a comprehensive review of products, as I am sure that I am missing many interesting tool sets. My goal is rather to start a discussion in this community about your thoughts and experiences.
1) Jasper Design Automation, ActiveDesign with Behavioral Indexing™
http://jasper-da.com/products/ActiveDesign.htm
I saw a demo at DvCon and at http://www.demosondemand.com/dod/proddemos/vendors/pd_jasper.aspx#JASP003
What's interesting about this tool is that it uses a GUI tied to a formal verification engine and a data base (DB) that is filled by the analysis and user. The formal verification engine is used to witness functional coverage sequences. Initially, you can load your RTL, and start picking signals of interest (e,g., an output or internal signal), and the tool will witness the cover sequence(variable). The Gui automatically creates functional coverage assertions, and uses a sophisticated DB, and the formal tools to do the witnessing. Through the GUI you can add more constraints to create things like cover sequence(var1 ##3 var2).
Behavioral Indexing, which is part of the tool, (see Srini's take on this http://www.cvcblr.com/blog/?p=144 ) allows you to annotate the data base (DB) with diagrams, comments, questions, resolutions, etc, and as the design evolves, one can query the DB that links everything together, including of course the RTL. Since ActiveDesign is linked to Jasper Gold for formal verification, any assertions written in SVA are taken into account in your evaluation and understanding of your design. The witnessing of assertions, and functional coverage (easily added with the GUI) shows waveforms that can be linked to the code. Anyway, this looks like a friendly user tool that is very beneficial in the design process and life cycle of the design, include iterations that may occur further down the line (years later?), even with different engineers; this is because the behavioral indexing (the DB and its querry) can bring back information about the design, including code, rationals for certain decitions, documents, diagrams, timing data, etc. I like this tool because it's a living tools that can be used during the whole design and verification process. I wish I had such a thing when i was doing design. I also wished I had access to a laptop and the Internet when I went to college (instead of a stupid typewriter), and I wished I bought the Apple stock at $100 ... but that is a different story.

2) BugScopeTM Assertion Synthesis This topic was was addressed in Assertion Synthesis // Is it worth it? It is different than Jasper's ActiveDesign with Behavioral Indexing™ as it requires a simulation to extract properties of your design as tested by your simulation, and can find holes in your design. It's a different animal than Jasper's toolset.

3) OneSpin 360® MV Product Family
OneSpin is a very aggressive company. http://www.onespin-solutions.com/ OneSpin was used in our SystemVerilog Assertions Handbook, 2nd Edition book in the chapter on formal verification. From their site 360 MV has powerful support for standard formal ABV applications – such as automatic RTL checks, implementation intent verification, and verification of end-to-end functional requirements – and extends them with a unique Operational ABV methodology. Operational ABV simplifies verification planning, eases assertion writing working from timing diagrams and is the key for an exhaustive coverage analysis ensuring no design behavior is missed during verification. Also from http://www.onespin-solutions.com/news_x-verification.php 360 MV automatically identifies all design signals that can become X, and enables designers to use X-aware constructs – such as "$isunknown" and "===" – to write simple assertions to fully explore the propagation of X's ... designers can now easily determine whether given registers can safely be left uninitialized – to reduce chip area – without breaking their design. 360 MV ensures the X-robustness of designs before synthesis, saving effort in late gate-level simulation.
This exploration of Xs is an important thing that is being stressed by several vendors.

4) Real Intent http://www.realintent.com/
They have a set of interesting tools including the exploration of Xs; Real Intent offers automatic verification solutions using innovative formal techniques in an easy to use methodology, solving critical problems with comprehensive error detection and high ROI. I intend to stop by and further understand their product lines.
_________________
Ben Cohen http://www.systemverilog.us/
* SystemVerilog Assertions Handbook, 2nd Edition, 2010
* A Pragmatic Approach to VMM Adoption
* Using PSL/SUGAR ... 2nd Edition
* Real Chip Design and Verification
* Cmpt Design by Example
* VHDL books

vhdlcohen · Posted: Fri Jun 11, 2010 10:22 am **Post subject:**

Industry Gadfly -- My Cheesy Must See List for DAC 2010
http://www.deepchip.com/gadfly/gad061010.html

vhdlcohen · Posted: Wed Jun 30, 2010 2:25 pm **Post subject:**

Saw the RealIntent, http://www.realintent.com/real-intent-products/ascent Ascent product family. It has some interesting tools for early functional verification. An advanced LINT analysis tool is very useful since it also addresses VHDL, Verilog, and SystemVerilog. They claim it is low noise, which would be very useful, but I missed how they do that. The tool does syntax/semantic errors, synthesis/simulation mismatch, naming conventions etc. It also uses exhaustive formal sequential analysis to compute state and block reachability, single or pair-wise state deadlock, dead code, synthesis pragma violations, etc. To really appreciate the tool, I suggest that a user gets a trial license. It is interesting that their posters also showed a formal ABV tool for verification of SVA and PSL user assertions but they did not have a demo or presentation of it. They told me their emphasis is on easy to use, completely automated tools - they want you to be up and running fast.

The LINT tool is static checks only. Another tool, IIV (Implied Intent Verification) is the one that does sequential analysis from automatically generated checks. The two big checks are block reachability and state machine deadlocks and reachability.

Regarding the LINT noise, the checks are up to date checks. They only report on each module, not each instance of that module with the exception of parameterized modules, and then it is only things that are different as a result of the parameterization. There is a configuration GUI that makes it really easy to get up and running fast.
_________________
Ben Cohen http://www.systemverilog.us/
* SystemVerilog Assertions Handbook, 2nd Edition, 2010
* A Pragmatic Approach to VMM Adoption
* Using PSL/SUGAR ... 2nd Edition
* Real Chip Design and Verification
* Cmpt Design by Example
* VHDL books

Hanken · Senior Joined: Aug 02, 2005 Posts: 22

Hi Ben,

I am very interested in Jasper's tool, but I don't have chance to visit DAC. Can you explain a little bit more about this tool (its theory, flow). Did you try it with real design? It seems formal verfication is so hotter than ever. Razz

What is your opinion towards nowadays Formal Verification?

Thanks.

aloksanghavi · Newbie Joined: Mar 31, 2010 Posts: 1

Hi Hanken,

You can find more detailed info on Active Design below.

http://jasper-da.com/products/ActiveDesign.htm

Thanks.

vhdlcohen · Posted: Wed Jul 28, 2010 12:55 pm **Post subject:**