Making your products more Reliable, Safe and Secure

Formal Discussions at DAC

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

23rd May, 2012|Hardware Verification|