Application of linearly transformed BDDs in sequential verification

Author

Gunther, Wolfgang ; Hett, Andreas ; Becker, Bernd

Author_Institution

Inst. of Comput. Sci., Albert-Ludwigs-Univ., Freiburg, Germany

fYear

2001

fDate

2001

Firstpage

91

Lastpage

96

Abstract

The computation of the set of reachable states is the key problem of many applications in sequential verification. Binary Decision Diagrams (BDDs) are extensively used in this domain, but tend to blow up for larger instances. To increase the computational power of BDDs, linearly transformed BDDs (LTBDDs) have been proposed. In this paper we show how this concept can be incorporated into the sequential verification domain by restricting dynamic reordering in such a way that the relational product can still be carried out efficiently. Experimental results are given to show the efficiency of our approach

Keywords

binary decision diagrams; finite state machines; formal verification; logic CAD; reachability analysis; sequential circuits; binary decision diagrams; computational power; dynamic reordering; linearly transformed BDDs; reachable states; relational product; sequential verification; sequential verification domain; Application software; Automata; Boolean functions; Computer science; Data structures; Formal verification; Minimization; Polynomials; Reachability analysis; Sequential circuits;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 2001. Proceedings of the ASP-DAC 2001. Asia and South Pacific

Conference_Location

Yokohama

Print_ISBN

0-7803-6633-6

Type

conf

DOI

10.1109/ASPDAC.2001.913286

Filename

913286