It’s common knowledge that formal property verification – “formal”, for short – delivers exhaustive results. In a nutshell, formal tools statically analyze a design’s behavior with respect to a given set of properties, exhaustively exploring all possible input sequences in a breadth-first search manner to uncover design errors that would otherwise be missed.
But what does that really mean?
How can you get away with saying the results of a formal analysis are truly and completely exhaustive; for all time, and for all inputs to the DUT?
How does it all work?
This two part video series answers these questions in two stages:
First, formal verification expert Doug Smith gives a high level introduction on what formal property checking is about: how formal differs from simulation, how constraints on expected inputs apply in the formal world, how it provides exhaustive results, and more.
Next, Jeremy Levitt of the Questa Formal R&D team takes you on a deep dive into the many different formal algorithms used by Questa products under-the-hood. Specifically, Jeremy walks through what are formal property checking engines and how they work, why they incredibly powerful for some properties, but not so good for others, and what's the state of the art and what's coming in the near future.
