In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ, Starnet, Forte Design System and Cypber WorkBench

User track presentation on formal verification

The user track presentation is where users of the EDA present their work on how make the best and creative use of the EDA tools.  There are about 40 presentation today and about 10 of them is related to verification.  I read their presentation poster and then talk to them to exchange ideas.  Here is a few pointers I picked up from the presentation:

• Use formal verification tool to aid closing of code coverage.  For the line of code is not yet covered, we can write a property statement for that line, feed it to the formal engine and ask it to come up with a input sequence that will trigger the assertion.  The formal engine may either generate an input sequence or prove the line is unreachable.
• Sun/Oracle has the idea to run the property in the simulation to keep both formal and simulation in sync.  The trick  is to have some “useless” signals in the DUT to qualify the assertion check to avoid having tons of false-negative when the DUT is an invalid state.
• One presentation presents the result that using formal verification early in the development cycle will catch more bugs in FV.  Duh!
• This is a good one.  In formal verification, there are two types of properties, abstract properties that is safe and incomplete, constraint properties that are unsafe and complete.  Using which properties type is a trade off between finding counter example or getting a full proof of the design.
• Exhaust prove is difficult, it is more practical to limit the proof to some reasonable depth.

Onespin

This company build formal verification tool.  Their basic product is similar to IFV, except it has a better and easier to use GUI that allow users do a lot more interaction and visualization.  Their flag ship product is operational formal ABV, instead of defining basic cause-reaction properties in ABV, the tool provides assertion library allow user define operational properties.  Then the user will go through an iteration to get a full coverage on the formal space with the aid of the tool.  The idea is to generate a set of properties that completely define the RTL.  I think the tool will work as it advertise because at the end is human who has to enter the missing properties.  However I wonder what’s the use of getting a complete ABV definition of the RTL.  It seems the idea is totally up side down.  I guess the idea is instead of auditing the implementation of the RTL code, the auditor should audit the complete properties of the code.

One thing I don’t like about Onespin is they have way too many products and it’s really confusing.  The flag ship product has all the features and the rest are just crippled version with fancy marketing terms simply to confuse users.  For example, the difference between two products is only the ability to load external property files vs the property has to be in the same file of the RTL code.  I don’t really like this kind of marketing ploy simply exist to milk more money from the customer.

Jasper

Jasper is THE formal verification tool vendor.   I spent almost 2 hours (and have my lunch) in their booth walk through all the demo and try out almost all the features in their product.  This is the tools of choice in may formal verification presentation in DAC.  The tool is much more user friendly and powerful than IFV.  IFV seems so primitive compare to Jasper.  Jasper also has property libraries for different memory, FIFO model instead of just black-boxing them out.  It support tunnel, so the user can steer the formal engine.  It comes with a lot more formal engines than IFV and gives very clever ways to get a counter example or a proof.  Active design uses the same formal engine but it is for a different application.  The idea is if we have poorly documented legacy RTL, the new designer can use active design to generate properties of the RTL and understand exactly what the RTL can and cannot do.  Another benefit is when we ask the designer can the RTL do such and such, we no longer have to take their work for it, the designer can generate recipe to prove their design to answer our question.  Jasper has an account manager for PMC and she know Bob and Alan.  I think we really should try Jasper in Digi and get Bob setup the tool for us.

SpringSoft

Springsoft acquired Debussy.  Debussy and Verdi does not change much, other than it added support to power-aware design and system verilog.  Siloti is an very neat add-on to Debussy for waveform compression.   The idea is very neat, in simulation we really only need the input, output and flip flop values in the waveform database.  The waveform viewer can calculate the value of the combination signals on the fly.  The waveform database is only 25% of the original size.  Certitude is a tool to test the testbench.  It corrupts the DUT and check whether the testbench fail.  If the testbench still pass when there is signal corruption in the DUT, there must be something wrong with the testbench.

Tuscany

This company has only 1 product.  It is a web interface GUI to display the timing report.  I like the GUI, even though I don’t know much about timing report.  I can see it solve the problem of how to keep track of so many timing reports.

AMIQ

Another small company with only 1 product.  They have a DVT IDE for Specman and SystemVerilog base on Eclipse, the open source Java IDE.  The IDE works like Visual Studio, it has editor, data browser, structure tree, keyword auto-complete, quick linting, hooks to launch Specrun, all under the same GUI.  It is a lot more user friendly compare to editing e code with vi or Emacs.  They are working on the debug interface hooking into the simulation for the next release, it will work like gdb.  I highly recommend purchase a few license (1k per seat, but I am sure Bob can negotiate volume discount if we buy more), give it out to the team to evaluate the product. I think we will see productivity increase with the DVT IDE instantly.

Starnet

They are selling a VNC replacement that they claim s much faster then VNC.  I know CAD is evaluating some fast VNC-like software right now.  Maybe we should get CAD to try out this product as well.  We all know how painful is it to view waveform in Banaglore via VNC.

Forte Design System and Cypber WorkBench

Both company sells high level synthesis (HLS) tool, that compile SystemC into RTL code.  It looks like HLS is finally here.  I don’t have enough domain knowledge to evaluate the tools.  All I can tell is they have a nice GUI and the RTL code generated is not very readable.  I asked about is there any limitation on the SystemC code and the efficiency of the generated RTL, I only got the typical marketing answer.  Too bad that both tools only work with SystemC, it would be nice if there is HLS for behavioral SystemVerilog.