Click here for the answer.
Let’s come back to our simple counter example again (no pun intended at first, enjoyed ever since), and let’s build a quiz from it again.
This time we’ve fixed the issue with the initial
we’ve chosen to ignore the ASIC designers who will insist our counter
requires an initial reset signal (it wouldn’t fit on the slide with a reset,
but you can add one if to the puzzle above if it makes you feel better),
and we’ve asserted that our counter will never meet or exceed
24. (You may assume the
counter has enough of a bit width to reach
24 …) We’ve also brought back
i_start_signal, which will trigger our counter.
Today, though, we want to assume that the start signal is never raised, and having assumed that we want to prove that the counter will remain zero.
Will the assertion below prove that?