In this paper, we propose a methodology to make Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) Solvers cooperate. The underlying idea is simple: We start a verification task with BDDs, we go on with them as long as the problem remains of manageable size, then we switch to SAT, without losing the work done on the BDD domain. We propose target enlargement as an attempt to bring some of the advantages of state set manipulation from BDDs to SAT-based verification. We first, "enlarge" initial and target state sets of a given verification problem by affordable BDD manipulations. This step is carried on with a few breadth-first steps of traversal, or with what we call high-density dynamic abstraction, i.e., a new technique to collect under-approximate reachable state sets. Then, we perform SAT-based verification with the newly computed "enlarged" sets. We experimentally test our methodology within an industrial environment, the Intel BOolean VErifier BOVE. Preliminary results on standard benchmarks (the ISCAS'89, ISCAS'89--addendum, and VIS suites), and industrial ones (the IBM Formal Verification Benchmark Library) are provided. Results show interesting improvements over state-of-the-art techniques: We could decrease CPU time up to a 5x factor, when performing verification with the same depth, or we could increase the verification depth up to 30%, when performing verification within the same time limit.

Exploiting Target Enlargement and Dynamic Abstraction within Mixed BDD and SAT Invariant Checking / Cabodi, Gianpiero; Brace, K. S.; Bischoff, G. P.; Nocco, Sergio; Quer, Stefano. - STAMPA. - (2004). (Intervento presentato al convegno Second International Workshop on Bounded Model Checking (BMC 2003) tenutosi a Boston, Massachusetts, USA nel July, 2004).

Exploiting Target Enlargement and Dynamic Abstraction within Mixed BDD and SAT Invariant Checking

CABODI, Gianpiero;NOCCO, SERGIO;QUER, Stefano
2004

Abstract

In this paper, we propose a methodology to make Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) Solvers cooperate. The underlying idea is simple: We start a verification task with BDDs, we go on with them as long as the problem remains of manageable size, then we switch to SAT, without losing the work done on the BDD domain. We propose target enlargement as an attempt to bring some of the advantages of state set manipulation from BDDs to SAT-based verification. We first, "enlarge" initial and target state sets of a given verification problem by affordable BDD manipulations. This step is carried on with a few breadth-first steps of traversal, or with what we call high-density dynamic abstraction, i.e., a new technique to collect under-approximate reachable state sets. Then, we perform SAT-based verification with the newly computed "enlarged" sets. We experimentally test our methodology within an industrial environment, the Intel BOolean VErifier BOVE. Preliminary results on standard benchmarks (the ISCAS'89, ISCAS'89--addendum, and VIS suites), and industrial ones (the IBM Formal Verification Benchmark Library) are provided. Results show interesting improvements over state-of-the-art techniques: We could decrease CPU time up to a 5x factor, when performing verification with the same depth, or we could increase the verification depth up to 30%, when performing verification within the same time limit.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2654254
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo