Relative timing based verification of timed circuits and systems
- 23 April 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 15228681,p. 115-124
- https://doi.org/10.1109/async.2002.1000302
Abstract
Aggressive timed circuits, including synchronous and asynchronous self-resetting circuits, are particularly challenging to design and verify due to complicated timing constraints that must hold to ensure correct operation. Identifying a small, sufficient, and easily verifiable set of relative timing constraints simplifies both design and verification. However, the manual identification of these constraints is a complex and error-prone process. This paper presents the first systematic algorithm to generate and optimize relative timing constraints sufficient to guarantee correctness. The algorithm has been implemented in our RTCG tool and has been applied to several real-life circuits. In all cases, the tool successfully generates a sufficient set of easily verifiable relative timing constraints. Moreover the generated constraint sets are the same size or smaller than that of the hand-optimized constraints.Keywords
This publication has 14 references indexed in Scilit:
- Verification of delayed-reset domino circuits using ATACSPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- RAPPID: an asynchronous instruction length decoderPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Relative timingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Circuit design techniques for a gigahertz integer microprocessorPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verification of speed-dependences in single-rail handshake circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal verification of safety properties in timed circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A theory of timed automataPublished by Elsevier ,2002
- Synthesizing Petri nets from state-based modelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1995
- Symbolic model checking for sequential circuit verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- Elementary transition systemsTheoretical Computer Science, 1992