Hardware Verification Using Coinductive Assertions
Steven Johnson, Paul S. Miner · 1998
Systems of mutually recursive stream equations provide a concise model of digital hardware designs. The formal design algebra presented by Johnson illustrates the utility of this representation for design derivation. The design derivation approach has been mechanized by Bose and applied to significant case studies. However, a design optimization sometimes depends upon the semantics of the implemented function. This cannot be captured within the design algebra. Design derivation needs to be augmented with additional verification strategies. The stream equations employed in the design derivation approach are an instance of definition corecursion. Therefore, the design derivation approach may be augmented using proof by coinduction. Coinduction is a useful strategy for proving that two sequential hardware designs have the same behavior. This enables safe substitution of an innovative optimization into a mature design. Furthermore, coinduction is useful for establishing that a signals within a design satisfy invariant properties. Such invariants, called coinductive assertions, are essential to ensure the validity of aggressive design optimizations. This dissertation illustrates how design derivation is augmented using the Prototype Verification System (PVS). A PVS library to provide the basic declarations needed for reasoning about streams is developed. Stream equations are defined using corecursion, and equality between streams is proven using coinduction. The combination of derivation-based and theorem prover-based verification is illustrated using two significant examples. First, a fault-tolerant clock synchronization circuit, suitable for use in critical applications, is developed using this combined approach. A clever optimization that reduces the chip area is verified using coinductive proof within PVS. The second example is the development of an architecture for floating-point division. A number of optimizations that reduce the cycle time of the inner loop of the algorithm are verified using the combined approach.