Combining Partial Orders and Symbolic Traversal for Eficient Verification of Asynchronous Circuits (1995)

Author(s): Semenov A, Yakovlev A

    Abstract: Petri nets (PNs) are most adequate for the modelling of the event-triggered behaviour of asynchronous circuits, whose correctness is primarily concerned with freedom from hazards and dead-locks. A recently proposed method for the verification of Petri nets is based on implicit symbolic traversal of the net markings, which often yields better performance than using standard reachability graph analysis. It employs a Binary Decision Diagram (BDD) representation of the boolean functions characterising the state space of the model. This method may however suffer from the problem of a bad ordering of the BDD variables. In this paper, we propose an algorithm combining two approaches to PN verification: PN unfolding and BDD-based traversal. We introduce a new application of the PN unfolding method. It acts as a pre-processor for obtaining the close to optimal ordering of BDD variables. The effect of this combination is demonstrated on a set of benchmarks. The overall framework has been used for the verification of circuits in an asynchronous microprocessor.

      • Date: 1995
      • Series Title: Department of Computing Science Technical Report Series
      • Pages: 17
      • Institution: Department of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

      Keywords: asynchronous circuit design, bounded petri net, labelled petri net, signal transition graph, unfolding

      Staff

      Professor Alex Yakovlev
      Professor of Computer System Design