Modeling and Verifying Circuits Using Generalized Relative Timing

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.