Диссертация, Technische Universiteit Eindhoven, 1997, -156 pp.With the increasing complexity and tight time-to-market schedules of today’s digital systems, it is becoming more and more difficult to design correct circuits for these systems. Therefore, throughout the design process it is necessary to check that no errors are made. This task is called verification. Traditionally, a design is verified by simulating it extensively. This approach is no longer adequate, because it is too time-consuming and it gives no absolute guarantees about the correctness of the design. One of the approaches that have been put forward to solve these problems is formal verification. The key characteristic of this approach is that formal methods are applied to actually construct a mathematical proof for the correctness of the design.
In this thesis, we discuss formal methods for the verification of synchronous digital circuits. More specifically, we describe methods to verify the functional equivalence of circuits specified at the register transfer and gate level. Such methods can be used in practice to verify that the circuit descriptions preceding and following a design step define the same functionality. We focus on the development of formal verification methods with a high degree of automation and with sufficient performance to handle circuits of industrial complexity. Theoretically, most problems related to the formal verification of digital circuits belong to complexity classes for which no polynomial algorithms are believed to exist. Therefore the development of verification methods solving each problem instance in a reasonable time is out of the question. Instead, we have to find other ways to develop methods which perform adequately in practice. In this thesis, we apply an approach based on the observation that verification is typically used to compare circuits which show certain similarities. We propose verification methods which combine powerful general verification algorithms with techniques to utilize these similarities. We apply this approach to the following three verification problems.
The first problem we consider is that of verifying the functional equivalence of combinational circuits. We focus on the verification of combinational circuits optimized by logic synthesis tools. These synthesis tools typically have a limited effect on the structure of a circuit. Therefore, it is often possible to identify signals in the circuits preceding and following synthesis which implement the same function. We show how a well-known verification method based on binary decision diagrams (BDDs) can be extended to automatically detect and utilize these signals. We also demonstrate that the resulting method has sufficient performance to verify the correctness of circuits synthesized in an industrial environment.
The second verification problem we address in this thesis is that of verifying the functional equivalence of sequential circuits with identical state encodings. We show that if for each register an initial value is specified, the corresponding registers can be detected automatically by solving a sequence of combinational verification problems. Therefore, combinational verification methods can easily be extended to automatically extract the register correspondence. In practice, this means that it is not necessary to require that the register correspondence is specified explicitly or that it can be derived from the names of the registers.
Checking the functional equivalence of sequential circuits is the third and most general verification problem we consider in this thesis. We propose a BDD-based verification method which uses functional dependencies to utilize the relation between the state encodings of both circuits. These functional dependencies can be detected while calculating the reachable state space of the so-called product machine. We also propose two techniques to detect specific types of functional dependencies before the reachable state space is calculated. Exploiting functional dependencies clearly results in a significant increase in performance, and in some cases it also enables the verification of significantly larger circuits.
To manage the complexity of sequential verification, it is necessary to decompose the product machine into a number of smaller sub-machines which can each be analyzed separately. To really benefit from this approach, it is generally necessary to abstract from the detailed interactions between these sub-machines. Therefore, we investigate the use of weakly-preserving abstraction techniques in the context of sequential verification. We propose an appropriate abstraction mechanism and we present a decompositionbased verification method based on this mechanism. Furthermore, we also describe abstraction techniques for disproving the equivalence of sequential circuits.Formal Verification
Preliminaries
Combinational Verification
Register Correspondences
Sequential Verification
Abstraction Techniques
Concluding Remarks
