Posts Tagged ‘formal’

8 May, 2017

At the recent DVCon in Shanghai, China, my colleague Jin Hou delivered the tutorial “Back to Basics: Doing Formal the Right Way”. Jin is an expert in formal and CDC methodologies, and in her career she has trained hundreds of engineers how to get up to speed with formal, and leverage its strengths as part of a complete enterprise-class verification flow. I’ve been to DVCons in the US, EU, and India, so I was eager to hear her first-hand account of the latest incarnation of this successful conference series. Below is a review of her experience.

Joe: Tell me more about your tutorial

Jin: In recent years there has been a lot activity around automated formal apps. This is a good thing not only because they help any engineer take advantage of formal’s power, but their success has also inspired interest in property checking. Consequently, this tutorial was created to show engineers who are new to formal what is involved in the planning, setup, execution, and results analysis with formal property checking verification. Wherever it made sense, I would make analogies to testbench simulation flows to explain formal methodology, and show how formal and simulation can be used in combination.

——

Joe: Did you get to survey the attendees at all? If so, what were the results?

Jin: Yes, but first let me say the tutorial was standing room only – there were at least 40 people were in a room setup for half that number!

At the beginning I asked for a show of hands for the following questions:

“How many people are using formal now?” Only 3 people raised their hands.

“How many of you are thinking of using formal in 6 months?”  Just 7 hands went up.

In my 1-on-1 discussions after the tutorial concluded, an attendee told me, “Assertions are still pretty new to Chinese engineers. Except for [a major semiconductor supplier], most customers don’t have any assertion and formal experts.” However, I also heard some great news on this point: a professor from an area university told me his department was starting a course on SystemVerilog – including writing SVA — this coming academic year!

In general, it was clear to me that there is a great opportunity for formal usage to grow in China!

—–

Joe: Were there any particular comments or questions from the attendees?

Jin: The overall theme of the Q&A I received was around the benefits that property checking provided over other verification techniques. Indeed, I was directly asked “Why do you need formal?” It’s a fair question – especially since property checking with hand-written assertions (vs. automated formal apps) does impose a learning curve on its users; and it is not always obvious what formal is capable of doing better than the alternatives.

Of course we setup the tutorial to address exactly these concerns; so over the course of the presentation I showed how the formal can address many serious verification tasks long before a simulation testbench would be available. For starters, hand-written assertions themselves help designers communicate their concerns to the verification team, bridging the gaps between them. With such an “executable specification” (which, by the way, with the right syntax can be easily reused in simulation and emulation), verification tasks that would take forever in simulation can be quickly solved by formal. Perhaps the most well received example of this was when I spoke of how formal can deliver exhaustive proofs of liveness and safety properties.

[Ed. Note: “Liveness” == something good must eventually occur. “Safety” == something bad must never occur, i.e., good behavior should be always true. A well regarded, in-depth review of these valuable formal analyses is available here https://www.doc.ic.ac.uk/~jnm/book/firstbook/pdf/ch7.pdf ]

In general, the fact that you can do such significant verification with exhaustive results, before you write a single line of testbench code, means that formal should be part of any serious verification project.

—–

Joe: Looking back on the experience, how has it inspired you?

Jin: It’s given me great ideas on how we can further enhance our Verification Academy courses to help new formal users to get up to speed with the key concepts and work flows. In particular, we need to better promote “formal coverage” – what it tells you, how it helps the formal engineer measure their personal progress, and how it feeds into the overall verification project status alongside simulation code and functional coverage reporting. 

—–

Joe: Thanks, Jin!  Final thoughts?

Jin: While I enjoy supporting customers here in the San Francisco Bay Area, I also look forward to introducing more engineers to formal verification across China!

—–

If you went to DVCon in Shanghai — or in San Jose – this spring, please share your experiences in the comments below.

Until DAC, may your power consumption be low and your coverage be high!

Joe Hupcey III

Reference links:

DVCon Shanghai 2017 proceedings — https://dvcon-china.org/dvcon-china-history-archive

Safety & Liveness Properties, Chapter 7, Concurrency: State Models & Java Programs, Jeff Magee and Jeff Kramer, https://www.doc.ic.ac.uk/~jnm/book/firstbook/pdf/ch7.pdf

Related Verification Academy courses:

Getting Started with Formal-Based Technology
https://verificationacademy.com/courses/Getting-Started-with-Formal-Based-Technology

Formal Assertion-Based Verification
https://verificationacademy.com/courses/Formal-Assertion-Based-Verification

Formal-Based Technology: Automatic Formal Solutions
https://verificationacademy.com/courses/Formal-Based-Technology-Automatic-Formal-Solutions

Assertion-Based Verification
https://verificationacademy.com/courses/assertion-based-verification

, , , , , , , ,

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 www.verificationacademy.com, and it’s all FREE!

Enjoy!

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!): http://www.mentor.com/events/design-automation-conference/schedule

, , , , , , , , ,

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.

 

ARM

 

Doulos

 

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 DAC.com.

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

  • #ARM now hiring formal verification engineers in Austin: exciting tech challenge + Ram is a great guy to work with.…https://t.co/uwIXLHWqvg
  • Attention all SF Bay Area formal practitioners: next week Wednesday 7/26 on Mentor's Fremont campus the Verificatio…https://t.co/9Y0iFXJdYi
  • This is a very hands-on, creative role for a verification expert -- join us! https://t.co/jXWFGxGrpn

Follow jhupcey