/ A. R. Taubin / Professor
/ Dmitri A. Pospelov / Visiting Professor
The Computer Education 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 CAD tools. This requires the development of new efficient methods, especially essential for relatively new fields of asynchronous design and deep submicron technology (DSM).
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.
The technology of interest for research targeting at 10-15 years ahead is the one which is less than 100 nm. (deep submicron or DSM). It is now almost a common place to point out that for DSM noise immunity is becoming a metric of compatible importance to area, timing and power.
The results of 1997 year laid the theoretical and practical basis to the development of model transformation and behavior-improving methods for the Low noise asynchronous design.
Topics and Contents
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. In an unfolding the ordering relations can be determined directly by the structure of an underlying graph. We improved on the previously known cutoff criterion for truncating the unfolding. No restrictions are imposed on the class of general PNs. The new criterion significantly reduces the size of unfolding obtained by PN.
Petri nets are a powerful formalism for modeling concurrent systems. They are capable of implicitly describing a vast state space by a succinct representation which gracefully captures the notions of causality, concurrency and conflict between events. Petri nets have also been chosen by many authors as a formalism to describe the behavior of asynchronous circuits by interpreting the events as signal transitions, thus coining the term Signal Transition Graph. A design framework for asynchronous systems involves three main aspects: formal specification, verification and synthesis. In this paper we review the main techniques we have used to cover these aspects in recent years, with a special focus on asynchronous circuits.
Unfoldings of Petri Nets (PN) provide a method for analysis of concurrent systems without restoring the state space of a system. This allows one to overcome the ``state explosion'' problem while dealing with Petri Nets. Many properties of the initial PN (boundedness, safety, persistency and hazards) can be checked on-the-fly by constructing the unfolding. This paper presents techniques for deadlock prevention based on unfoldings of PN.
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. We present a method for synthesis of safe PCNs from transition systems, which generalizes the theory of regions previously developed for PCNs.
Hazard-free robust path delay fault testing (HFRPDFT) is a critical problem in asynchronous circuits that can insure correct and hazard-free operation only in the absence of delay faults (isocronic forks, negligible wire delays, bounded gate and wire delays, etc.). Asynchronous nets are circuits without clock signals composed from combinational gates and asynchronous latches (in this paper we consider only C-elements) such that feedbacks are allowed only inside latches. We reduced the problem of HFRPDFT for asynchronous nets to the classical problem of single stuck fault test generation for combinational logic. This yields an efficient algorithm for robust fault test generation of asynchronous circuits. We consider two testing schemes: a full output scan technique, simplified in comparison with the previously published results, for which each testable path can be tested with two vectors, and a partial scan -- for which applying testing pair must be preceded with an initialization phase. In the latter case a test can be a longer sequence of testing vectors. Experimental results illustrates the method.
Asynchronous circuits operate correctly only under timing assumptions. Hence testing those circuits for delay faults is crucial. Previous work has shown that full-scan delay-fault testing of asynchronous circuits is feasible. In this work we tackle the problem of partial scan testing, that requires test pattern generation on a sequential circuit. We show how this problem can be effectively reduced to a classical problem of stuck-at test pattern generation for a related combinational circuit. The technique is complete, automated, and requires only partial scan of some memory element outputs.
An unfolding is a finite acyclic prefix of a Petri Net behavior, which preserves all essential properties of the original Petri net, in particular all reachable markings of the net. An unfolding allows one to analyze partial orders between instances of places and events of the original net in a much simpler form due to absence of cycles. Cutoff criteria for truncating an infinite occurrence net into finite unfoldings are reviewed. We then show how unfoldings can be used for analysis of different properties of Petri Nets: boundedness, safety, persistency, deadlocks, etc. Signal Transition Graphs are interpreted Petri nets widely used for specification and design of asynchronous control circuits. We show how unfoldings can be used at different stages of the design cycle.
State coding conflict detection is a fundamental part of synthesis of asynchronous concurrent systems from their specifications as Signal Transition Graphs (STGs), which are a special kind of labelled Petri nets. The paper develops a method for identifying state coding conflicts in STGs that is intended to work within a new synthesis framework based on Petri net unfolding. The latter offers potential advantages due to a partial order representation of highly concurrent behaviour as opposed to the more traditional construction of a state graph, known to suffer from combinatorial explosion. We develop a necessary condition for coding conflicts to exist, by using an approximate state covering approach. Being computationally easy, yet conservative, such a solution may produce fake conflicts. A technique for refining the latter, with extra computational cost, is provided.
This paper introduces Lazy Transitions Systems (LzTSs). The notion of laziness explicitly distinguishes between the enabling and the firing of an event in a transition system. LzTSs can be effectively used to model the behavior of asynchronous circuits in which relative timing assumptions can be made on the occurrence of events. These assumptions can be derived from the information known a priori about the delay of the environment and the timing characteristics of the gates that will implement the circuit. The paper presents necessary conditions to synthesize circuits with a correct behavior under the given timing assumptions. Preliminary results show that significant area and performance improvements can be obtained by exploiting the extra ``don't care'' space implicitly provided by the laziness of the events.
Academic Activities