/ A. R. Taubin / Professor
The Computer Education Laboratory (the Laboratory name is suppose to be changed to the Design Automation Laboratory) together with the Computer Architecture Laboratory is participating in research on theoretical and applied problems of asynchronous and concurrent systems design.
The future growth of digital systems is made possible only by the development of sophisticated design automation (DA) tools. This requires the development of new efficient DA methods, especially essential for relatively new field of asynchronous design. The asynchronous and concurrent design is required an extensive formal methods and DA support that has been lacking up to now.
Development of DA is also of importance for training both engineers and students.
The basic apparatus for the asynchronous circuit study and design is a behavior model as far as semantically asynchronous properties can be defined in terms of behavior: through the causal relations between the switchings of the elements.
Formal models of concurrency especially Petri nets (PN) and Signal Transition Graphs (STG) as interpreted Petri nets are widely used for specification and design of asynchronous control circuits.
Petri nets unfoldings methods can be used at different stages of the design cycle.
The results of 1996 year laid the theoretical and practical basis to the development of model transformation and behavior-improving methods for the general type of Petri nets (PN) with choices (including unsafe case). This approach reduces the deadlock detection and deadlock prevention for PN and Signal Transition Graph (STG) to analysis of its unfolding on some simple formal properties and to transformation of the initial PN and therefore reduces time complexity.
1. Formal Models for Concurrent Hardware and Verification of Asynchronous System
In 1996 the deadlock prevention domain of application of the unfolding methods was explore.
A deadlock prevention procedure first detects deadlocks using an unfolding. Then, the first method reduces the unfolding to a set of deadlock-free sub-unfoldings that cover all live behaviors. The modified unfolding is further folded to a cyclic deadlock-free PN. The second method uses a direct transformation at the level of the original PN. This transformation is based on ordering relations between places and transitions in PN and inserts special ``switch" places and transitions to control choice that can lead to a deadlock situation.
The PN transformation based on unfolding could be useful for synthesis of asynchronous circuits, for functional testing of asynchronous circuits and for automatic test generation.
The effectiveness of the methods was proofed be the large set of benchmarks and real examples from asynchronous circuits benchmarks and from flexible and agile automation benchmarks.
2. CAD Development
The third step of UNIX-version of software was developed and tested on the set of benchmarks. Deadlock analysis and prevention by unfolding was most efficient for processes with high concurrency and low unsafeness.
New principles of the specification analysis and transformation (design methods by PN transformation using unfolding) allow to increase the analysis power for deadlock detection on 1-2 orders and provide deadlock free solutions.
Although the size of the unfolding can be exponential from the size of the initial Petri Net and the deadlock detection problem is known to be NP-complete the experimental results show that for highly parallel specifications a deadlock prevention by unfoldings is typically more efficient than a deadlock prevention based on symbolic BDD traversal of the corresponding reachability graph.
Refereed Proceeding Papers
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.
A model, called Place Chart Nets (PCN), is presented. It allows the modelling of both asynchronicity and exception handling (preemption). Contrary to State Charts and other reactive models, which are inherently synchronous, PCNs specify a system behavior using partial orders. Contrary to Petri nets, PCNs have a notion of hierarchy. Contrary to other hierarchical models based on Petri net extensions, the hierarchy in PCNs is determined by preemption. PCNs are a non-trivial generalization of classical PN. Then we present a method for synthesis of safe PCNs from transition systems, which generalizes the theory of regions previously developed for PNs.
Asynchronous circuits operate correctly only under timing assumptions that must be tested. Asynchronous nets/are a subclass in which feedback is allowed only inside/, sequential elements, and can be obtained from asynchronous circuits by partial scan. We show a reduction from delay fault testing of asynchronous nets to stuck-at testing on combinational circuits.
Unrefereed Papers