postscript version (formated doubleside, 187 pp.)
Validation of industrial designs is becoming more challenging as technology advances and demand for higher performance increases. One of the most suitable debugging aids is automatic formal verification . Unlike simulation, which tests behaviors under a specific execution, automatic formal verification tests behaviors under all possible executions of a system, and therefore, is able to detect errors that cannot be reliably repeated using simulation.
However, automatic formal verification is limited by the state explosion problem . The number of states for practical systems is often too large to check exhaustively within the limited time and memory that is available. Existing solutions have widened the range of verifiable systems, but they are either insufficient or hard to use.
This thesis presents several techniques for reducing the number of states that are examined in automatic formal verification. These techniques have been evaluated on high-level descriptions of industrial designs, rather than gate-level descriptions of circuits, because maximum economic advantage of using verification relies on catching the most expensive errors as early as possible.
A major contribution of this thesis is the design of simple extensions to the Murphi description language, which enable us to convert two existing abstraction strategies into two fully automatic algorithms, making these strategies easy to use and safe to apply.
The algorithms rely on two facts about high-level designs: they frequently exhibit structural symmetry, and their behavior is often independent of the exact number of replicated components they contain . A static analysis of a Murphi description can identify these characteristics, and the verification tool (or the user) can then safely change the description to include appropriate extensions. With the extensions, the verification tool can automatically remove redundant information in the corresponding state graph, thereby decreasing the number of states necessary to represent the system.
Reductions of more than two orders of magnitude, in both time and memory requirements, were obtained through the use of these two reduction algorithms. In the cases of two important classes of infinite systems, infinite state graphs were automatically converted to small finite state graphs.
Another contribution is the design of a new state space reduction algorithm, which relies on reversible rules (transitions that do not lose information) in a system description. This new reduction algorithm can be used simultaneously with the other two algorithms, further reducing the time and memory requirements in automatic formal verification.
These techniques, implemented in the Murphi verification system, have been applied to a wide range of applications, such as cache coherence protocols, distributed algorithms and memory models. With these new techniques, complex systems that used to take more than a few hundred megabytes of memory and many hours to verify can now be verified in less than one megabytes of memory and a few minutes.
Norris's Publications