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:
[LIST=1]
- 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
- 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
- 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
- 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
- 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 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
- 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
- checking that bus protocols (for example a bus bridge from processor to an AMBA bus in an ARM-based design) are correctly implemented
- 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
- 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…
TSMC Unveils the World’s Most Advanced Logic Technology at IEDM