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.