An informal introduction

Formal verification can mean different things depending upon who you speak to. If I were blogging under Logic Design, it would probably indicate a series of loosely correlated opinions and observations on the topic of equivalency checking. However, this happens to be the Functional Verification forum and this blog about model-checking.

Model-checking: The process of checking whether a given structure is a model of a given logical formula. Or in engineer-speak, a way of automatically checking if your RTL implementation meets your design specification without a testbench.

Now that we have clearly and comprehensively established the technical context of this weekly bitstream, some disclaimers.

• I am a self-confessed model-checking evangelist
• It is my intention to convince you
  • that model-checking might just be the most productivity-boosting tool you knew the least about
  • that you do not need to be a formal methods PhD to apply it effectively
  • that it is being used in the here and the now by your competition
  • that it might just be the most intellectually satisfying verification experience
  • that it will make you say at least once every morning - "How did it ever find that scenario?"

• I will use facts, reasoning, dialog and weak puns like the title of this post, if necessary, to assimilate you

Next Week: Why simulation guys do not get model-checking.