/ 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 self-timed circuit study and design is a behavior model, with self-timing defined semantically in terms of behavior through causal relations between switchings of the elements.
Research being done in the laboratory includes:
Choosing the formal language of asynchronous behavioral description is a pivotal question. It is always a tradeoff between the desire to have the circuit specification as compact as possible and the aspiration to reach such a level of detail that would allow the designer to genuinely and comprehensively represent the semantics of parallelism, to analyze the correctness of the model, and to provide for the efficiency of realization of the desired behavior, i.e., of the circuits design according to the prescribed specification.
In the last few years, a major tool of self-timed circuit behavior specification has been event models, Change Diagrams and Signal Transition Graph (STG) in particular.
For the specification of circuits with external inputs and outputs, the designer requires a means to express non-deterministic behavior (choices). This is to reflect the lack of knowledge about environmental functioning. Until recently there have been no methods to deal with non-deterministic descriptions directly.
The results of research in 1994 laid the theoretical basis for the development of verification methods and algorithms for a general type of STG with choices. This approach reduces the analysis of STG to the analysis of its unfolding on some simple formal properties and, therefore, reduces time complexity.
For the purpose of verification (checking of STG implementability), only the finite prefix of the occurrence net was considered and in this the great compression in data was achieved.
Correctness criteria has been formulated in such a way that the circuit implemented by STG has speed-independence properties, i.e., behaves correctly in any distribution of gate delays.
Based on these criteria the polynomial algorithms of verification were suggested.
Asynchronous and self-timed design is significantly different from current methods of synchronous design and is more complicated. Thus, it requires an extensive CAD support that has been lacking up to now.
The development of CAD is also of importance for training both engineers and students.
This year, the first step of UNIX-version software was developed and tested on a set of benchmarks. As was expected, an analysis by unfolding was most efficient for processes with high concurrency.
New principles of specification analysis (design methods by event-based specifications) allow an increase in analysis power of 1-2 orders.
Refereed Journal Papers
Problems of self-timed behavior specification and verification are considered on the basis of event models. A new model, Change Diagrams (CD), based on two types of causal relations (AND, OR) is suggested. The notion of CD correctness is introduced and the necessity and sufficiency of this notion for the implementation to be in self-timed class is shown. The original approach for CD correctness verification is considered. The main advantage of the method is a simple (polynomial) algorithm of CD analysis.
The object of this paper is the analysis of asynchronous circuits for speed-independence or delay-insensitivity. The circuits are specified as a netlist of logic functions describing the components. The analysis is based on a derivation of an event specification of the circuit behavior in a form of a Signal Graph. Signal Graphs can be viewed either as a formalization of timing diagrams , or as a signal interpreted version of Marked Graphs (a subclass of Petri Nets). The main advantage of this method is that a state explosion is avoided. A restoration of an event specification of a circuit also helps to solve the behavior identification problem, i.e. to compare the obtained specification with the desired specification. We illustrate the method by means of some examples.
The idea of analysis is based on the STG unfolding into an acyclic graph. The improved method of unfolding is suggested. Based on this method the verification algorithms of STG analysis are developed. These algorithms are polynomial from the size of STG unfolding. Their efficiency is considered on the set of benchmarks.
In this paper we use the interpreted Petri Nets model for verification of asynchronous circuits. The main property in analysis is the speed-independence of a circuit. The analysis is based on the PN unfolding into an occurrence net. In terms of unfolding the necessary and sufficient conditions for correctness are formulated.
Totally self-checking circuits are considered. The notion of self-checking is based on a certain partition of the sets of input and output combinations into classes. The paper discusses the formal approach on verification the self-checking property for asynchronous circuits.
The method of analysis of implementability for general (with choices) class of speed-independent circuits is presented. The new principles of the specification analysis allow to increase the analysis power on 1-2 orders.
Technical Reports