Affiliations: School of Computing Science, University of Newcastle
upon Tyne, NE1 7RU, United Kingdom | School of Electrical, Electronic and Computer
Engineering, University of Newcastle upon Tyne NE1 7RU, United Kongdom
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 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.
Keywords: asynchronous circuits, automated synthesis, complete state coding, CSC, Petri nets, signal transition graphs, STG, SAT, net unfoldings, partial order techniques
