Click here for the answer.

Induction can be very confusing to an HDL designer trying to use the formal verification tools for the first time. A common refrain that I’ve heard among those I’ve mentored is, “but I set this value on reset! How can it ever get into this state?”

The induction exercise in my formal verification training course is also a place where I slow down, and take some time with the students to learn and watch what happens. We take examples, like the one above, and then try several formal verification techniques to see what works and what doesn’t. In many ways, it’s like trying out the various tools in your tool box. That way, when you need to use one, you’ll know which one is most suited for the task at hand.

In practice, the problem is never this simple. It’s usually found buried within a much more complex design, and it takes some work to recognize it. The good news is that the solutions to the simple problems, such as the one above, can often be applied to these more complex examples as well–so knowing the tools in your toolbox is quite valuable.

In this case, there are several ways around this bug.