Next: Computer Industry Laboratory Up: Department of Computer Previous: Multimedia Devices Laboratory

Computer Education Laboratory


/ 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:


Refereed Journal Papers

  1. M. Kishinevsky, A. Kondratyev, and A. Taubin. Specification and analysis of self-timed circuits. Journal of VLSI Signal Processing, 7(1):117--135, 1994.

    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.

  2. M. Kishinevsky, A. Kondratyev, A. Taubin, and V. Varshavsky. Analysis and identification of speed-independent circuits on an event model. Formal Methods in System Design, 4(1):33--75, 1994.

    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

  1. Kondratyev A. and Taubin A. Verification of the speed-independent circuits by {STG} unfolding. In Proc. of the International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 64--75, Salt Lake City, Utah, November 1994. IEEE Computer Society, IEEE Computer Society Press.

    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.

  2. Kondratyev A., Taubin A., and Ten S. Verification of asynchronous circuits by petri net unfolding. In 1994 IEEE Symposium on Emerging Technologies & Factory Automation. Proceedings., pages 404--413. IEEE IES, IEEE Industrial Electronics Society, November 1994.

    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.

  3. Taubin A. Notes on the formal approach to totally self-checking property. In Ran Genosar, editor, 1995 Israel Workshop on Asynchronous VLSI., page 26. The Ministry of Science and the Arts, The Ministry of Science and the Arts, March 1995.

    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.

  4. Taubin A. Checking {STG} implementability for speed-independent circuits synthesis. In Ran Genosar, editor, 1995 Israel Workshop on Asynchronous VLSI, page 20. The Ministry of Science and the Arts, The Ministry of Science and the Arts, March 1995.

    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.

Books

  1. M. Kishinevsky, A. Kondratyev, A. Taubin, and V. Varshavsky. Concurrent Hardware, The Theory and Practice of Self-Timed Design. J. Wiley & Sons, New York, 1994.

Technical Reports

  1. A. Kondratyev and A. Taubin. On verification of the speed-independent circuits by stg unfoldings. 94-2-001, The University of Aizu, June 1994.

Academic Activities

  1. Alexander Taubin, IEEE, July 1994. Member.

  2. Alexander Taubin, ACM, August 1994. Member.



Next: Computer Industry Laboratory Up: Department of Computer Previous: Multimedia Devices Laboratory


www@u-aizu.ac.jp
January 1996