Logic Synthesis Avoiding State Space Explosion (2003)

Author(s): Khomenko V, Koutny M, Yakovlev A

    Abstract: 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. Following the description of our method, we present some problem-specific optimization rules. 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.

      • Date: August 2003
      • Series Title: School of Computing Science Technical Report Series
      • Pages: 19
      • Institution: School of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

      Keywords: logic synthesis, asynchronous circuits, self-timed circuits, Petri nets, signal transition graphs, STG, SAT, net unfoldings, partial order techniques


      Dr Victor Khomenko
      Reader in Formal Methods

      Professor Maciej Koutny
      CS Director of Research

      Professor Alex Yakovlev
      Professor of Computer System Design