Formal verification of FIRE
Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley · 1997
We present our experiences with the formal verification of an automotivechip used to control the safety features in a car. We useda BDD based model checker in our work. We describe our verificationmethodology for verifying a very complicated property on arelatively large design. We also describe the bugs that were foundand present our views on how to make model checking an effectiveintegrated part of the design flow for complex hardware systems.