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

fYear

1995

fDate

29 Aug-1 Sep 1995

Firstpage

567

Lastpage

573

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ASPDAC.1995.486371

Filename

486371