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?