Formal Verification Of FIRE: A Case Study
Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley · 2005
We present our experiences with the formal verification of an automotive chip used to control the safety features in a car. We used a BDD based model checker in our work. We describe our verification methodology for verifying a very complicated property on a relatively large design. We also describe the bugs that were found and present our views on how to make model checking an effective integrated part of the design flow for complex hardware systems. 1 Introduction Verification is increasingly becoming the bottleneck in the design flow of electronic systems. Simulation of designs is very expensive in terms of time and exhaustive simulation is virtually impossible. As a result, designers have turned to formal methods for verification. Symbolic model checking is becoming a popular method for verifying commercial sequential designs. In this work, we used Verdict, a BDD based CTL (Computational Tree Logic [1]) model checker under development at Motorola, to verify the correctness of an a...