Logic Synthesis for Asynchronous Circuits Based on STG Unfoldings and Incremental SAT

• Autorzy: Khomenko V. , Koutny M. , Yakovlev A.
• Języki publikacji: EN

Abstrakty

EN

The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for logic synthesis based on the Incremental Boolean Satisfiability (SAT) approach. Experimental results show that this technique leads not only to huge memory savings when compared with the methods based on reachability graphs, but also to significant speedups in many cases, without affecting the quality of the solution.

Słowa kluczowe

EN

logic synthesis; automated synthesis; asynchronous circuitis; self-timed circuits; Petri net; Signal Transition Graphs (STGs); incremental SAT; net unfoldings; partial order techniques

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 1,2
• Strony: 49--73
• Opis fizyczny: tab., wykr., bibliogr. 33 poz.

Twórcy

autor

Khomenko V.

autor

Koutny M.

autor

Yakovlev A.

• School of Computing Science, University of Newcastle, Newcastle upon Tyne NE1 7RU, U.K.,

Bibliografia

• [1] Bryant, R.: Graph-Based Algorithms for Boolean FunctionManipulation, IEEE Transactions on Computers, C-35-8, 1986, 677-691.
• [2] Carrion, C., Yakovlev, A.: Design and Evaluation of Two Asynchronous Token Ring Adapters, Technical Report CS-TR-562, School of Computing Science, University of Newcastle upon Tyne, 1996.
• [3] Chu, T.-A.: Synthesis of Self-Timed VLSI Circuits from Graph-Theoretic Specifications, Ph.D. Thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, 1987.
• [4] Cortadella, J., Kishinevsky,M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Complete State Encoding Based on Theory of Regions, Proc. ASYNC'1996, IEEE Computer Society Press, 1996.
• [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), 1997, 315-325.
• [6] Cortadella, J., Kishinevsky,M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Logic Synthesis of Asynchronous Controllers and Interfaces, Springer-Verlag, 2002.
• [7] Engelfriet, J.: Branching Processes of Petri Nets, Acta Informatica, 28, 1991, 575-591.
• [8] Esparza, J.: Decidability and Complexity of Petri Net Problems-an Introduction, Lectures on Petri Nets I: Basic Models (W. Reisig, G. Rozenberg, Eds.), Lecture Notes in Computer Science 1491, Springer-Verlag, 1998.
• [9] Esparza, J., Römer, S., Vogler, W.: An Improvement of McMillan's Unfolding Algorithm, Formal Methods in System Design, 20(3), 2002, 285-310.
• [10] Furber, S., Efthymiou, A., Singh, M.: A Power-Efficient Duplex Communication System, Proc. AINT'2000 (A. Yakovlev, R. Nouta, Eds.), TU Delft, The Netherlands, 2000.
• [11] Heljanko, K.: Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets, Fundamenta Informaticae, 37(3), 1999, 247-268.
• [12] Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings, Ph.D. Thesis, School of Computing Science, University of Newcastle upon Tyne, 2003.
• [13] Khomenko, V., Koutny, M.: LP Deadlock Checking Using Partial Order Dependencies, Proc. CONCUR'2000 (C. Palamidessi, Ed.), Lecture Notes in Computer Science 1877, Springer-Verlag, 2000.
• [14] Khomenko, V., Koutny, M., Vogler, W.: Canonical Prefixes of Petri Net Unfoldings, Proc. CAV'2002 (E. Brinksma, K. Larsen, Eds.), Lecture Notes in Computer Science 2404, Springer-Verlag, 2002, Full version: Acta Informatica, 40(2), 2003, 95-118.
• [15] Khomenko, V., Koutny,M., Yakovlev, A.: Detecting State Coding Conflicts in STGs Using Integer Programming, Proc. DATE'2002 (C. Kloos, J. Franca, Eds.), IEEE Computer Society Press, 2002.
• [16] Khomenko, V., Koutny, M., Yakovlev, A.: Detecting State Coding Conflicts in STG Unfoldings Using SAT, Proc. ICACSD'2003 (J. Lilius, F. Balarin, R. Machado, Eds.), IEEE Computer Society Press, 2003, Full version: IOS Press, Fundamenta Informaticae, 62(2), 2004, 1-21.
• [17] Khomenko, V., Koutny,M., Yakovlev, A.: Logic Synthesis Avoiding State Space Explosion, Technical Report CS-TR-813, School of Computing Science, University of Newcastle upon Tyne, 2003.
• [18] Khomenko, V., Koutny,M., Yakovlev,A.: Logic Synthesis for AsynchronousCircuits Based on Petri Net Unfoldings and Incremental SAT, Proc. ICACSD'2004 (M. Kishinevsky, P. Darondeau, Eds.), IEEE Computer Society Press, 2004.
• [19] Kondratyev, A., Cortadella, J., Kishinevsky, M., Lavagno, L., Taubin, A., Yakovlev, A.: Identifying State Coding Conflicts in Asynchronous System Specifications Using Petri Net Unfoldings, Proc. ICACSD'1998, IEEE Computer Society Press, 1998.
• [20] Kondratyev, A., Cortadella, J., Kishinevsky, M., Pastor, E., Roig, O., Yakovlev, A.: Checking Signal Transition Graph Implementability by Symbolic BDD Traversal, Proc. DATE'1995, IEEE Computer Society Press, 1995.
• [21] Low, K., Yakovlev, A.: Token Ring Arbiters: an Exercise in Asynchronous Logic Design with Petri Nets, Technical Report CS-TR-537, School of Computing Science, University of Newcastle upon Tyne, 1995.
• [22] Madalinski, A., Bystrov, A., Khomenko, V., Yakovlev, A.: Visualization and Resolution of Coding Conflicts in Asynchronous Circuit Design, Proc. DATE'2003, IEEE Computer Society Press, 2003, Full version: IEE Proceedings: Computers & Digital Techniques 150(5), 2003, 285-293.
• [23] McMillan, K.: SymbolicModel Checking: an Approach to the State Explosion Problem, Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, 1992.
• [24] McMillan, K.: Using Unfoldings to Avoid State Explosion Problem in the Verification of Asynchronous Circuits, Proc. CAV'1992, Lecture Notes in Computer Science 663, Springer-Verlag, 1992.
• [25] McMillan, K.: A Technique of State Space Search Based on Unfoldings, Formal Methods in System Design, 6(1), 1995, 45-65.
• [26] Moskewicz, S., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: CHAFF: Engineering an Efficient SAT Solver, Proc. DAC'2001, ASME Technical Publishing, 2001.
• [27] Pastor, E., Cortadella, J., Roig, O.: Symbolic Analysis of Bounded Petri Nets, IEEE Transactions on Computers, 50(5), 2001, 432-448.
• [28] Semenov, A.: Verification and Synthesis of Asynchronous Control Circuits Using Petri Net Unfolding, Ph.D. Thesis, School of Computing Science, University of Newcastle upon Tyne, 1997.
• [29] Semenov, A., Yakovlev, A., Pastor, E., Pe˜na, M., Cortadella, J., Lavagno, L.: Partial Order Approach to Synthesis of Speed-Independent Circuits, Proc. ASYNC'1997, IEEE Computer Society Press, 1997.
• [30] Vanbekbergen, P., Catthoor, F., Goossens, G., De Man, H.: Optimized Synthesis of Asynchronous Control Circuits from Graph-Theoretic Specifications, Proc. ICCAD'1990, IEEE Computer Society Press, 1990.
• [31] Yakovlev, A.: Designing Control Logic for Counterflow Pipeline Processor Using Petri nets, FormalMethods in System Design, 12(1), 1998, 39-71.
• [32] Yakovlev, A., Lavagno, L., Sangiovanni-Vincentelli, A.: A Unified Signal Transition Graph Model for Asynchronous Control Circuit Synthesis, Formal Methods in System Design, 9(3), 1996, 139-188.
• [33] Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers, Proc. CAV'2002 (E. Brinksma, K. Larsen, Eds.), Lecture Notes in Computer Science 2404, Springer-Verlag, 2002.