Affiliations: School of Computing Science, University of Newcastle
upon Tyne, NE1 7RU, United Kingdom. E-mail:
Victor.Khomenko,Maciej.Koutny@ncl.ac.uk | School of Electrical, Electronic and Computer
Engineering, University of Newcastle upon Tyne, NE1 7RU, United Kingdom.
E-mail: Alex.Yakovlev@ncl.ac.uk
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. 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.
Keywords: logic synthesis, automated synthesis, asynchronous circuits, self-timed circuits, Petrinets, signal transition graphs, STG, incremental SAT, net unfoldings, partial order techniques
