Complete Functional Verification

  • The dissertation describes a practically proven, particularly efficient approach for the verification of digital circuit designs. The approach outperforms simulation based verification wrt. final circuit quality as well as wrt. required verification effort. In the dissertation, the paradigm of transaction based verification is ported from simulation to formal verification. One consequence is a particular format of formal properties, called operation properties. Circuit descriptions are verified by proof of operation properties with Interval Property Checking (IPC), a particularly strong SAT based formal verification algorithm. Furtheron, a completeness checker is presented that identifies all verification gaps in sets of operation properties. This completeness checker can handle the large operation properties that arise, if this approach is applied to realistic circuits. The methodology of operation properties, Interval Property Checking, and the completeness checker form a symbiosis that is of particular benefit to the verification of digital circuit designs. On top of this symbiosis an approach to completely verify the interaction of completely verified modules has been developed by adaptation of the modelling theories of digital systems. The approach presented in the dissertation has proven in multiple commercial application projects that it indeed completely verifies modules. After reaching a termination criterion that is well defined by completeness checking, no further bugs were found in the verified modules. The approach is marketed by OneSpin Solutions GmbH, Munich, under the names "Operation Based Verification" and "Gap Free Verification".

Download full text files

Export metadata

Author:Joerg Bormann
Document Type:Other
Language of publication:English
Date of Publication (online):2017/07/09
Year of first Publication:2009
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2017/07/11
Tag:coverage; digital integrated circuit; formal description technique; formal method; hardware verification
Page Number:126
Faculties / Organisational entities:Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
CCS-Classification (computer science):B. Hardware / B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION / B.5.3 Reliability and Testing** (B.8)
I. Computing Methodologies / I.6 SIMULATION AND MODELING (G.3) / I.6.4 Model Validation and Analysis
J. Computer Applications / J.6 COMPUTER-AIDED ENGINEERING / Computer-aided design (CAD)
DDC-Cassification:6 Technik, Medizin, angewandte Wissenschaften / 621.3 Elektrotechnik, Elektronik
Licence (German):Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0)