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".

Volltext Dateien herunterladen

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS
Metadaten
Verfasserangaben:Joerg Bormann
URN (Permalink):urn:nbn:de:hbz:386-kluedo-46801
Dokumentart:Sonstiges
Sprache der Veröffentlichung:Englisch
Veröffentlichungsdatum (online):09.07.2017
Jahr der Veröffentlichung:2009
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):11.07.2017
Freies Schlagwort / Tag:coverage; digital integrated circuit; formal description technique; formal method; hardware verification
Seitenzahl:126
Fachbereiche / Organisatorische Einheiten:Fachbereich Elektrotechnik und Informationstechnik
CCS-Klassifikation (Informatik):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-Sachgruppen:6 Technik, Medizin, angewandte Wissenschaften / 621.3 Elektrontechnik, Elektronik
Lizenz (Deutsch):Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0)

$Rev: 13581 $