Carnegie Mellon University
Browse

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.

History

Date

2005-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC