How Can You Say That Formal Verification Is Exhaustive?
As a companion to my previous post on Learn Formal the Easy Way, allow me to explain what are often the most perplexing – yet fundamental – aspects of formal analysis: formal results are good for all time, and all inputs – i.e. formal verification is exhaustive.
I grant that this sounds like a wildly exaggerated claim for any technology – indeed, over the years several new-to-formal customers have, um, enthusiastically shared their skepticism about this with me. However, this claim can be clearly proven (formal pun intended); but the problem is that the official academic proof can take several graduate-level lectures and math that (if you’re like me) will leave you speechless and more confused than before. Fortunately, (to the chagrin of my PhD colleagues), I’ve discovered an overly simplified analogy to explain how formal is exhaustive: finding solutions to the quadratic equation:
ax2 + bx + c = 0
Recall from your school days that in the above equation “a”, “b”, and “c” are constants, and the goal is to solve for the value(s) of variable “x”.
Here is where the analogy comes in:
- The constrained-random simulation approach to solving this equation would be to randomly plug-in numbers in the hope you eventually satisfy the equation.
- Conversely, the “formal-style” approach is to algebraically compute the solutions to this.
Think about it: formal analysis tools take the HDL code for your DUT (VHDL, Verilog, SystemVerilog, or SystemC) and properties (SVA or PSL) that capture the intended behavior and operational constraints of said-HDL (i.e. a testbench), automagically converts it all into big, fat, Boolean equations under-the-hood, then algebraically solves them for the solutions to “x”. If there is a mismatch of any sort between the DUT and testbench “math”, the tool reports it. In short, formal analysis seeks a mathematical solution to the equations, and informs you if it can or cannot be done for all (legal) inputs.
But what about the “for all time” claim?
One thing to notice about the above quadratic equation — and the Boolean equations that the formal tools create from your code – is that there is no parameter for time at all. A mathematical solution to an equation that does not include time as a variable is independent of time – rephrasing, its solutions are valid for all time.
Again, I appreciate that the above analogy is highly over-simplified; but the principles it illustrates are correct: formal results are valid for all inputs, and all time. In a word, formal verification is exhaustive!
Few things in life are more certain than a mathematical proof; so if you are looking to benefit from this powerful technology and are new-to-formal, I welcome you to check out the formal verification areas of Verification Academy to test the waters with the many automated formal apps, or just dive right into property checking!
Joe Hupcey III,
for the Siemens EDA Formal Verification team
Reference links:
Verification Horizons: Learn Formal the Easy Way
Verification Academy > Courses > Getting Started with Formal-Based Technology
