Detecting State Coding Conflicts in STG Unfoldings Using SAT

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), Unique State Coding (USC), or normalcy (a necessary condition for their implementability using gates without input invertors) requirements, e.g., by using model checking based on the reachability graph of an STG. 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. The model checking algorithm is derived by adopting the Boolean Satisfiability (SAT) approach. Following the basic formulation of the state coding conflict relationship, we pres...

• Type: Conference
• Year: 2003
• Where: ACSD
• Authors: Victor Khomenko, Maciej Koutny, Alexandre Yakovlev
• Keywords: ACSD 2003, Hardware, Model Checking, Reachability Graphs, Signal Transition Graphs