tutorial

Formal verification at higher levels of abstraction

Authors:

Daniel Kroening,

Sanjit A. SeshiaAuthors Info & Claims

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

Pages 572 - 578

Published: 05 November 2007 Publication History

Abstract

Most formal verification tools on the market convert a high-level register transfer level (RTL) design into a bit-level model. Algorithms that operate at the bit-level are unable to exploit the structure provided by the higher abstraction levels, and thus, are less scalable.

This tutorial surveys recent advances in formal verification using high-level models. We present word-level verification with predicate abstraction and satisfiability modulo theories (SMT) solvers. We then describe techniques for term-level modeling and ways to combine word-level and term-level approaches for scalable verification.

References

[1]

Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah. Refinement strategies for verification methods based on datapath abstraction. In Asia South Pacific Design Automation Conference (ASP-DAC), pages 19--24, 2006.

Digital Library

[2]

Z. S. Andraus and K. A. Sakallah. Automatic abstraction and verification of Verilog models. In Design Automation Conference (DAC), pages 218--223. ACM Press, 2004.

Digital Library

[3]

D. Babić and M. Musuvathi. Modular Arithmetic Decision Procedure. Technical report, Microsoft Research, Redmond, 2005.

[4]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN Workshop, pages 103--122, 2001.

Digital Library

[5]

C. W. Barrett, D. L. Dill, and J. R. Levitt. A decision procedure for bit-vector arithmetic. In Design Automation Conference (DAC), pages 522--527. ACM Press, 1998.

Digital Library

[6]

S. Berezin, V. Ganesh, and D. Dill. A decision procedure for fixed-width bit-vectors. Technical report, Computer Science Department, Stanford University, April 2005.

[7]

A. Biere, A. Cimatti, E. Clarke, and Y. Yhu. Symbolic model checking without BDDs. In TACAS, pages 193--207, 1999.

Digital Library

[8]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC), 1999.

Digital Library

[9]

R. Brinkmann and R. Drechsler. RTL-datapath verification using integer linear programming. In Proceedings of VLSI Design, pages 741--746, 2002.

Digital Library

[10]

R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, Z. Hanna, A. Nadel, A. Palti, and R. Sebastiani. A lazy and layered SMT(BV) solver for hard industrial verification problems. In Computer Aided Verification (CAV), LNCS. Springer, 2007.

Digital Library

[11]

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady. Deciding bit-vector arithmetic with abstraction. In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4424 of LNCS, pages 358--372. Springer, 2007.

Digital Library

[12]

R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In CAV, pages 78--92, 2002.

Digital Library

[13]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In 13th ACM Conference on Computer and Communications Security (CCS), pages 322--335. ACM, 2006.

Digital Library

[14]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. H. Counterexample-guided abstraction refinement. In CAV, pages 154--169. Springer, 2000.

Digital Library

[15]

E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In POPL, pages 342--354, 1992.

Digital Library

[16]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

Digital Library

[17]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD), 25:105--127, 2004.

Digital Library

[18]

E. Clarke, M. Talupur, and D. Wang. SAT based predicate abstraction for hardware verification. In SAT, 2003.

[19]

E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, volume 131 of LNCS. Springer, 1981.

Digital Library

[20]

E. M. Clarke and H. Veith. Counterexamples revisited: Principles, algorithms, applications. In Verification: Theory and Practice, pages 208--224. Springer, 2003.

[21]

B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In Proceedings of CAV 2005, pages 296--300. Springer, 2005.

Digital Library

[22]

Cadence SMV, http://www.kenmcmil.com/smv.html.

[23]

D. Cyrluk, M. O. Möller, and H. Rueß. An efficient decision procedure for the theory of fixed-sized bit-vectors. In Computer-Aided Verification (CAV '97), pages 60--71, 1997.

Digital Library

[24]

B. Dutertre and L. de Moura. The Yices SMT solver. Available at http://yices.csl.sri.com/tool-paper.pdf, September 2006.

[25]

V. Ganesh and D. Dill. A decision procedure for bit-vectors and arrays. In Computer Aided Verification (CAV), LNCS. Springer, 2007.

Digital Library

[26]

S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Computer Aided Verification (CAV), volume 1254, pages 72--83, 1997.

Digital Library

[27]

C.-Y. Huang and K.-T. Cheng. Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. In Design Automation Conference (DAC), pages 118--123, 2000.

Digital Library

[28]

H. Jain, D. Kroening, N. Sharygina, and E. M. Clarke. Word level predicate abstraction and refinement for verifying RTL Verilog. In Design Automation Conference (DAC), pages 445--450. ACM, 2005.

Digital Library

[29]

D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 2575 of LNCS, pages 298--309. Springer, 2003.

Digital Library

[30]

R. Kurshan. Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, 1994.

Digital Library

[31]

S. K. Lahiri, S. A. Seshia, and R. E. Bryant. Modeling and verification of out-of-order microprocessors in UCLID. In Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of LNCS, pages 142--159. Springer, 2002.

Digital Library

[32]

P. Manolios, S. K. Srinivasan, and D. Vroon. Automatic memory reductions for rtl model verification. In International Conference on Computer-Aided Design (ICCAD), pages 786--793. ACM, 2006.

Digital Library

[33]

K. L. McMillan. An interpolating theorem prover. In TACAS, pages 16--30. Springer, 2004.

[34]

MiniSat. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/.

[35]

G. Parthasarathy, M. K. Iyer, K.-T. Cheng, and L.-C. Wang. An efficient finite-domain constraint solver for circuits. In Design Automation Conference (DAC), pages 212--217, 2004.

Digital Library

[36]

M. Wedler, D. Stoffel, and W. Kunz. Normalization at the arithmetic bit level. In Design Automation Conference (DAC), pages 457--462. ACM Press, 2005.

Digital Library

Cited By

Mukherjee RSchrammel PKroening DMelham TFanucci LTeich J(2016)Unbounded safety verification for hardware using software analyzersProceedings of the 2016 Conference on Design, Automation & Test in Europe10.5555/2971808.2972077(1152-1155)Online publication date: 14-Mar-2016
https://dl.acm.org/doi/10.5555/2971808.2972077
Gluska ALibis L(2009)Shortening the verification cycle with synthesizable abstract modelsProceedings of the 46th Annual Design Automation Conference10.1145/1629911.1630032(454-459)Online publication date: 26-Jul-2009
https://dl.acm.org/doi/10.1145/1629911.1630032
Wienand OWedler MStoffel DKunz WGreuel G(2008)An Algebraic Approach for Proving Data Correctness in Arithmetic Data PathsProceedings of the 20th international conference on Computer Aided Verification10.1007/978-3-540-70545-1_45(473-486)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1007/978-3-540-70545-1_45

Formal verification at higher levels of abstraction

Recommendations

Lazy Abstraction for Higher-Order Program Verification
PPDP '18: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming

This paper proposes a lazy abstraction algorithm for verification of functional programs. The feature of the lazy abstraction method is that the predicate abstraction and the model checking are fused, and that abstractions for unreachable configurations ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Verification by Augmented Finitary Abstraction

The paper deals with the proof method of verification by finitary abstraction (VFA), which presents a feasible approach to the verification of the temporal properties of (potentially infinite-state) reactive systems. The method consists of a two-step ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

November 2007

933 pages

ISBN:1424413826

General Chair:
Georges Gielen
ESAT-MICAS, Katholieke Univ. Leuven, Leuven, Belgium

Sponsors

CEDA: Council on Electronic Design Automation
SIGDA: ACM Special Interest Group on Design Automation
IEEE CASS/CANDE
IEEE-CS\DATC: IEEE Computer Society

Publisher

IEEE Press

Publication History

Published: 05 November 2007

Check for updates

Qualifiers

Tutorial

Conference

ICCAD07

Sponsor:

CEDA
SIGDA
IEEE-CS\DATC

ICCAD07: The International Conference on Computer-Aided Design 2007

November 5 - 8, 2007

California, San Jose

Acceptance Rates

ICCAD '07 Paper Acceptance Rate 139 of 510 submissions, 27%;

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
267
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mukherjee RSchrammel PKroening DMelham TFanucci LTeich J(2016)Unbounded safety verification for hardware using software analyzersProceedings of the 2016 Conference on Design, Automation & Test in Europe10.5555/2971808.2972077(1152-1155)Online publication date: 14-Mar-2016
https://dl.acm.org/doi/10.5555/2971808.2972077
Gluska ALibis L(2009)Shortening the verification cycle with synthesizable abstract modelsProceedings of the 46th Annual Design Automation Conference10.1145/1629911.1630032(454-459)Online publication date: 26-Jul-2009
https://dl.acm.org/doi/10.1145/1629911.1630032
Wienand OWedler MStoffel DKunz WGreuel G(2008)An Algebraic Approach for Proving Data Correctness in Arithmetic Data PathsProceedings of the 20th international conference on Computer Aided Verification10.1007/978-3-540-70545-1_45(473-486)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1007/978-3-540-70545-1_45

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten