TECHNICAL SESSION Today's complex electronic designs contain many behaviors that are difficult or even impossible to fully verify using conventional simulation-based verification techniques (For example, complex control logic, error recovery circuitry, Single Event Upset detection and correction logic, internal storage elements such as FIFOs, and many others). Verifying these types of design behaviors using simulation can lead to extremely long (and expensive) design verification tasks. Furthermore, even after "completing" the verification task, the design in question might not behave properly under all circumstances. It's common knowledge that bugs left in any design can be problematic, but for certain types and classes of designs, design errors are simply intolerable, especially if they are contained in satellites (where repair is intractable), safety critical designs (where bugs could cause injury or death), or military designs (where errors could place our military personnel or innocent bystanders in mortal peril).
Luckily, there are alternative approaches that can be used to verify design correctness that are significantly faster and more thorough than traditional simulation-based verification. One such technique is Static Formal Verification (also known as "Model Checking"). Static Formal Verification is a technique that utilizes a mathematical analysis of the synthesizable digital design, and creates an unequivocal proof that the design behavior in question is, indeed, 100% correct – or it will prove that the design is NOT correct (i.e. It contains a bug), and will provide a waveform trace demonstrating the failure. This analysis is exhaustive, covering all input conditions across all time. When a design MUST be correct, and extremely thorough or exhaustive verification is needed, then Static Formal Verification is obviously a good technology to have in your tool belt. Static Formal Verification has a very strong pedigree. Many companies have used it for more than 15 years, and its popularity is growing rapidly thanks to IEEE design and verification standards.
This presentation will discuss the use of Static Formal Verification, what it is and how it works, as well as the types of design behaviors where it is most and least effective. It will also discuss limitations and caveats, and provide links to papers and presentations containing more detailed information.