A New Specification Model for Timing constraints and Efficient Methods for their Verification (thesis)

Abstract:

Correct timing is a critical issue in hardware design, especially in the case of asynchronous systems such as buses. As a result timing verification becomes an important ingredient of the circuit analysis problem. Furthermore, given the non-trivial timing constraints characterizing the temporal behavior of interface
circuits, it is clear that the problem of timing verification is tightly bound to the problem of temporal behavior specification. In this dissertation we present a new specication model which significantly extends the type of constraints which can be expressed. The model is based on dependency graphs
and vectors of signal values over time. The timing constraints are verified using a new verification methodology based on "event graphs". Our verification method is to compare the intended circuit behavior, described in our specification model, with the behavior of the implemented circuit. In order
to obtain the behavior of the implemented circuit we use an event driven simulation approach. The implemented behavior of the circuit is derived in the form of an "event graph." To avoid the penalty of an exhaustive simulation, an extended value system is used. The specification model and the event graph verification methodology are integrated into a new timing verification tool: CLOVER. CLOVER provides the designer of a digital circuit with an integrated environment where he can describe his design, formally specify the timing constraints governing the implementation, obtain the timing behavior of the
implemented design and verify it against the stated timing constraints. Although the current system does not allow hierarchical verification, the problem of designing a good hierarchical verification methodology is also addressed in this dissertation. CLOVER has been used for the analysis and verification of two interface circuits: the Multibus Design Frame and the SPUR PCC-to-SPC interface. We present a summary of the results for these circuits.