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