Modeling and Verifying Circuits Using Generalized Relative Timing

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