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.