A. Semenov
A. Yakovlev
University of Newcastle upon Tyne. 1994
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.