You know a webinar is hot when the questions just keep rolling on in from the audience and go well into overtime. Such was the case in a newly archived Cadence webinar titled "Automate Assertion Generation for Simulation, Formal and Emulation Flows." The webinar showed how "assertion synthesis," as provided by Cadence partner NextOp Software, can expedite assertion-based verification, reveal functional coverage holes, and increase verification observability.
The Oct. 13 webinar was presented by Joe Hupcey, product marketing director at Cadence, and Yuan Lu, CTO of NextOp. It is part of an ongoing functional verification webinar series that will extend into November and December.
Hupcey started with a brief review of ABV terminology, noting that assertions express desired behavior of a device under test (DUT), while cover statements express the desired reachability of states in the DUT and the environment. Both are subcategories of "properties," which are statements about the behavior of a design and its environment. The value of ABV, Hupcey said, is two-fold - significant time savings, and higher design quality. He noted that ABV can result in a 25% faster time to market.
So, why isn't ABV in broader use? One reason is that assertions are difficult to create and maintain due to syntax complexity. Manual coding typically takes 20 minutes to 1 hour for each assertion. It is challenging to debug failed assertions, and easy to fall short of the number of assertions needed. Thus, the ability to automatically generate assertions through assertion synthesis is a tremendous benefit.
One tool that automatically generates assertions is Automatic Formal Analysis (AFA), which is included with the Cadence Incisive Formal Verifier and Incisive Enterprise Verifier. This is a pushbutton solution that generates assertions for the most common design errors from the DUT. However, it only supports basic white box assertions. As Hupcey noted, the BugScope product from NextOp goes further.
Yuan Lu took over from here and noted that BugScope creates both high-quality white box assertions and high-quality functional coverage goals. It leverages simulation to create assertions automatically. Lu said that BugScope can produce assertions for 1-10% of RTL lines, without duplicating RTL or other properties. Assertions offer a low runtime overhead and can be leveraged in simulation, formal verification, and emulation flows.
As shown in a demo in the webinar, BugScope has three basic steps:
- Simulate using the BugScope PLI. Input is the testbench, plus test vectors and RTL. Output is a NextOp database file for each simulation run.
- BugScope post processing. Input is NextOp databases plus RTL. Output is BugScope-generated properties.
- Users manually classify properties as assertions or cover statements. BugScope supports SystemVerilog assertions (SVA), Property Specification Language (PSL), or Verilog.
The diagram below shows how BugScope works in a metric-drive verification flow with the Cadence Incisive platform. Basically, users start with a UVM testbench in the Incisive Enterprise Simulator (IES) and run BugScope to synthesize assertions and cover statements. These can be brought into simulation, formal or emulation flows, and can target code coverage in Incisive Enterprise Verifier (IEV). Finally, results are displayed in an executable vPlan (verification plan) in Incisive Enterprise Manager.
Here are a few of the many questions that were asked by attendees - and answered by Lu -- during the webinar.
Q: Does the tool have the capacity to do an entire chip in one shot, or is it done in pieces?
A: The tool is module based, but you can launch as many modules as possible to the server farm.
Q: If the RTL code has a bug, and the RTL is incorrect, will NextOp create an incorrect assertion on incorrect behavior?
A: If you have good behavior in your simulation and you still have a bug that was never activated, hopefully our cover properties will show that. If a bug is activated but does not propagate to the checker, hopefully we can discover the cover property that blocks this bug. When we give you a property you will probably realize something is wrong with the RTL.
Q: Does BugScope require a testbench or can it just get assertions from RTL?
A: We require a testbench. If there's no testbench, you can use [Cadence] AFA or manual generation.
Q: How complex are the assertions? Are they structural or operational?
A: We are focusing on white box assertions and we typically generate assertions that take one to two cycles. We don't generate long temporal assertions for now. We have a pipeline to add temporal assertions in future versions of the tool.
Q: If I'm not familiar with assertions, can I interpret the output of the tool?
A: We are not targeting experts, and people who are not used to assertion languages can use the tool. The output format is very much like Verilog.
Q: Do you synthesize assertions for design behavior not simulated by any test?
A: In such an area we cannot give you assertions, but we can tell you this area was never covered.
As Hupcey said at the end of the webinar, "ABV is extraordinarily powerful. And assertion synthesis with BugScope automates the front end of this challenge. It creates the assertions and the coverage and identifies pretty well hidden corner cases in the process." Further information, including a whitepaper, is available at the NextOp web site. To view the webinar, available free to Cadence Community members, click here.
Related Cadence Community blog posts
Q&A: NextOp CEO Describes "Assertion Synthesis"
Video: Interview With NextOp CEO Yunshan Zhu on Assertion-Based Verification (ABV) With "BugScope"
Connections Partner NextOp on Assertion Synthesis and Assertion-Based Verification (ABV) with "BugScope"
Video: DVCon and DVClub Case Study: NextOp's BugScope for Assertion-Based Verification (ABV)
Video: DAC 2011 Update From NextOp CEO Yunshan Zhu
Video: DVCon 2011 Update From NextOp CEO Yunshan Zhu
DVClub: Verification Users Discuss Assertion Challenges and Solutions