Title :
On the temporal equivalence of sequential circuits
Author :
Shenoy, Narendra V. ; Singh, Kanwar Jit ; Brayton, Robert K. ; Sangiovanni-Vincentelli, Alberto L.
Author_Institution :
California Univ., Berkeley, CA, USA
Abstract :
The authors extend the abstract notion of temporal behavior to compare arbitrary circuits with arbitrary multiphase clocking schemes. They consider the input-output behavior of circuits with respect to time. Properties are discussed that remain invariant under certain transformations. Constraints are derived that permit a legal retiming in the case of multiphase sequential circuits with edge triggered and/or transparent latches. For a particular design style an efficient procedure is described to check for temporal equivalence of sequential circuits. A model and a formal definition for the temporal behavior of an arbitrary multiphase circuits and an algorithm for formal verification of the temporal behavior of circuits are outlined
Keywords :
formal verification; sequential circuits; temporal logic; abstract notion; arbitrary circuits; arbitrary multiphase clocking schemes; formal verification; input-output behavior; sequential circuits; temporal behavior; temporal equivalence; transparent latches; Circuit synthesis; Clocks; Delay effects; Equivalent circuits; Latches; Law; Legal factors; Sequential circuits;
Conference_Titel :
Design Automation Conference, 1992. Proceedings., 29th ACM/IEEE
Conference_Location :
Anaheim, CA
Print_ISBN :
0-8186-2822-7
DOI :
10.1109/DAC.1992.227770