Above, you can see my two favorite assumptions.
First, we assume that the step size is never zero. Not all designs require this assumption, but if you want to skip it you might have a challenge passing induction. Why? Well, the induction engine is known for doing such crazy things as keeping the clock idle until the very end of the trace. Then, just before the end of the trace, a single clock edge will take the design from a (not-illegal) state to one that violates an assertion. Worse, it doesn’t matter how long your proof is–adding more steps to the proof doesn’t help in this case. However, if you force the clocks to always step forward, you can keep this situation from happening.
This criteria is closely related to the usage of
$past(). If you want to use
$past() with either of the two clocks above, you’ll need to guarantee that
there’s at least two clock ticks within the duration of your proof–one of
which will actually set the
$past() value and guarantee its relevance to the
design, and the second of which will test it. (Otherwise, the solver might
$past() being anything–an ugly failure mode that you’d never be
able to observe on the trace.) If you also have very slow clocks, this will
also drive the duration of your proof. In the example above, for example,
the proof will need to be a minimum of 258 steps to guarantee a second clock
edge before the final one.
A tedious, but alternative, way of working around this is to make all of your
assertions run combinatorially,
always @(*), and to implement
yourself. Indeed, I found this to be the key to getting my asynchronous
FIFO proof down
from a rough hour to less than a second–but I digress. (Note that these
updates were part of a rewrite of the entire
and took place after writing my article on verifying an asynchronous
The other assumption above simply keeps the solver from working too hard. Once the clock step size becomes greater than a half interval, the clock frequency will stop increasing as the step size increases anymore. Indeed, the clock frequency will then go down as the step size increases due to a phenomenon known as aliasing. If we instead assume that the clock frequency stays at a half interval or less, we can keep the solver from examining the alias frequencies. This also has the helpful side-effect of making any resulting traces more comprehensible.