Application of Model Checking to the IBM Power4

  • Applied "functional formal verification" (equivalence checking and model checking) to some extent on approximately 40 design components, including portions of the instruction unit, floating point unit, control logic, memory subsystem and I/O chips
  • Found more than 200 design flaws at various stages and of varying complexity
  • At least one bug was found by almost every application of formal verification
  • Estimate: 15% of bugs would have evaded simulation
    • Some of the bugs literally escaped 1-2 years of simulation
  • Found that application of formal techniques by designers themselves, using formal team as consultants, was very fruitful