Simulation offers us a way of checking the design is doing what we expect, but that is almost exactly why simulation on its own isn’t enough.
When we simulate we are testing what we expect to happen. The problems happen when your design experiences something outside the expected.
There are a couple of extra tools we can use to increase our confidence that the design will work as designed.
A coverage tool tests how complete your simulation or verification efforts actually are.
I’m only aware of one free coverage tool we can use for HDL, and that’s Symbiotic EDA’s mcy.
Formal verification offers the opportunity to prove various properties of your design. For example, in the multi project harness, I wanted to
prove that when the design is in reset the outputs are all undefined.
I can do that by adding an assertion to my design:
assert(gpio_out == 10'bz);
Then I run a tool that uses a solver to prove that this assertion will always hold. If there is any way it can fail it will produce a short trace called a counter example.
Even though this example is very simple it’s good to know that if I do something that accidentally messes up this property the assertion will fail, alerting me.
I have made a short course on Formal Verification for Symbiotic EDA you can follow here:
If you've got any interest in how the sausage is made you should get on the course and you should dig in and find out more. I mean this was the work of secret witches and wizards in mysterious cloaks casting strange incantations over a cauldron! This was all secret stuff and I love that this project is trying to do to silicon design what the open source community has been trying to do with software for the last 30 years. This feels like the next logical step and I think we'll look back and say well of course you can make your own chips that's just a thing and it will just be obvious and commonplace and I look forward to that.