Automated Verification of Asynchronous Circuits Using Circuit Petri Nets

To detect problematic circuit behaviour, such as potential hazards and deadlocks, in a reasonable amount of time a technique is required which would avoid exhaustive exploration of the state space of the system. Many of the existing methods rely on symbolic traversal of the state space, with the use of binary decision diagrams (BDDs) and associated software packages. This paper presents an alternative approach of using a special type of Petri nets to represent circuits. An algorithm for automatic conversion of a circuit netlist into a behaviourally equivalent Petri net is proposed. Once the circuit Petri net is constructed and composed with the provided environment specification, the presence and reachability of troublesome states is verified by using methods based on finite prefixes of Petri net unfoldings. The shortest trace leading to a deadlock or a hazard in the circuit Petri net is mapped back onto the gate-level representation of the circuit, thus assisting a designer in solving the problem. The method has been automated and compared against previously existing circuit verification tools.