|Designation:||Senior Staff Engineer|
|Title:||Compatible Qualification Metrics for Formal Property Checking|
Abstract: Measuring verification progress and completeness is not only crucial for the management of automotive microcontroller product development, but also demanded by the ISO 26262 safety standard for road vehicles. Formal property checking has been successfully used for decades in the chip industry for verifying digital components of SOCs. However, despite the exhaustiveness of property checks with respect to each single property, the quality and completeness of property sets is by no means guaranteed, if assumptions are too restrictive and output logic is not sufficiently checked. The formal proof environment of OneSpin Solutions has comprised of an outstanding formal completeness checker for a few years, which formally checks whether property sets fully cover all possible input-output-behavior of a digital module. While this completeness criterion is the mathematically strongest possible one, it is not compatible with coverage metrics that are well-established in the simulation world. As modern verification environments are mixed and optimized towards exploiting the strengths of the different verification methodologies, there is a strong demand for mergeable coverage metrics which allow verification results contributed by different approaches to be combined.
Recently, two new metrics have evolved which allow formal property sets to be qualified and a direct relation to simulation coverage results to be established. One such metric is provided by Synopsys’ Certitude tool, which does HDL instrumentation with activatable faults, and contains extensive infrastructure for measuring fault detection by simulating test-cases or proving formal properties. Another new code coverage feature is offered in OneSpin’s proof environment which computes compatible coverage figures by formal property checks.
This paper gives an overview of both approaches and their productive application.
Biography : Holger Busch received his diploma degree in Electrical Engineering from the Technical University of Aachen in 1986, and then joined the Siemens Central Corporate Research Department for VLSI Design Automation. His PhD thesis at Brunel University of West London in 1991 investigated transformational hardware based-on higher-order logic theorem proving technology. He was involved in the development of the in-house SIEMENS CVE property checker, and contributed several patents and publications, and gave numerous trainings in formal property checking.
At Infineon Technologies, he has led numerous formal verification application and methodology projects. Recently he has developed concepts, designs, and verification and qualification methodologies for safety-critical components of Infineon’s latest microcontroller systems.