Automated Verification of Asynchronous Circuits Using Circuit Petri Nets (2008)

Author(s): Poliakov I, Mokhov A, Rafiev A, Sokolov D, Yakovlev A

    Abstract: 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.

      • Date: 7-11 April 2008
      • Conference Name: 14th IEEE International Symposium on Asynchronous Circuits and Systems
      • Pages: 161-170
      • Publisher: IEEE Computer Society Press
      • Publication type: Conference Proceedings (inc. abstract)
      • Bibliographic status: Published
      Staff

      Professor Alex Yakovlev
      Professor of Computer System Design