Synthesis of Reactive Systems: Application to Asynchronous Circuit Design

  • Josep Carmona
  • Jordi Cortadella
  • Enric Pastor
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2549)


Synthesis bridges the gap between specification and implementation by systematically transforming one model into another and approaching the primitives of the specification to those realizable by the implementation. This work faces the problem of the synthesis of reactive systems, in which there is an explicit distinction between input and output actions. The transformations used during synthesis must preserve the properties that characterize the correct interaction between the system and the environment. The concept of I/O compatibilty is proposed to define this correctness, and is used to provide a set of transformations for the synthesis of reactive systems. p] The theoretical contributions of the work are applied to the synthesis of asynchronous circuits. Petri nets are used as specification model, and a set of structural methods are proposed for the transformations of the model and the synthesis of digital circuits.


State Machine State Graph Input Event Excitation Region Boolean Equation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Arnold. Finite Transition Systems. Prentice Hall, 1994. 112Google Scholar
  2. [2]
    G. Berthelot. Checking Properties of Nets Using Transformations. In G. Rozenberg, editor, Advances in Petri Nets 1985, volume 222 of Lecture Notes in Computer Science, pages 19–40. Springer-Verlag, 1986. 121CrossRefGoogle Scholar
  3. [3]
    Janusz A. Brzozowski and Carl-Johan H. Seger. Asynchronous Circuits. Springer-Verlag, 1995. 126Google Scholar
  4. [4]
    J. Carmona and J. Cortadella. Input/Output Compatibility of Reactive Systems. In Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, Oregon, USA, November 2002. Springer-Verlag. 116Google Scholar
  5. [5]
    J. Carmona, J. Cortadella, and E. Pastor. A structural encoding technique for the synthesis of asynchronous circuits. In Int. Conf. on Application of Concurrency to System Design, June 2001. 141, 143Google Scholar
  6. [6]
    Tam-Anh Chu. Synthesis of Self-Timed VLSI Circuits from Graph-Theoretic Specifications. PhD thesis, MIT Laboratory for Computer Science, June 1987. 115, 131, 135Google Scholar
  7. [7]
    J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev. Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. IEICE Transactions on Information and Systems, E80–D(3):315–325, March 1997. 132, 146Google Scholar
  8. [8]
    J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev. Logic synthesis of asynchronous controllers and interfaces. Springer-Verlag, 2002. to appear. 130, 132Google Scholar
  9. [9]
    René David. Modular design of asynchronous circuits defined by graphs. IEEE Transactions on Computers, 26(8):727–737, August 1977. 141zbMATHCrossRefGoogle Scholar
  10. [10]
    M. Hack. Analysis of production schemata by Petri nets. M.s. thesis, MIT, February 1972. 115Google Scholar
  11. [11]
    D. Harel and A. Pnueli. On the development of reactive systems. In Krzystof R. Apt, editor, Logic and Model of Concurrent Systems, volume 13 of NATO ASI, pages 477–498. Springer-Verlag, October 1984. 112Google Scholar
  12. [12]
    Michael Kishinevsky, Alex Kondratyev, Alexander Taubin, and Victor Varshavsky. Concurrent Hardware: The Theory and Practice of Self-Timed Design. Series in Parallel Computing. John Wiley & Sons, 1994. 141Google Scholar
  13. [13]
    Alex Kondratyev and Alexander Taubin. Verification of speed-independent circuits by stg unfoldings. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 64–75, November 1994. 134Google Scholar
  14. [14]
    A. Kovalyov and J. Esparza. A polynomial algorithm to compute the concurrency relation of free-choice signal transition graphs. In Proceedings of the International Workshop on Discrete Event Systems, WODES’96, pages 1–6, August 1996. 115Google Scholar
  15. [15]
    A. V. Kovalyov. On complete reducibility of some classes of Petri nets. In Proceedings of the 11th International Conference on Applications and Theory of Petri Nets, pages 352–366, Paris, June 1990. 122Google Scholar
  16. [16]
    Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. In CWI-Quarterly, volume 2, pages 219–246, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, September 1989. 108Google Scholar
  17. [17]
    R. Milner. A Calculus for Communicating Processes, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980. 111, 116, 151Google Scholar
  18. [18]
    Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–574, April 1989. 109, 114, 122Google Scholar
  19. [19]
    Enric Pastor. Structural Methods for the Synthesis of Asynchronous Circuits from Signal Transition Graphs. PhD thesis, Universitat Polit`ecnia de Catalunya, February 1996. 133Google Scholar
  20. [20]
    Enric Pastor, Jordi Cortadella, Alex Kondratyev, and Oriol Roig. Structural methods for the synthesis of speed-independent circuits. IEEE Transactions on Computer-Aided Design, 17(11):1108–1129, November 1998. 133, 136CrossRefGoogle Scholar
  21. [21]
    C. A. Petri. Kommunikation mit Automaten. PhD thesis, Bonn, Institut für Instrumentelle Mathematik, 1962. (technical report Schriften des IIM Nr. 3). 114Google Scholar
  22. [22]
    L. Y. Rosenblum and A. V. Yakovlev. Signal graphs: from self-timed to timed ones. In Proceedings of International Workshop on Timed Petri Nets, pages 199–207, Torino, Italy, July 1985. IEEE Computer Society Press. 128Google Scholar
  23. [23]
    Manuel Silva, Enrique Teruel, and José Manuel Colom. Linear algebraic and linear programming techniques for the analysis of place/transition net systems. Lecture Notes in Computer Science: Lectures on Petri Nets I: Basic Models, 1491:309–373, 1998. 126Google Scholar
  24. [24]
    Victor I. Varshavsky, editor. Self-Timed Control of Concurrent Processes: The Design of Aperiodic Logical Circuits in Computers and Discrete Systems. Kluwer Academic Publishers, Dordrecht, The Netherlands, 1990. 141zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Josep Carmona
    • 1
  • Jordi Cortadella
    • 2
  • Enric Pastor
    • 1
  1. 1.Computer Architecture DepartmentUniversitat Politècnica de CatalunyaBarcelonaSpain
  2. 2.Software DepartmentUniversitat Politècnica de CatalunyaBarcelonaSpain

Personalised recommendations