The accurate and efficient timing verification of interacting finite state machines.
Ajay J. Daga, William P. Birmingham · Deep Blue (University of Michigan) · 1995
There is a well recognized need for accurate timing verification tools. Such tools, however, are susceptible to an exponential increase in task complexity as circuit complexity increases. The viability of accurate timing verifiers hinges on their ability to efficiently analyze a small subset of circuit behaviors, while verifying timing characteristics of the overall space of behaviors. We address this issue for the timing verification of complex sequential circuits, modeled in terms of interacting finite state machines (FSMs). Accurate verification requires reasoning about the manner in which functional aspects of FSM behavior impact its temporal behavior. Toward this end, we present a model for the description of both functional and temporal aspects of FSM behavior, and theoretical results that allow the reduction of FSMs to a form that is minimal from a timing verification standpoint. We define a partition on the state-transition behavior of FSMs that allows their decomposition into multiple independent FSMs. This decomposed model of FSM behavior allows an efficient timing verification methodology, VITCh, that guarantees exact, and implicit, coverage of the space of circuit behaviors using symbolic simulation. Experimental results have demonstrated VITCh's utility in extracting delays through combinational logic and in verifying realistic board-level circuits, in a few seconds, while detecting subtle timing violations.