SemiWiki Podcast Banner
WP_Term Object
    [term_id] => 157
    [name] => EDA
    [slug] => eda
    [term_group] => 0
    [term_taxonomy_id] => 157
    [taxonomy] => category
    [description] => Electronic Design Automation
    [parent] => 0
    [count] => 3239
    [filter] => raw
    [cat_ID] => 157
    [category_count] => 3239
    [category_description] => Electronic Design Automation
    [cat_name] => EDA
    [category_nicename] => eda
    [category_parent] => 0

Pizza con Questa

Pizza con Questa
by Paul McLellan on 07-30-2014 at 11:01 am

 Last week I went to a lunch and learn at Mentor about their Questa formal product given by Kurt Takara. Like everyone else these days, Questa is packaged as a number of Apps for doing different tasks. Formal verification is different from other EDA tools in that different approaches can be used for different sub-tasks. There are three outcomes: it succeeds in proving correctness (you are done), it succeeds in finding a bug (you have to fix it) or it doesn’t complete. But if one approach either succeeds or fails you don’t need to try other approaches. Indeed, you can extend this to products from different vendors, and if one vendor succeeds in proving something correct you don’t need to try it in another tool.

Kurt structured his talk as a top-10 list. Verification is a big deal. Mentor funded a study that discovered that the ratio of verification engineers to design engineers is now 1-1. But on top of that, the design engineers spend half their time on verification too. So that comes to about 75% of effort going on verification.

The Apps in Questa can be split up into groups. There are automatic formal Apps such as clock-domain crossing checks. There are traditional formal Apps such as protocol checking. There are assertion-based verification Apps such as bug-hunting. And then there are some specialized Apps (that were not covered in the lunch and learn) for things like cache-coherency checking.

The top 10 list was:

  • Clock domain crossing (CDC)

    • this checks that when different clock domains interact that appropriate precautions have been taken to handle the asynchronous nature of the signals. An important additional issue is that in modern designs where IEEE 1801 (UPF) may contain the power policy, the power intent could introduce CDC paths that need to be checked
  • AutoCheck

    • this is push-button formal for debugging, requiring no assertions or testbench. it runs multiple engines and explores the design state space looking for corner case bugs such as unreachable states or transitions in state-machines
  • X-check

    • simulation doesn’t handle X values very well, and is often pessimistic (it transmits an X value when the value is well defined) or optimistic (it transmits a value when it should propagate an X). X-check finds these problem areas
  • CoverCheck

    • this App automates code coverage checks, discovering what is coverable and highlighting areas that are not coverable (there is no sequence of inputs that can reach that line of code) where waivers need to be granted
  • PropGen

    • automation of assertion-based verification. Creates assertions to check design implementation and finds coverage holes, comparing results to design intent. For IP blocks it can create self-checking blocks that detect misuse of the IP at the SoC level
  • Connectivity checking

    • connectivity checking seems like something where formal might be a sledgehammer to crack a nut, but with designs having 1000s of I/Os, often heavily multiplexed, just checking that everything is hooked up right using simulation is tedious and error-prone. The formal approach can catch not just the obvious errors but also corner cases that simulation would probably miss
  • Control and status register (CSR) checking

    • reads the RTL and the register description file and automatically creates assertions for CSR verification (and then checks them), for example ensuring that a read-only register is never written
  • Interface protocol compliance checking

    • checking that bus protocols (for example a bus bridge from processor to an AMBA bus in an ARM-based design) are correctly implemented
  • IP block design assurance

    • for blocks where it makes sense, automatically checking the integrity of the outputs from the block based on the inputs, basically that the block meets its high level requirements
  • Bug hunting

    • formal is not always the first thing that comes to mind post-silicon, but it is a good weapon in the search for a bug that previous verification (such as simulation) obviously missed. The problem is probably deep and an obscure corner case that simulation never exercised. Capturing the bug as an assertion and then unleashing Questa to find what’s wrong often quickly produces a waveform that exhibits the problem

    But the proof of the pudding (formally proved of course) is in the eating. As NamDo Kim of Samsung says (and also presented in papers at the last two DVCons):We have successfully deployed the wide range of Questa applications from fully automatic formal to property checking to improve productivity and design quality.

    More articles by Paul McLellan…

    Share this post via:

  • Comments

    There are no comments yet.

    You must register or log in to view/post comments.