Component refinement and CSC-solving for STG decomposition. (English) Zbl 1143.68055
Summary: STGs (Signal Transition Graphs) give a formalism for the description of asynchronous circuits based on Petri nets. To overcome the state explosion problem one may encounter during circuit synthesis, a nondeterministic algorithm for decomposing STGs was suggested by Chu and improved by one of the present authors.
Here we study how CSC-solving-which is essential for circuit synthesis-can be combined with decomposition. For this purpose, the correctness definition for decomposition is enhanced with internal signals and hierarchical decomposition is proven correct. Based on this, it is shown that speed-independent CSC-solving preserves correctness and can be combined with decomposition.
Furthermore, we use our new correctness definition to give the first correctness proof for the decomposition method of Carmona and Cortadella. Finally, we compare three different implementation relations for STGs: one derived from our correctness definition; one defined by Dill based on trace structures; and one derived from I/O-compatibility defined by Carmona and Cortadella.
Here we study how CSC-solving-which is essential for circuit synthesis-can be combined with decomposition. For this purpose, the correctness definition for decomposition is enhanced with internal signals and hierarchical decomposition is proven correct. Based on this, it is shown that speed-independent CSC-solving preserves correctness and can be combined with decomposition.
Furthermore, we use our new correctness definition to give the first correctness proof for the decomposition method of Carmona and Cortadella. Finally, we compare three different implementation relations for STGs: one derived from our correctness definition; one defined by Dill based on trace structures; and one derived from I/O-compatibility defined by Carmona and Cortadella.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Software:
PetrifyReferences:
| [1] | Josep Carmona, Structural methods for the synthesis of well-formed concurrent specifications, Ph.D. Thesis, Universitat Politècnica de Catalunya, 2003; Josep Carmona, Structural methods for the synthesis of well-formed concurrent specifications, Ph.D. Thesis, Universitat Politècnica de Catalunya, 2003 |
| [2] | Carmona, J.; Cortadella, J., Input/output compatibility of reactive systems, (Formal Methods in Computer-Aided Design. Formal Methods in Computer-Aided Design, FMCAD 2002, Portland, USA. Formal Methods in Computer-Aided Design. Formal Methods in Computer-Aided Design, FMCAD 2002, Portland, USA, Lect. Notes Comp. Sci., vol. 2517 (2002), Springer), 360-377 · Zbl 1019.68616 |
| [3] | J. Carmona, J. Cortadella, ILP models for the synthesis of asynchronous control circuits, in: Proc. of the IEEE/ACM International Conference on Computer Aided Design, 2003, pp. 818-825; J. Carmona, J. Cortadella, ILP models for the synthesis of asynchronous control circuits, in: Proc. of the IEEE/ACM International Conference on Computer Aided Design, 2003, pp. 818-825 |
| [4] | T.-A. Chu, Synthesis of self-timed VLSI circuits from graph-theoretic specifications, in: IEEE Int. Conf. Computer Design ICCD ’87, 1987, pp. 220-223; T.-A. Chu, Synthesis of self-timed VLSI circuits from graph-theoretic specifications, in: IEEE Int. Conf. Computer Design ICCD ’87, 1987, pp. 220-223 |
| [5] | Cortadella, J.; Kishinevsky, M.; Kondratyev, A.; Lavagno, L.; Yakovlev, A., Petrify: A tool for manipulating concurrent specifications and synthesis of asynchronous controllers, IEICE Transactions on Information and Systems, E80-D, 3, 315-325 (1997) |
| [6] | Cortadella, J.; Kishinevsky, M.; Kondratyev, A.; Lavagno, L.; Yakovlev, A., Logic Synthesis of Asynchronous Controllers and Interfaces (2002), Springer · Zbl 1013.68273 |
| [7] | Dill, D., Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits (1988), MIT Press: MIT Press Cambridge |
| [8] | Ebergen, J., Arbiters: An exercise in specifying and decomposing asynchronously communicating components, Science of Computer Programming, 18, 223-245 (1992) · Zbl 0769.68004 |
| [9] | F. Garc-Vall, J.M. Colom, Structural analysis of signal transition graphs, in: Petri Nets in System Engineering, 1997; F. Garc-Vall, J.M. Colom, Structural analysis of signal transition graphs, in: Petri Nets in System Engineering, 1997 |
| [10] | A. Kondratyev, M. Kishinevsky, A. Taubin, Synthesis method in self-timed design. Decompositional approach, in: IEEE Int. Conf. VLSI and CAD, 1993, pp. 324-327; A. Kondratyev, M. Kishinevsky, A. Taubin, Synthesis method in self-timed design. Decompositional approach, in: IEEE Int. Conf. VLSI and CAD, 1993, pp. 324-327 |
| [11] | V. Khomenko, M. Koutny, A. Yakovlev, Logic synthesis for asynchronous circuits based on Petri net unfoldings and incremental sat, in: M. Canada Kishinevsky, Ph. Darondeau (Eds.), ACSD 2004, 2004, pp. 16-25; V. Khomenko, M. Koutny, A. Yakovlev, Logic synthesis for asynchronous circuits based on Petri net unfoldings and incremental sat, in: M. Canada Kishinevsky, Ph. Darondeau (Eds.), ACSD 2004, 2004, pp. 16-25 |
| [12] | Muller, D. E.; Bartky, W. S., A theory of asynchronous circuits, (Proceedings of an International Symposium on the Theory of Switching (1959), Harvard University Press), 204-243 · Zbl 0171.37902 |
| [13] | Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008 |
| [14] | M. Schaefer, W. Vogler, R. Wollowski, V. Khomenko, Strategies for optimised STG decomposition. in: Proc. ACSD’06, 2006; M. Schaefer, W. Vogler, R. Wollowski, V. Khomenko, Strategies for optimised STG decomposition. in: Proc. ACSD’06, 2006 · Zbl 1183.68125 |
| [15] | Vogler, W.; Kangsah, B., Improved decomposition of signal transition graphs, Fundamenta Informaticae, 76, 161-197 (2006) · Zbl 1138.68472 |
| [16] | Vogler, W.; Wollowski, R., Decomposition in asynchronous circuit design, (Cortadella, J.; etal., Concurrency and Hardware Design. Concurrency and Hardware Design, Lect. Notes Comp. Sci., vol. 2549 (2002), Springer), 152-190 · Zbl 1029.68006 |
| [17] | Yakovlev, A.; Kishinevsky, M.; Kondratyev, A.; Lavagno, L.; Pietkiewicz-Koutny, M., On the models for asynchronous circuit behaviour with or causality, Formal Methods in System Design, 9, 189-233 (1996) |
| [18] | T. Yoneda, H. Onda, C. Myers, Synthesis of speed independent circuits based on decomposition, in: ASYNC 2004, 2004, pp. 135-145; T. Yoneda, H. Onda, C. Myers, Synthesis of speed independent circuits based on decomposition, in: ASYNC 2004, 2004, pp. 135-145 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
