Formal Verification of Safety Mechanisms

Conference:	DVCLUB Europe \| Selection of 2021 DVCon/DAC Verification Papers
Speaker:	Keerthi Devarajegowda, Staff Engineer, Infineon Technologies AG.
Abstract:	This talk will highlight how formal verification is deployed to exhaustively verify designs that implement safety mechanisms such as Error Correction Codes (ECCs). ECC designs that encode a large data vector and detect multiple bit errors have been traditionally verified with simulation-based methods even though they are better suited for formal verification. The main reason was the scalability of formal verification for large ECC designs. Properties that are written to verify large ECC designs time-out without an outcome owing to limited memory or time resources. We discovered that a succinct characteristic of ECC designs can be exploited to achieve an exhaustive proof on large ECC designs. For instance, the proof runtime of a 3 bit error detection/correction property requires less than 2 hours for passing on a 256 bit ECC design. Previously, the same property timed out after running for 6 days. We successfully applied this approach to multiple instances of ECC designs implemented across several safety-critical automotive SoCs. Results show that the proof runtime of the properties leveraging the proposed approach decreases at least by a factor of 50, and scales proportionally with the width of the data vector and detection and correction capability of the codes. 3 Key Points: To protect against abnormal operational conditions special design mechanisms are adopted for semiconductor chips used in safety critical applications Formal Verification is key to find all design bugs and to prove the absence of design bugs in safety critical designs By exploiting underlying principles of the design, formal verification can be used to exhaustively verify the designs even for larger designs that are often considered as “too bug for formal”.
Speaker Biography:	Keerthi Devarajegowda is currently with Infineon Technologies AG, Germany as a Staff Engineer. He obtained his doctoral degree from TU Kaiserslautern, Germany in 2021. In his current role, Keerthi is responsible for formal verification of complex design blocks, formal verification methodology project, and automation of design development flows.

Sponsors

DVCLUB Europe is made possible through the generosity of our sponsors.