/ A. R. Taubin / Professor
The Computer Education Laboratory together with the Computer Architecture Laboratory is participating in research on theoretical and applied problems of asynchronous design, verification of asynchronous circuits and the automated method of their synthesis.
The basic apparatus for the self-timed circuit study and design is a behavior model as far as semantically self-timing can be defined in terms of behavior: through the causal relations between the switchings of the elements.
The results of 1995 year laid the theoretical and practical basis to the development of verification methods and algorithms for the general type of Petri nets (PN) with choices (including unsafe case). This approach reduces the analysis of PN and Signal Transition Graph (STG) to analysis of its unfolding on some simple formal properties and therefore reduces time complexity.
The analysis of the unfolding gives us a new possibility to transform the PN and to produced a correct specification from the incorrect one and to automatic design of correct Hardware or Software System (resynthesis).
Formal Models for Concurrent Hardware
Models for specification of concurrent processes (General PN). The unfoldings methods was developed for general case of Petri net model (General STG), new property and criteria were investigated. In 1995 a new domain of application of the unfolding methods was opened - Deadlock prevention. Two approach of deadlock prevention for Petri net was developed: by folding of modified unfolding and by direct transformation of the initial Petri net.
Verification of Asynchronous and Self-timed Systems
Verification of a formal specification against desired properties (Checking implementability).
The effectiveness of the new unfolding criteria were proofed be the large set of benchmarks and real examples.
CAD Development
The second step of UNIX-version of software was developed and tested on the set of benchmarks. As was expected the analysis by unfolding was most efficient for the processes with high concurrency and middle alternativity.
New principles of the specification analysis (design methods by event-based specifications) allow to increase the analysis power on 1-2 orders.
Graphical interface for STG verification software was implemented and tested. The result (unfolding, modified STG, etc.) became more observable.
Refereed Journal Papers
This paper suggests a way for Petri Net analysis by checking the ordering relations between places and transitions. The method is based on unfolding the original net into an equivalent acyclic description. We improved on the previously known cutoff criterion for truncating unfoldings. No restrictions are imposed on the class of general PNs. Circuit behavior is specified by an interpreted Petri net,called a Signal Transition Graph (STG) which is then analyzed for implementability by an asynchronous hazard-free circuit. The implementability conditions are formulated in such a way that they can be checked by analysis of ordering relations between signal transitions rather than by traversal of states. This allows us to avoid the state explosion problem for highly parallel specifications. The experimental results show that for highly parallel STGs checking their implementability by an unfolding is one to two orders of magnitude less time-consuming than checking it by symbolic BDD traversal of the corresponding State Graph.
The new criterion significantly reduces the size of an unfolding obtained by a PN. The properties of PNs for analysis can be various: boundedness, safety, persistency etc. A practical example of the suggested approach is given in an application to asynchronous design.
A deadlock prevention procedure first detects deadlocks using the unfolding, then reduces the unfolding to a deadlock-free sub-unfolding, and finally folds the deadlock-free acyclic net into a cyclic net. For the class of reinitialized processes which are very common for the manufacture systems the obtained cyclic net is live equivalent to the initial Petri Net. The live equivalence implies that each trace of the transformed net has an equivalent feasible trace in the initial net and all live (infinite) traces of the initial net are also present in the final net. As a side effect our method constructs ordering relations between places and transitions and checks boundedness, safety, persistency and hazards in the initial Petri Net specification.