Holger Busch, Infineon Technologies 2014-04-17T14:34:14+00:00

Name:Holger Busch
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.

Verification Futures Conference Presentation                                                      Video Presentation

 

 

T&VS NEWSLETTER SIGN-UP
The T&VS newsletters inform you about industry news, events and information from T&VS. No spam, we promise and it is always easy to unsubscribe.
We never share your information. Read our Privacy Statement
Interested in Formal Verification?
Then why not attend the TVS Formal
Verification Bootcamp training?
The 2-day Formal Verification Bootcamp is for design and verification engineers looking to enhance their knowledge of formal verification and to learn how to write effective assertions to find and fix bugs. The course is a mix of presentations and hands-on development exercises.
Bootcamp Enquiry Form
If you are interested in receiving additional information on the course then simply email Mike Bartley (TVS CEO and Course Leader) by entering your details below.
Interested in SystemC?
FREE SystemC UVM Library Now Available
The TVS SystemC UVM library closely mimics UVM but gives users a license free UVM-based verification environment.
Have your product requirements been successfully tested and implemented?
Find out how asureSIGN can help you implement a successful Requirements Driven Verification and Test Strategy by visiting asureSIGN or enter your details and we will be in touch.
Course Dates and Pricing
To receive additional information, including course dates and pricing, please contact our training team who will be happy to help.
Download Request
Please complete the following form then click 'submit' to access the download.
Presentation Request
Please complete the following form then click 'submit' to gain access to the presentations.
DOWNLOAD REQUEST
Please complete the following form and then click 'submit' to gain access to the download.
FREE QA ASSESSMENTS
Did you get what you were looking?

Let the testing experts help. We will run a FREE QA assessment which will include our top 5 recommendations to help maximise your testing.