Carnegie Mellon University

File(s) stored somewhere else

Please note: Linked content is NOT stored on Carnegie Mellon University and we can't guarantee its availability, quality, security or accept any liability.

Modeling and Verifying Circuits Using Generalized Relative Timing

journal contribution
posted on 2005-01-01, 00:00 authored by Sanjit A. Seshia, Randal BryantRandal Bryant, Kenneth S. Stevens

We propose a novel technique for modeling and verifying
timed circuits based on the notion of generalized relative
timing. Generalized relative timing constraints can express
not just a relative ordering between events, but also
some forms of metric timing constraints. Circuits modeled
using generalized relative timing constraints are formally
encoded as timed automata. Novel fully symbolic verification
algorithms for timed automata are then used to either
verify a temporal logic property or to check conformance
against an untimed specification. The combination
of our new modeling technique with fully symbolic verification
methods enables us to verify larger circuits than has
been possible with other approaches. We present case studies
to demonstrate our approach, including a self-timed circuit
used in the integer unit of the Intel Pentium 4 processor.




Usage metrics