Skip to main content
Erschienen in:

26.06.2021

HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits

verfasst von: Mishal Fatima Minhas, Osman Hasan, Sa’ed Abed

Erschienen in: Journal of Electronic Testing | Ausgabe 4/2021

Einloggen

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

search-config
loading …

Abstract

Automated formal verification techniques, based on model checking and theorem proving, usually have scalability issues for contemporary digital circuits. On the other hand, interactive theorem provers can overcome this issue, by verifying circuits using universally quantified variables, at the cost of significant skilled guidance. Leveraging upon the complimentary nature of the techniques, this paper presents a hybrid model checking - theorem proving approach for the formal functional verification of digital circuits (HVoC). The main idea is to first use a higher-order-logic theorem prover to replace the structural (RTL or gate level) implementations of the combinational modules with their, formally verified, corresponding behavior and then verify the complete behavioral implementation using a model checker. This kind of a 2-step process not only reduces the computational complexity, but, is also quite effective in terms of counterexample generation time. Our experiments on some benchmarks show an average \(50\%\) reduction in analysis time.

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!

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!

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!

Weitere Produktempfehlungen anzeigen
Literatur
1.
Zurück zum Zitat Hasan O, Tahar S (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition. IGI Global, pp. 7162–7170 Hasan O, Tahar S (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition. IGI Global, pp. 7162–7170
2.
Zurück zum Zitat Shiraz S, Hasan O (2018) A HOL library for hardware verification using theorem proving. IEEE Trans Comput Aided Des Integr Circuits Syst 37(2):512–516CrossRef Shiraz S, Hasan O (2018) A HOL library for hardware verification using theorem proving. IEEE Trans Comput Aided Des Integr Circuits Syst 37(2):512–516CrossRef
3.
Zurück zum Zitat Yu C, Brown W, Liu D, Rossi A, Ciesielski M (2016) Formal verification of arithmetic circuits by function extraction. IEEE Trans Comput Aided Des Integr Circuits Syst 35(12):2131–2142CrossRef Yu C, Brown W, Liu D, Rossi A, Ciesielski M (2016) Formal verification of arithmetic circuits by function extraction. IEEE Trans Comput Aided Des Integr Circuits Syst 35(12):2131–2142CrossRef
4.
Zurück zum Zitat Chandrasekharan A, Soeken M, Große D, Drechsler R (2016) Precise error determination of approximated components in sequential circuits with model checking. In Design Automation Conference, ACM, p. 129 Chandrasekharan A, Soeken M, Große D, Drechsler R (2016) Precise error determination of approximated components in sequential circuits with model checking. In Design Automation Conference, ACM, p. 129
5.
Zurück zum Zitat Hamad GB, Hasan SR, Mohamed OA, Savaria Y (2015) Characterizing, modeling, and analyzing soft error propagation in asynchronous and synchronous digital circuits. Microelectron Reliab 55(1):238–250CrossRef Hamad GB, Hasan SR, Mohamed OA, Savaria Y (2015) Characterizing, modeling, and analyzing soft error propagation in asynchronous and synchronous digital circuits. Microelectron Reliab 55(1):238–250CrossRef
6.
Zurück zum Zitat Klein G, Gamboa R (2016) Interactive theorem proving. J Autom Reason 56(3):201–203CrossRef Klein G, Gamboa R (2016) Interactive theorem proving. J Autom Reason 56(3):201–203CrossRef
7.
Zurück zum Zitat Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of model checking, vol. 10. Springer Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of model checking, vol. 10. Springer
8.
Zurück zum Zitat Guo X, Dutta RG, Mishra P, Jin Y (2016) Scalable SoC trust verification using integrated theorem proving and model checking. In Hardware Oriented Security and Trust, pp. 124–129 Guo X, Dutta RG, Mishra P, Jin Y (2016) Scalable SoC trust verification using integrated theorem proving and model checking. In Hardware Oriented Security and Trust, pp. 124–129
9.
Zurück zum Zitat Seidel PM (2014) A case for multi-level combination of theorem proving and model checking tools. In Microprocessor Test and Verification, pp. 90–97 Seidel PM (2014) A case for multi-level combination of theorem proving and model checking tools. In Microprocessor Test and Verification, pp. 90–97
10.
Zurück zum Zitat Chau C, Hunt WA, Roncken M, Sutherland I (201) A framework for asynchronous circuit modeling and verification in ACL2. In Haifa Verification Conference, Springer, pp. 3–18 Chau C, Hunt WA, Roncken M, Sutherland I (201) A framework for asynchronous circuit modeling and verification in ACL2. In Haifa Verification Conference, Springer, pp. 3–18
11.
Zurück zum Zitat Russinoff DM (2019) Formal verification of floating-point hardware design: A mathematical approach. Springer Russinoff DM (2019) Formal verification of floating-point hardware design: A mathematical approach. Springer
12.
Zurück zum Zitat Bozzano M, Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2019) nuXmv 2.0.0 User Manual Bozzano M, Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2019) nuXmv 2.0.0 User Manual
13.
Zurück zum Zitat Irfan A, Cimatti A, Griggio A, Roveri M, Sebastiani R (2016) Verilog2SMV: A tool for word-level verification. In Design, Automation & Test in Europe, pp. 1156–1159 Irfan A, Cimatti A, Griggio A, Roveri M, Sebastiani R (2016) Verilog2SMV: A tool for word-level verification. In Design, Automation & Test in Europe, pp. 1156–1159
14.
Zurück zum Zitat Minhas M, Hasan O, Saghar K (2018) Ver2Smv - A tool for verilog to SMV translation for verifying digital circuits. In Engineering and Emerging Technologies, pp. 1–5 Minhas M, Hasan O, Saghar K (2018) Ver2Smv - A tool for verilog to SMV translation for verifying digital circuits. In Engineering and Emerging Technologies, pp. 1–5
15.
Zurück zum Zitat Vasudevan S, Liu L, Hertz S (2019) A comparative study of assertion mining algorithms in GoldMine. In Machine Learning in VLSI Computer-Aided Design. Springer, pp. 609–645 Vasudevan S, Liu L, Hertz S (2019) A comparative study of assertion mining algorithms in GoldMine. In Machine Learning in VLSI Computer-Aided Design. Springer, pp. 609–645
16.
Zurück zum Zitat Zhang T, Saab D, Abraham JA (2017) Automatic assertion generation for simulation, formal verification and emulation. In VLSI, pp. 471–476 Zhang T, Saab D, Abraham JA (2017) Automatic assertion generation for simulation, formal verification and emulation. In VLSI, pp. 471–476
17.
Zurück zum Zitat Mehta AB (2018) SystemVerilog Assertions (SVA). In ASIC/SoC Functional Design Verification. Springer, pp. 75–128 Mehta AB (2018) SystemVerilog Assertions (SVA). In ASIC/SoC Functional Design Verification. Springer, pp. 75–128
18.
Zurück zum Zitat Wolf C, Glaser J, Kepler J (2013) Yosys - A free Verilog synthesis suite. In 21st Austrian Workshop on Microelectronics (Austrochip) Wolf C, Glaser J, Kepler J (2013) Yosys - A free Verilog synthesis suite. In 21st Austrian Workshop on Microelectronics (Austrochip)
Metadaten
Titel
HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits
verfasst von
Mishal Fatima Minhas
Osman Hasan
Sa’ed Abed
Publikationsdatum
26.06.2021
Verlag
Springer US
Erschienen in
Journal of Electronic Testing / Ausgabe 4/2021
Print ISSN: 0923-8174
Elektronische ISSN: 1573-0727
DOI
https://doi.org/10.1007/s10836-021-05956-y

Weitere Artikel der Ausgabe 4/2021

Journal of Electronic Testing 4/2021 Zur Ausgabe