Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Electronic Testing
Published in: Journal of Electronic Testing 4/2021

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.
previous article Neural Network-based Online Fault Diagnosis in Wireless-NoC Systems

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
Show more products
Literature
1.
Hasan O, Tahar S (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition. IGI Global, pp. 7162–7170
2.
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.
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.
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.
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.
Klein G, Gamboa R (2016) Interactive theorem proving. J Autom Reason 56(3):201–203CrossRef
7.
Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of model checking, vol. 10. Springer
8.
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.
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.
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.
Russinoff DM (2019) Formal verification of floating-point hardware design: A mathematical approach. Springer
12.
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.
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.
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.
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.
Zhang T, Saab D, Abraham JA (2017) Automatic assertion generation for simulation, formal verification and emulation. In VLSI, pp. 471–476
17.
Mehta AB (2018) SystemVerilog Assertions (SVA). In ASIC/SoC Functional Design Verification. Springer, pp. 75–128
18.
Wolf C, Glaser J, Kepler J (2013) Yosys - A free Verilog synthesis suite. In 21st Austrian Workshop on Microelectronics (Austrochip)
19.
20.
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

News

Test Technology Newsletter

OriginalPaper

Performances and Stability Analysis of a Novel 8T1R Non-Volatile SRAM (NVSRAM) versus Variability

OriginalPaper

Clock-Less DFT and BIST for Dual-Rail Asynchronous Circuits

OriginalPaper

SC-COTD: Hardware Trojan Detection Based on Sequential/Combinational Testability Features using Ensemble Classifier

OriginalPaper

Neural Network-based Online Fault Diagnosis in Wireless-NoC Systems

OriginalPaper

Neuro-Fuzzy Evaluation of the Software Reliability Models by Adaptive Neuro Fuzzy Inference System