Top

Published in:

2019 | OriginalPaper | Chapter

Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction

Authors : Aman Goel, Karem Sakallah

Published in: NASA Formal Methods

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

While bit-level IC3-based algorithms for hardware model checking represent a major advance over prior approaches, their reliance on propositional clause learning poses scalability issues for RTL designs with wide datapaths and complex word-level operations. In this paper we present a novel technique that combines IC3 with syntax-guided abstraction (SA) to allow scalable word-level model checking using SMT solvers. SA defines the abstraction implicitly from the syntax of the input problem, has high granularity and an abstract state-space size completely independent of the bit widths of the design’s registers. We show how to efficiently integrate IC3 with SA, and demonstrate its effectiveness on a suite of open-source and industrial Verilog RTL designs. Additionally, SA aligns easily with data abstraction using uninterpreted functions. We demonstrate how IC3+SA with data abstraction allows reasoning that is completely independent of the bit width of variables, and becomes scalable irrespective of the state-space size or complexity of operations.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Optimizing a Verified SAT Solver

next chapter Towards a Two-Layer Framework for Verifying Autonomous Vehicles

In this notation, vertical bars separate the equivalence classes of the partition. Thus \(\{ a, b | c \}\) should be interpreted to mean \(\{ \{a, b\}, \{c\} \}\) in the standard notation for partitions.

.ilang is a format for textual representation of the yosys’s design.

We obtained these designs under non-disclosure agreements and, unfortunately, cannot make them publicly available.

https://github.com/aman-goel/nfm2019exp

ABC: System for Sequential Logic Synthesis and Formal Verification. https://github.com/berkeley-abc/abc

The nuXmv model checker. https://nuxmv.fbk.eu

Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Reveal: a formal verification tool for Verilog designs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 343–352. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_25CrossRefMATH

Babić, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 366–378. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_41CrossRefMATH

Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_19CrossRefMATH

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org

Berkeley Logic Synthesis and Verification Group: ABC: A system for sequential synthesis and verification (2017). http://www.eecs.berkeley.edu/~alanmi/abc/

Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Adv. Comput. 58(11), 117–148 (2003)CrossRef

10.

Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: FMCAD, p. 9 (2017)

11.

Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831–848. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_55CrossRef

12.

Bjørner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263–281. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_15CrossRef

13.

Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7CrossRef

14.

Bradley, A.R., Somenzi, F., Hassan, Z.: IIMC: incremental inductive model checker. http://www.github.com/mgudemann/iimc

15.

Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58179-0_44CrossRef

16.

Cabodi, G., Nocco, S., Quer, S.: The PdTRAV tool. http://fmgroup.polito.it/index.php/download/viewcategory/3-pdtrav-package

17.

Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22CrossRef

18.

Chockler, H., Ivrii, A., Matsliah, A., Moran, S., Nevo, Z.: Incremental formal verification of hardware. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 135–143. FMCAD Inc. (2011)

19.

Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_23CrossRef

20.

Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46–61. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_4CrossRefMATH

21.

Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods Syst. Des. 49(3), 190–218 (2016)CrossRef

22.

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15CrossRef

23.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

24.

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49CrossRef

25.

Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125–134 (2011)

26.

Goel, A., Sakallah, K.: Averroes 2. http://www.github.com/aman-goel/avr

27.

Goel, A., Sakallah, K.: Empirical evaluation of IC3-based model checking techniques on Verilog RTL designs. In: Proceedings of the Conference on Design, Automation and Test in Europe. EDA Consortium (2019)

28.

Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10CrossRef

29.

Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 391–408. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-40922-X_22CrossRef

30.

Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: FMCAD, pp. 157–164 (2013)

31.

Ho, Y.S., Chauhan, P., Roy, P., Mishchenko, A., Brayton, R.: Efficient uninterpreted function abstraction and refinement for word-level model checking. In: FMCAD, pp. 65–72 (2016)

32.

Ho, Y.S., Mishchenko, A., Brayton, R.: Property directed reachability with word-level abstraction. In: FMCAD, pp. 132–139 (2017)

33.

Ho, Y.S., Mishchenko, A., Brayton, R., Eén, N.: Enhancing PDR/IC3 with localization abstraction (2017)

34.

Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_13CrossRef

35.

Irfan, A., Cimatti, A., Griggio, A., Roveri, M., Sebastiani, R.: Verilog2SMV: a tool for word-level verification. In: Proceedings of the 2016 Conference on Design, Automation & Test in Europe, pp. 1156–1159. EDA Consortium (2016)

36.

Jain, H., Kroening, D., Sharygina, N., Clarke, E.: VCEGAR: Verilog CounterExample guided abstraction refinement. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 583–586. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_45CrossRef

37.

Kurshan, R.P.: Computer-aided verification of coordinating processes. Princeton series in computer science (1994)

38.

Lange, T., Neuhäußer, M.R., Noll, T.: IC3 software model checking on control flow automata. In: Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, pp. 97–104. FMCAD Inc. (2015)

39.

Lee, S.: Unbounded scalable hardware verification (2016)

40.

Lee, S., Sakallah, K.A.: Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction. In: CAV, pp. 849–865 (2014)

41.

Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Automated Reasoning 40(1), 1–33 (2008)MathSciNetCrossRef

42.

McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_1CrossRef

43.

Mneimneh, M., Sakallah, K.: Sat-based sequential depth computation. In: Proceedings of the 2003 Asia and South Pacific Design Automation Conference, pp. 87–92. ACM (2003)

44.

Mukherjee, R., Tautschnig, M., Kroening, D.: v2c – a Verilog to C translator. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 580–586. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_38CrossRef

45.

Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: Amuse: a minimally-unsatisfiable subformula extractor. In: Proceedings of the 41st Annual Design Automation Conference, pp. 518–523. ACM (2004)

46.

Rota, G.C.: The number of partitions of a set. Am. Math. Monthly 71(5), 498–504 (1964)MathSciNetCrossRef

47.

Tafertshofer, P., Ganz, A.: Sat based ATPG using fast justification and propagation in the implication graph. In: Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, pp. 139–146. IEEE Press (1999)

48.

Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and sat-based reachability in hardware model checking. In: FMCAD, pp. 173–181 (2012)

49.

Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: CAV, pp. 260–276 (2014)CrossRef

50.

Welp, T., Kuehlmann, A.: QF BV model checking with property directed reachability. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 791–796. EDA Consortium (2013)

51.

Wolf, C.: Yosys open synthesis suite. http://www.clifford.at/yosys/

Title: Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction
Authors: Aman Goel
Karem Sakallah
Publisher: Springer International Publishing
Book: NASA Formal Methods
Print ISBN: 978-3-030-20651-2

Electronic ISBN: 978-3-030-20652-9

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-20652-9_11

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner