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 | 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.
https://hdl.handle.net/11583/1858565
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo