Feb. 18, 2011, 3:10 a.m.
posted by nfrank
Using Model-Checking Tools
In this section we will look at practical issues encountered when using model checkers. There are three stages in the cycle of verifying using a model checker: property writing, input constraining, and property debugging.
Before writing properties for a design, the verification engineer has to have a firm grasp of the specifications of the design. This is usually accomplished by reading the specification documentation and communicating with the architects.
Because of memory capacity and runtime limitations, most industrial designs cannot be accepted as a whole by a model checker. Instead, blocks or modules relevant to the properties under verification are carved out and run on a model checker. As a result, the user often will have to constrain the inputs of the block to be consistent with those values in the embedded environment. Without constraining to legal inputs, false failures may occur. Because the block is carved out from the design, some of the primary inputs to the block are not primary inputs to the design, but are intermediate nodes. The legal values of these intermediate-turn-primary inputs may not be obvious to the verification engineer, and in most situations they must be determined through debugging false failures. Therefore, the constraining process demands a major engineering effort. Constraining inputs, in essence, builds a model of the environment in which the block resides in the design. If the block is in a feedback loop of the design, constraining amounts to recreating the feedback loop around the block. This use of constraints is illustrated in Figure.
32. (A) The block under verification is embedded in the design. (B) The block is verified as a standalone. The constraints are added to ensure that only legal inputs are given to the block.
Once a property fails, the tool will generate a counterexample for the user to simulate to determine why the property failed. By understanding the counterexample, the user determines whether the failure was a design fault or whether it was caused by an illegal input. In the former case, the design is reworked; in the latter case, more input constraints are added to eliminate the illegal values. Overconstraining, meaning some legal values are prevented from feeding the inputs, can cause false successes, which are far more damaging than false failures. These steps are repeated until all properties have been proved correct.