nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Synthesizing Environment Invariants for Modular Hardware Verification

verfasst von : Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We automate synthesis of environment invariants for modular hardware verification in processors and application-specific accelerators, where functional equivalence is proved between a high-level specification and a low-level implementation. Invariants are generated and iteratively strengthened by reachability queries in a counterexample-guided abstraction refinement (CEGAR) loop. Within each iteration, we use a syntax-guided synthesis (SyGuS) technique for generating invariants, where we use novel grammars to capture high-level design insights and provide guidance in the search over candidate invariants. Our grammars explicitly capture the separation between control-related and data-related state variables in hardware designs to improve scalability of the enumerative search. We have implemented our SyGuS-based technique on top of an existing Constrained Horn Clause (CHC) solver and have developed a framework for hardware functional equivalence checking that can leverage other available tools and techniques for invariant generation. Our experiments show that our proposed SyGuS-based technique complements or outperforms existing property-directed reachability (PDR) techniques for invariant generation on practical hardware designs, including an AES block encryption accelerator, a Gaussian-Blur image processing accelerator and the PicoRV32 processor.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation

Nächstes Kapitel Systematic Classification of Attackers via Bounded Model Checking

Hereafter, we will use “equivalence checking” to refer to instruction-level functional equivalence checking.

Our tool implementation can utilize general constraints in an environment abstraction, not necessarily invariants; however, we focus on invariant generation in this paper – hence we will use abstractions/constraints/invariants interchangeably when discussing the environment hereafter.

All CHC rules are considered to be universally quantified over the variables.

Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1–8 (2013)

Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84–93 (2018)CrossRef

Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14CrossRef

Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885 (2009)

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

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

Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_5CrossRef

Bueno, D., Sakallah, K.A.: euforia: complete software model checking with uninterpreted functions. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 363–385. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-11245-5_17CrossRefMATH

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

10.

Cadence Design Systems Inc: Jaspergold: Formal property verification app (2019). http://www.jasper-da.com/products/jaspergold-apps/. Accessed 20 Sept 2019

11.

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

12.

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

13.

Clifford Wolf: Picorv32 - a size-optimized RISC-V cpu (2019). https://github.com/cliffordwolf/picorv32. Accessed 20 Sept 2019

14.

Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324–342. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_19CrossRef

15.

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

16.

Fadiheh, M.R., Stoffel, D., Barrett, C., Mitra, S., Kunz, W.: Processor hardware security vulnerabilities and their detection by unique program execution checking. In: DATE, pp. 994–999 (2019)

17.

Fadiheh, M.R., et al.: Symbolic quick error detection using symbolic initial state for pre-silicon verification. In: DATE, pp. 55–60 (2018)

18.

Fan, K., Yang, M.J., Huang, C.Y.: Automatic abstraction refinement of TR for PDR. In: Asia and South Pacific Design Automation Conference, pp. 121–126 (2016)

19.

Fedyukovich, G., Bodík, R.: Accelerating syntax-guided invariant synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 251–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_14CrossRef

20.

Fedyukovich, G., Kaufman, S., Bodík, R.: Sampling invariants from frequency distributions. In: FMCAD, pp. 100–107 (2017)

21.

Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained horn clauses using syntax and data. In: FMCAD, pp. 170–178 (2018)

22.

Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69–87. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_5CrossRef

23.

Giannakopoulou, D., Namjoshi, K.S., Păsăreanu, C.S.: Compositional reasoning. Handbook of Model Checking, pp. 345–383. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_12CrossRef

24.

Gleissenthall, K., Kıcı, R.G., Stefan, D., Jhala, R.: IODINE: verifying constant-time execution of hardware. In: USENIX Security Symposium, pp. 1411–1428 (2019)

25.

Gurfinkel, A.: IC3, PDR, and Friends. Summer School on Formal Techniques (2015)

26.

Gurfinkel, A., Belov, A., Marques-Silva, J.: Synthesizing safe bit-precise invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 93–108. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_7CrossRef

27.

Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_20CrossRef

28.

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

29.

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

30.

Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: FMCAD, pp. 158–164. IEEE (2018)

31.

Hsing, H.: Opencores.org tiny\(\_\)aes project page. https://opencores.org/projects/tiny_aes (2014). Accessed 20 Sept 2019

32.

Huang, B.-Y., Zhang, H., Gupta, A., Malik, S.: ILAng: a modeling and verification platform for SoCs using instruction-level abstractions. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 351–357. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_21CrossRef

33.

Huang, B., Zhang, H., Subramanyan, P., Vizel, Y., Gupta, A., Malik, S.: Instruction-level abstraction (ILA): a uniform specification for system-on-chip (SoC) verification. ACM Trans. Design Autom. Electr. Syst. 24(1), 10:1–10:24 (2019)

34.

Ivancic, F., et al.: Scalable and scope-bounded software verification in varvel. Autom. Softw. Eng. 22(4), 517–559 (2015)CrossRef

35.

Jacobs, S.: Extended AIGER format for synthesis. arXiv preprint:1405.5793 (2014)

36.

Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 396–410. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_40CrossRefMATH

37.

Kaivola, R., et al.: Replacing testing with formal verification in Intel Core™i7 processor execution engine validation. In: CAV, pp. 414–429 (2009)

38.

Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. FMSD 48(3), 175–205 (2016)MATH

39.

Kuehlmann, A., Bergamaschi, R.A.: High-level state machine specification and synthesis. In: ICCD, pp. 536–539 (1992)

40.

Lee, S., Sakallah, K.A.: Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 849–865. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_56CrossRef

41.

Manolios, P., Srinivasan, S.K.: A refinement-based compositional reasoning framework for pipelined machine verification. IEEE Trans. VLSI Syst. 16(4), 353–364 (2008)CrossRef

42.

Mattarei, C., Mann, M., Barrett, C., Daly, R.G., Huff, D., Hanrahan, P.: CoSA: integrated verification for agile hardware design. In: FMCAD. IEEE (2018)

43.

McMillan, K.L.: Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 110–121. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028738CrossRef

44.

McMillan, K.L.: Modular specification and verification of a cache-coherent interface. In: FMCAD, pp. 109–116 (2016)

45.

Mishchenko, A., Een, N., Brayton, R., Baumgartner, J., Mony, H., Nalla, P.: Gla: gate-level abstraction revisited. In: DATE, pp. 1399–1404 (2013)

46.

Nguyen, M.D., Thalmaier, M., Wedler, M., Bormann, J., Stoffel, D., Kunz, W.: Unbounded protocol compliance verification using interval property checking with invariants. IEEE Trans. CAD Integr. Circ. Syst. 27(11), 2068–2082 (2008)CrossRef

47.

Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference with learned features. In: PLDI, pp. 42–56. ACM (2016)

48.

Ragan-Kelley, J., Adams, A., Paris, S., Durand, F., Barnes, C., Amarasinghe, S.: Halide: a language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. In: PLDI, pp. 519–530 (2013)

49.

Reid, A.: Trustworthy specifications of ARM® v8-A and v8-M system level architecture. In: FMCAD, pp. 161–168 (2017)

50.

Reid, A., et al.: End-to-end verification of ARM \({textregistred}\) processors with ISA-formal. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 42–58. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_3CrossRef

51.

Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C., Tinelli, C.: cvc4sy: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74–83. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_5CrossRef

52.

Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI, pp. 159–169 (2008)

53.

Si, X., Yang, Y., Dai, H., Naik, M., Song, L.: Learning a meta-solver for syntax-guided program synthesis. In: International Conference on Learning Representations (2019)

54.

Subramanyan, P., Huang, B.Y., Vizel, Y., Gupta, A., Malik, S.: Template-based parameterized synthesis of uniform instruction-level abstractions for SoC verification. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 37(8), 1692–1705 (2018)CrossRef

55.

Subramanyan, P., Vizel, Y., Ray, S., Malik, S.: Template-based synthesis of instruction-level abstractions for SoC verification. In: FMCAD, pp. 160–167 (2017)

56.

Wolf, C.: Yosys open synthesis suite. http://www.clifford.at/yosys/. Accessed 20 Sept 2019

57.

Zhang, H., Yang, W., Fedyukovich, G.: Benchmark examples for environment invariant synthesis. https://github.com/zhanghongce/vmcai2020-inv-syn-benchmarks. Accessed 3 Oct 2019

Titel: Synthesizing Environment Invariants for Modular Hardware Verification
verfasst von: Hongce Zhang
Weikun Yang
Grigory Fedyukovich
Aarti Gupta
Sharad Malik
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-39321-2

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

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-39322-9_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"