Report Number: CS-TR-95-1557
Institution: Stanford University, Department of Computer Science
Title: Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution
Author: Wolf, Elizabeth Susan
Date: October 1995
Abstract: We develop a mathematical model of synchronous sequential circuits that supports both formal hierarchical verification and substitution. We have implemented and proved the correctness of automatic decision procedures for both of these applications using these models. For 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. We compare the behavior of a circuit model to a requirements specification in order to determine whether the circuit is an acceptable implementation of the specification. Our structural view of a circuit provides the capability to plug in one circuit component in place of another. We derive a requirements specification for the acceptable replacement components, in terms of the desired behavior of the full circuit. We also support nondeterministic specifications, which capture the minimum requirements of a circuit. Previous formalisms have relied on syntactic methods for distinguishing apparent from actual unlatched feedback loops in hierarchical hardware designs. However, these methods are not applicable to nondeterministic models. Our model of the behavior of a synchronous circuit within a single clock cycle provides a semantic method to identify cyclic dependencies even in the presence of nondeterminism.
http://i.stanford.edu/pub/cstr/reports/cs/tr/95/1557/CS-TR-95-1557.pdf