Detecting State Encoding Conflicts in STG Unfoldings Using SAT

• Autorzy: Khomenko V. , Koutny M. , Yakovlev A.
• Konferencja: Third International Conference on Application of Concurrency to System Design (ACSD'03) (18-20 June, 2003, Guimaraes, Portugal)
• 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 that of identifying whether an STG satisfies the Complete State Coding (CSC) requirement (which states that semantically different reachable states must have different binary encodings), and, if necessary, modifying the STG (by, e.g., inserting new signals helping to trace the current state) to meet this requirement. 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 detection of CSC conflicts based on the Boolean Satisfiability (SAT) approach. Following the basic formulation of the state encoding conflict relationship, we present some problem-specific optimization rules. Experimental results show that this technique leads not only to huge memory savings when compared to the CSC conflicts detection methods based on reachability graphs, but also to significant speedups in many cases.

Słowa kluczowe

EN

asynchronous circuitis; automated synthesis; Complete State Coding; Petri net; Signal Transition Graphs; STGs; net unfoldings; partial order techniques

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 62, nr 2
• Strony: 221--241
• Opis fizyczny: Bibliogr. 38 poz., tab., wykr.

Twórcy

autor

Khomenko V.

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

autor

Koutny M.

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

autor

Yakovlev A.

• School of Electrical, Electronic and Computer Engineering, University of Newcastle, upon Tyne NEl 7RU, United Kingdom

Bibliografia

• [11 Bryant, R.: Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, C-35-8, 1986, 677-691.
• [2] Carmona, J.; Structural Methods for the Synthesis of Wei I-Formed Concurrent Specifications, Ph.D. Thesis, Universitat Pohtècnica de Catalunya (UPC), 2004.
• [3] Carrion. C. Yakovlev. A.: Design and Evaluation of Two Asynchronous Token Ring Adapters, Technical Report CS-TR-562, Department of Computing Science, University of Newcastle upon Tyne, 1996.
• [41 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.
• [5] 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.
• [6] Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: PETRIFY: a Tool tor Manipulating Concurrent Specifications and Synthesis of Asynchronous Controllers, lEICE Transactions on information and Systems, E80-D(3), 1997, 315-325.
• [7] Cortadella. J., Kishinevsky. M., Kondratyev, A., Lavagno, L., Yakoviev, A.: Logic Synthesis of Asynchronous Controllers and Interfaces. Springer-Verlag, 2002.
• [8] Engelfriet, J.: Branching Processes of Petri Nets, Acta Informatica, 28. 1991. 575-591.
• [9] 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.
• [10] Esparza, J., Romer, S., Vogler, W.: An Improvement of McMillan's Unfolding Algorithm, Formal Methods in System Design, 20(3). 2002, 285-310.
• [11] 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.
• [12] Furber, S., Garside, J., Gilbert, D.: AMULET-3: A High-Performance Self-Timed ARM Microprocessor, Proc. ICCD-1998, 1998.
• [13] Gu, J., Puri, R.: Asynchronous Circuit Synthesis with Boolean Satisfiability, IEEE Transactions on Computer-Aided Design of Integrated Circuits, 14(8), 1995. 961-973.
• [14] 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.
• [15] 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.
• [16] 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.
• [17] 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.
• [18] Kishinevsky, M., Kondratyev, A., Taubin, A., Varshavsky, V: Concurrent Hardware: The Theory and Practice of Self-Timed Design, Series in Parallel Compufing, John Wiley & Sons, Inc., New York. USA, 1994.
• [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] Lin, B., Ykman-Couvreur, C. Vanbekbergen. P.: A General State Graph Transformation Framework for Asynchronous Synthesis. Proc. EURO-DAC1994, IEEE Computer Society Press. 1994.
• [22] Lin, K.-J., Kuo, J.-W., Lin. C.-S.: Direct Synthesis of Hazard-Free Asynchronous Circuits from STGs Based on Lock Relation and MG-Decomposition Approach, Proc. of EDTC'1994, IEEE Computer Society Press, 1994.
• [23] Lin, K.-J., Kuo. J.-W., Lin, C.-S.: Synthesis of Hazard-Free Asynchronous Circuits Based on Characteristic Graph, IEEE Transactions on Computers, 46(11), 1997, 1246-1263.
• [24] Low, K., Yakovlev. A.: Token Ring Arbiters: an Exercise in Asynchronous Logic Design with Petri Nets, Technical Report CS-TR-537, Department of Computing Science, University of Newcastle upon Tyne, 1995.
• [25] Madalinski, A.: CONFRES: Interactive Coding Conflict Resolver Based on Core Visualization, Proc. ICACSD '2003, IEEE Computer Society Press, 2003.
• [26] 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: Special Issue on Best Papers from DATE'2003, IEE Proceedings: Computers & Digital Techniques 150(5) (2003) 285-293.
• [27] McMillan. K.: Symbolic Model Checking: an Approach to the State Explosion Problem, Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, 1992.
• [28] McMillan. K.: A Technique of State Space Search Based on Unfoldings, Formal Methods in System Design, 6(1), 1995,45-65.
• [29] Moskewicz, S., Madigan, C, Zhao, Y, Zhang. L., Malik, S.: CHAFF: Engineering an Efficient SAT Solver, Proc. DAC'2001, ACM Technical Publishing. 2001.
• [30] Pastor, E., Cortadella, J.: Polynomial Algorithms for the Synthesis of Hazard-free Circuits from Signal Transition Graphs, Proc. of ICCAD'1993, IEEE Computer Society Press, 1993.
• [31] Pastor, E., Cortadella, J., Roig, O.: Symbolic Analysis of Bounded Petri Nets, IEEE Transactions on Computers, 50(5), 2001, 432-448.
• [32] Semenov, A.: Verification and Synthesis of Asynchronous Control Circuits Using Petri Net Unfolding, Ph.D. Thesis, Department of Computing Science, University of Newcastle upon Tyne, 1997.
• [33] Semenov, A., Yakovlev, A., Pastor, E., Pefla, M., Cortadella, J., Lavagno, L.: Partial Order Approach to Synthesis of Speed-Independent Circuits, Proc. ASYNC'1997, IEEE Computer Society Press, 1997.
• [34] Vanbekbergen, P., Catthoor, R, Goossens. G., De Man, H.: Optimized Synthesis of Asynchronous Control Circuits from Graph-Theoretic Specifications, Proc. ICCAD'J990. IEEE Computer Society Press, 1990.
• [35] Yakovlev, A.: Designing Control Logic for Counterflow Pipeline Processor Using Petri nets, Formal Methods in System Design, 12(1), 1998,39-71.
• [36] 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.
• [37] Yakovlev, A., Petrov, A.: Petri Nets and Parallel Bus Controller Design, Proc. of ICATPN'J990, 1990.
• [38] 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.