Skip to main content
Top
Published in:

26-06-2021

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

Authors: Mishal Fatima Minhas, Osman Hasan, Sa’ed Abed

Published in: Journal of Electronic Testing | Issue 4/2021

Log in

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

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.

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!

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!

Show more products
Literature
1.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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)
Metadata
Title
HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits
Authors
Mishal Fatima Minhas
Osman Hasan
Sa’ed Abed
Publication date
26-06-2021
Publisher
Springer US
Published in
Journal of Electronic Testing / Issue 4/2021
Print ISSN: 0923-8174
Electronic ISSN: 1573-0727
DOI
https://doi.org/10.1007/s10836-021-05956-y

Other articles of this Issue 4/2021

Journal of Electronic Testing 4/2021 Go to the issue