Posts Tagged ‘formal’

18 November, 2015

500x_shutterstock_37917877Given the dramatic increase in the scalability of formal engines over the past 5 years, “formal testbenches” have grown to comprise hundreds, if not thousands, of assertions, constraint properties, and cover properties. Like with simulation-based constrained-random verification, the number of constraints and the overlap and dependencies among them can quickly exceed what a single engineer can envision. Rephrasing, as the number of constraint properties grows from dozens to hundreds, it’s easy for them to constrain the input state space such that some of the legal input scenarios are omitted, thus causing assertions to be vacuous and/or cover statements unreachable. Fortunately, there is a clear procedure you can follow to untangle your formal constraints and move forward with verification.

First, temporarily remove ALL the constraints, run Questa PropCheck, and see which assertions are  reported as being “vacuous” – i.e. the property itself is inconsistent such that it never can be true — a trivial example is if you mistakenly ANDed a signal to its complement somehow. Naturally, the first step is to debug and fix any obvious errors. Vacuity can also be due to inconsistency with the design’s operation. Regardless of the source of the vacuity, these cases will need to be fixed regardless of external constraints.

Next, bring back in all the constraints and rerun PropCheck. This time some perfectly good properties could still be reported as being “vacuous”. Thus, if the properties ran clean before, without the constraints, chances are you are over-constraining the design with constraint properties that somehow conflict with each other to produce a false positive result – i.e. an error is reported when there really is none. This is where a very straightforward methodology described by Anshul Jain of Oski Technology comes in.

In his Verification Horizons article titled “Minimizing Constraints to Debug Vacuous Proofs”, Anshul outlines an easy-to-implement “divide and conquer” methodology that identifies a “minimum failing subset” (MFS) of constraints with a minimum number of formal runs.  In a nutshell, the recommended process is to split the number of constraints in half, execute a formal run with only one of the halves, and see if the formal tool still reports a vacuous proof and/or shows over-constraining. Then try the “other half” and see if vacuity/over-constraining is detected. If the properties run clean on one half or the other, you know the issue is in the other half. Next, keep recursively commenting out “half of the halves” until you’ve isolated the overwrought constraint properties.

As the article shows, even if you have 1,000 constraint properties, if one constraint is the culprit the worst-case is that you’ll only have to do 15 iterations to find your needle in a haystack.

I trust this tip will help you reach your verification goals faster – please share your questions and experiences in the Comments section.

Happy verifying!

Joe Hupcey III,
on behalf of the Questa Formal and CDC team

, , , ,

8 June, 2015

Do you have a really tough verification problem – one that takes seemingly forever for a testbench simulation to solve – and are left wondering whether an automated formal application would be better suited for the task?

Are you curious about formal or clock-domain crossing verification, but are overwhelmed by all the results you get from a Google search?

Are you worried that adding in low power circuitry with a UPF file will completely mess up your CDC analysis?

Good news: inspired by the success of the UVM courses on the Verification Academy website, the Questa Formal and CDC team has created all new courses on a whole variety of formal and CDC-related subjects that address these questions and more.  New topics that are covered include:

* What’s a formal app, and what are the benefits of the approach?

* Reviews of automated formal apps for bug hunting, exhaustive connectivity checking and register verification, X-state analysis, and more

* New topics in CDC verification, such as the need for reconvergence analysis, and power-aware CDC verification

* How to get started with direct property checking including: test planning for formal, SVA coding tricks that get the most out of the formal analysis engines AND ensure reuse with simulation and emulation, how to setup the analysis for rapidly reaching a solution, and how to measure formal coverage and estimate whether you have enough assertions

The best part: all of this content is available NOW at, and it’s all FREE!


Joe Hupcey III,
on behalf of the Questa Formal and CDC team

P.S. If you’re coming to the DAC in San Francisco, be sure to come by the Verification Academy booth (#2408) for live presentations, end-user case studies, and demos on the full range of verification topics – UVM, low power, portable stimulus, formal, CDC, hardware-software co-verification, and more.  Follow this link for all the details & schedule of events (including “Formal & CDC Day” on June 10!):

, , , , , , , , ,

20 July, 2012

Live & In-Person at DAC 2012!

DAC 2012 4Verification Academy, the brain child of Harry Foster, Chief Verification Scientist at Mentor Graphics, was live from the Design Automation Conference tradeshow floor this year.  Harry is pictured to the right giving an update on his popular verification survey from the DAC tradeshow floor.

The Verification Academy, predominantly a web-based resource is a popular site for verification information with more than 11,000 registered members for forum access on topics ranging from OVM/UVM, SystemVerilog and Analog/Mixed-Signal design.  The popular OVM/UVM Cookbook, which used to be available as a print edition, is now a live online resource there as well.  A whole host of educational modules and seminars can also be found there too.

If you know about the Verification Academy, you know all about  the content mentioned above and that there is much more to be found there.  For those who don’t know as much about it, Harry took a break from the being at the Verification Academy booth at DAC to discuss the Verification Academy with Luke Collins, Technology Journalist, Tech Design Forum.  (Flash is required to watch Harry discuss Verification Academy with Luke.)

The Verification Academy at DAC was a great venue to connect in person with other Verification Academy users to discuss standards, methodologies, flows and other industry trends.  Each hour there were short presentations by Verification Academy members that proved to be a popular way to start some interesting conversations.  While we realize not all Verification Academy members were able to attend DAC in person, we know many have expressed an interest to some of the presentations.  Verification Academy “Total Access” members now have access to many of the presentations.






Thales Alenia Space


Test & Verification Solutions


Willamette HDL


Sunburst Design


Mentor Graphics

Total Access members can also download all the presentations in a .zip file.  Happy reading to all those who were unable to visit us at DAC and thank you to all who were able to stop by and visit.

, , , , , , , , , , , , , , , , , , , ,

7 June, 2010

After spending years verifying ASICs with dynamic simulation, I started working on static verification 10 years ago in a startup called 0-In Design Automation. I firmly believe that static verification can complement dynamic simulation. Static verification uses synthesis and formal technologies to find bugs in the design. It does not rely on simulation stimulus. You do not need to exercise the bugs, propagate the results, and check the outputs to detect them.

Static verification includes RTL lint, static checks, formal checks, automated and assertion-based formal property checking. To read more on static verification, you can take a look at my white paper: Getting Started With Static Verification. If you are interested in formal methods, you can take a look at Harry Foster’s white paper: Why Now for Formal Property Checking. Both can be found in the Knowledge Center of

In the future, we are going to talk about individual static verification technologies and its application in areas such as RTL verification, clock domain crossing verification, low power verification, timing constraint verification, etc. Your feedback and comments are most welcome.

, , , , ,

@dennisbrophy tweets

Follow dennisbrophy

@dave_59 tweets

Follow dave_59

@jhupcey tweets

Follow jhupcey