This paper describes optimized techniques to efficiently compute and reap benefits from inductive invariants within SAT-based model checking. We address sequential circuit verification, and we consider both equivalences and implications between pairs of nodes in the logic networks. First, we present a very efficient dynamic procedure, based on equivalence classes and incremental SAT, specifically oriented to reduce the set of checked invariants. Then, we show how to effectively integrate the computation of inductive invariants within state-of-the-art SAT-based model checking procedures. Experiments (on more than 600 designs) show the robustness of our approach on verification instances on which stand-alone techniques fail.

Strengthening Model Checking Techniques with Inductive Invariants / Cabodi, Gianpiero; Nocco, Sergio; Quer, Stefano. - In: IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS. - ISSN 0278-0070. - 28:(2009), pp. 154-158.

Strengthening Model Checking Techniques with Inductive Invariants

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

Abstract

This paper describes optimized techniques to efficiently compute and reap benefits from inductive invariants within SAT-based model checking. We address sequential circuit verification, and we consider both equivalences and implications between pairs of nodes in the logic networks. First, we present a very efficient dynamic procedure, based on equivalence classes and incremental SAT, specifically oriented to reduce the set of checked invariants. Then, we show how to effectively integrate the computation of inductive invariants within state-of-the-art SAT-based model checking procedures. Experiments (on more than 600 designs) show the robustness of our approach on verification instances on which stand-alone techniques fail.
File in questo prodotto:
File Dimensione Formato  
riv09-01.pdf

accesso aperto

Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 192.83 kB
Formato Adobe PDF
192.83 kB Adobe PDF Visualizza/Apri
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/1858565
 Attenzione

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