Timing analysis and verification of timed asynchronous circuits
Henrik Hulgaard · 1996
This dissertation develops a formal framework for the analysis of temporal properties of concurrent systems. A concurrent system is modeled as a set of independent concurrent components that occasionally synchronize. Formally, such a model is represented by a safe Petri net where the timing information is specified using delay ranges annotated on the places of the net. Petri nets have a simple representation of concurrency, synchronization, and state, and have proven adequate for modeling many types of control dominated concurrent systems. The analysis we perform is to determine the extreme case separation in time between two system events (transitions in the Petri net.) This analysis is useful both for performance evaluation and for timing verification. We apply the techniques developed in this dissertation to a particular domain, namely the analysis and verification of timed asynchronous circuits. This will allow designers to reason about, and thus synthesize, non-speed-independent or timed asynchronous circuits. Our hope is that these techniques can be used in a complete synthesis methodology for developing robust and high-performance timed designs. The timing analysis problem is approached in a bottom-up manner. We identify two subclasses of safe Petri nets for which we develop efficient and exact solutions. For a choice-free Petri net we develop an exact and efficient algorithm, called the sc TSE algorithm. This algorithm is extended to an iterative algorithm, called the sc CTSE algorithm, for analyzing Petri net specification with choice. If the choice is limited to extended free choice and unique choice, the sc CTSE algorithm is exact. If the choice is more general, the sc CTSE algorithm provides conservative bounds on the extreme case separation in times. The algorithms developed in this dissertation have been implemented in C++ and the practicality of the timing analysis is demonstrated by benchmarking the algorithms on a number of realistically sized applications. The sc CTSE algorithm is able to analyze Petri net specifications with more than 3000 nodes and 10$\sp{16}$ reachable states in less than two hours on a modern workstation.