Circuit based quantification: back to state set manipulation within unbounded model checking

Author

Cabodi, Gianpiero ; Crivellari, Marco ; Nocco, Sergio ; Quer, Stefano

Author_Institution

Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy

fYear

2005

fDate

7-11 March 2005

Firstpage

688

Abstract

A non-canonical circuit-based state set representation is used to perform quantifier elimination efficiently. The novelty of this approach lies in adapting equivalence checking and logic synthesis techniques to the goal of compacting circuit based state set representations resulting from existential quantification. The method can be efficiently combined with other verification approaches such as inductive and SAT-based pre-image verifications.

Keywords

computability; logic circuits; logic design; set theory; AND inverted graphs; Boolean circuit; SAT-based pre-image verifications; circuit based quantification; equivalence checking; existential quantification; inductive verification; logic synthesis; noncanonical state set representations; quantifier elimination; unbounded model checking; Binary decision diagrams; Boolean functions; Circuit synthesis; Combinational circuits; Data structures; Databases; Explosions; Logic circuits; Merging; Switches;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation and Test in Europe, 2005. Proceedings

ISSN

1530-1591

Print_ISBN

0-7695-2288-2

Type

conf

DOI

10.1109/DATE.2005.93

Filename

1395656

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2589136