Formal verification has grown in importance as designs have grown and it has become necessary to face up to the theoretical impossibility of using simulation to get complete coverage along with the practical impossibility of simulating enough to even get close.
There are a number of solvers for what is called satisfiability (SAT) but these work in a rather rarefied theoretical environment different from the way designers work. So it is necessary to add a modeling layer to connect properties in the designer’s world to the types of equations that the solvers can prove. Some properties require additional logic to be added to the design in order to convert, for example, a temporal property into one that an SAT engine can prove.
The modeling layer takes in the design description, the property/properties to be verified, the initial state of the design and any constraints. It then transforms these into the formal equations required by the SAT solver. The solver attempts to find a “witness” for each property. A witness is a sequence of input vectors that make the property true while satisfying all the constraints.
The SAT solver produces one of 3 outcomes:
[LIST=1]
As an aside, formal verification products are quite interesting to sell. Typically, to evaluate them, the customer will have an application engineer run an old design through the tool, one that is already in production. It is interesting when the design promptly fails and a sequence is found that causes the design to do something it shouldn’t. Of course, you don’t tell the customer all the problems, they need to buy the tool to find that out.
Atrenta’s white papers on formal verification, which go into a lot more detail, are available here.
Next Generation of Systems Design at Siemens