Model Checking promises so much potential but how do we ensure we maximise the ROI? It helps by first trying to have a language to discuss how we can apply it:
- Bug Avoidance: In this application of model checking the objective is to avoid adding bugs to designs in the first place.
- Bug Hunting: The objective here is to find bugs in a design rather than try to prove the design satisfies the given requirements.
- Bug Absence: This is the traditional application of model checking where we try to prove that the design satisfies important properties.
- Bug Analysis: By writing the symptom of the bug as a property, a formal tool can generate a waveform of minimum length to show the failure. This has been shown to be very effective in post-silicon debug.
Follow the link to expand on these definitions PracticalApplicationofFormalVerification
Armed with our 4 different applications of formal and our language for describing them, we can better understand how formal fits into the design flow. Follow the link Formal_in_the_Design_Flow to see a picture of this.
We can also see how these applications can be better used to exploit formal and maximise the ROI.
- Maximise advantages of formal: Ease of set-up; Flexibility of verification environment; Full proofs; Intensive stressing of design; Corner cases
- Minimise drawbacks of formal: False failures; False proofs; Limits on size of the model that can be analysed; Non-exhaustive checks; Non-uniform run times
All this will be presented in a poster session at DAC at 12.30 on Tuesday 5th June 2012
Please note that TVS did this work in conjunction with ARM and Jasper