Hierarchical models of synchronous circuits for formal verification and substitution
Elizabeth Wolf · 1996
As industrial circuit designs become larger and more complex, the use of simulation as the sole means for verification of their correctness no longer suffices. One of the potential methods to complement simulation is formal verification, in which mathematical methods are applied to prove that desired properties hold of circuit models. In this thesis, we develop a mathematical model of synchronous sequential circuits that supports both formal hierarchical verification and substitution. In order to facilitate hierarchical verification, we model synchronous circuit specifications and implementations uniformly. Each of these descriptions provides both a behavioral and a structural view of the circuit or specification being modeled. For formal verification, our framework provides a means for comparison of the behavior of a circuit model to a requirements specification in order to determine whether the circuit is an acceptable implementation of the specification. For substitution, and to support a modular verification process, it provides a structural view of a circuit and the capability to plug in one component in place of another in a circuit model. This allows us to determine whether or not the new component constitutes an acceptable substitution in terms of the desired behavior of the full circuit. We derive a requirements specification for the acceptable replacement components. In addition, our model supports nondeterministic specifications, which capture the minimum requirements of a circuit without forcing us to overspecify by including irrelevant details. Hierarchical descriptions of combinational circuits may often contain apparent loops. Previous existing formalisms have relied on syntactic methods for distinguishing apparent from actual unlatched feedback loops in hardware designs. However, these methods do not work correctly for nondeterministic models. Our model of the behavior of a synchronous circuit within a single clock cycle correctly handles such cyclic dependencies even in the presence of nondeterminism, by providing a semantic method to describe them. In addition to developing a theoretical framework to support behavioral and structural comparison of synchronous circuit models at various levels of detail, we have implemented and proved the correctness of automatic decision procedures for both formal verification and substitution using these models.