Practical Application of Model Checking – a Taxonomy of Methodologies

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 was presented in a poster session at DAC on Tuesday 5th June 2012 –DAC_2012

Please note that TVS did this work in conjunction with ARM and Jasper

Leave a Reply