DocumentCode :
3257249
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
fYear :
1992
fDate :
8-12 Jun 1992
Firstpage :
405
Lastpage :
409
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design Automation Conference, 1992. Proceedings., 29th ACM/IEEE
Conference_Location :
Anaheim, CA
ISSN :
0738-100X
Print_ISBN :
0-8186-2822-7
Type :
conf
DOI :
10.1109/DAC.1992.227770
Filename :
227770
Link To Document :
بازگشت