/ A. R. Taubin / Professor
We are interested in theoretical and applied problems of formal models development for asynchronous design, verification of asynchronous circuits and the automated method of their synthesis.
The problems of clock distribution, transparent scaling, modularity, and power management are becoming increasingly difficult to solve using the current synchronous design methodologies.
Asynchronous circuits, on the other hand, handle all such problems much more gracefully because each circuit component behaves as an independent computing agent that synchronizes with other elements only when and where required.
The basic apparatus for the self-timed circuit study and design is a behaviour model as far as semantically self-timing can be defined in terms of behaviour: through the causal relations between the switchings of the elements.
The choice of model representation 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.
For the last year a major tool of self-timed circuits behaviour specification has been event models, particularly change diagrams. Based on them the polynomial algorithms of verification were suggested.
Promising are researches connected with the development of descriptive possibilities and improvement of verification algorithms of this model, especially - decrease of computing complexity of analysis procedures, model improvement with description facilities of indeterministic behaviour, etc.
For the specification of circuits with external inputs and outputs the designer requires a means to express non-deterministic behaviour (choices). This is to reflect the lack of knowledge about the environment functioning. Until recently there have been no methods to deal with non-deterministic descriptions directly.
The latest results laid the basis to the development of verification methods for the general type of Signal Transition Graphs (STG) with choices. This approach reduces the analysis of STG to analysis of its unfolding on some simple formal properties. It promises to obtain the verification algorithms of polynomial complexity.
CAD support is the bottleneck of self-timed design. The asynchronous and self-timed design is strongly different from current methods of asynchronous design and is more complicated. Thus it requires an extensive CAD support that has been lacking up to now.
Development of CAD is also of importance for training both engineers and students.
The key topics are:
- CAD for self-timed and delay-insensitive circuits, devices and systems;
- theory of concurrency;
- fault-tolerant systems (self-checking circuits);
- logic design of asynchronous circuit.
The most interesting questions still open in asynchronous design are:
- decrease of computing complexity of analysis and synthesis procedures,
- model expansion with description tools for nondeterministic behaviour and high-level hardware description languages
We think, theoretical researches today can be effective only if they maintain an immediate link with real design of hardware systems and with development of appropriate software.
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.
Refereed Proceeding Papers
A model generalizing model of Change Diagrams (CD) is presented. The advantages of CDs over the other assembler-type languages suggest an idea of topping the CD-based foundation with a high-level language intended for self-timed circuits behavioral design. One of the main objectives of such a language is to offer a formal tool for behavioral specification of analysis and design of open circuits
The decomposition method of synthesis of speed-independent circuits from Signal Transition Graphs (STG) is suggested. This method does not generate a state graph corresponding to the STG-specification, i.e. a state explosion is avoided. The resulting circuit is derived by assembling circuits implementing projections of the initial STG on various groups of signals. Both the method and the resulting circuit is of linear complexity from the size of the initial STG. The main advantage of the decomposition method is that it automatically solves Unique State Coding problem.
The paper proposes a formal model named change diagram (CD), for analysis and synthesis of the very high speed complex VLSI circuits/systems The CD allows for unambiguous expression of concurrent activities not only of distributive processes, but also those of semi-modular. The equivalence of CDs and Petri Nets is investigated too. Possible usage of CDs in new generation simulators design is outlined
Books
Others
Participation in one-month joint research with University of Newcastle upon Tyne (UK) by The Royal Society invitation. The reports were made in University of Newcastle and in Oxford University