I always struggle to know how to formally verify a counter. So often it seems like the logic within it is just plain obvious to me. How do you re-write something that looks obvious?
In the end, I typically build three basic assertions:
- Following any reset, the counter should return to zero. Although this counter didn’t have any reset logic, most of the counters I’ve worked with do.
- Otherwise (and the otherwise is important), if the counter was non-zero then it should be decrementing
- Don’t forget the induction assertion that the counter never exceeds its bounds!
- Finally, as we are doing here, upon a request the counter should start counting down.
Don’t forget to add a reset check if your design includes a reset.
This last assertion could be added to the if-else based assertion above, however you might notice that the more you do so the more the immediate assertion starts to look like the code given above. This isn’t necessarily a good thing, since you might just copy a bug from one place to another. For this reason, I recommend trying to keep your assertions from “looking-like” the logic they are trying to check.
Perhaps the best example that discusses this best on the blog is the example of the ZipTimer. The ZipTimer is a generic timer that I use with the ZipCPU with interrupt generation and even time-sliced multitasking.