Title :
Combining partial orders and symbolic traversal for efficient verification of asynchronous circuits
Author :
Semenov, Alexei ; Yakovlev, Alexandre
Author_Institution :
Dept. of Comput. Sci., Newcastle upon Tyne Univ., UK
fDate :
29 Aug-1 Sep 1995
Abstract :
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. The results of unfolding construction are used 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
Keywords :
Petri nets; asynchronous circuits; formal verification; logic testing; pipeline processing; BDD variables; BDD-based traversal; Petri net unfolding; Petri net verification; asynchronous circuits; asynchronous microprocessor; close-to-optimal ordering; efficient verification; partial orders; symbolic traversal; unfolding construction; Asynchronous circuits; Benchmark testing; Binary decision diagrams; Boolean functions; Circuit testing; Data structures; Microprocessors; Petri nets; State-space methods; Tree graphs;
Conference_Titel :
Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL '95/VLSI '95., IFIP International Conference on Hardware Description Languages. IFIP International Conference on Very Large Scal
Conference_Location :
Chiba
Print_ISBN :
4-930813-67-0
DOI :
10.1109/ASPDAC.1995.486371
