Hardware Reference
In-Depth Information
the transaction starting at clock tick 10; and in the fourth, we check the transaction
starting at clock tick 10, and when the second transaction comes at clock tick 20, it
is ignored. Why? The checker tracks only one transaction! Essentially, in the fourth
case we check the same scenario as in the third one, since a subsequent go does
not restart counting. FV considers all four scenarios together when it universally
quantifies the free variable, so we will be able to detect a maximal latency violation
for both transactions (if it happens): for the first transaction in the third and in the
fourth scenarios, and for the second transaction in the second scenario.
Lines 20 - 26 . Initially, stage is 0, and it is not incremented until go becomes 1,
which may happen in an arbitrary clock tick when the data_ready is high, as start
is a free variable. Otherwise, the stage number is incremented when the en control
of the corresponding stage is asserted, provided the data has not passed through the
entire pipe, i.e., provided stage != nstages .
Lines 28 - 32 . Initially, the value of latency is 0, and it is not incremented until
free variable start is asserted and data_ready is high. Then it is incremented
each clock tick until the max_latency is exceeded (the value of big_latency is
reached). Then it remains stuck at the value of big_latency forever.
Assertion a1 (Line 39 ) checks that when data leaves the pipeline, that is
when stage becomes nstages for the first time, latency should not exceed
max_latency . Note that in this case it is safe to use the sampled value function
$rose without an initial delay in the antecedent (see Sect. 7.2.1.3 ), since by con-
struction, stage cannot assume the value nstage at the beginning or immediately
after the rst deactivation. Note also that we chose latency != big_latency , and
not latency < big_latency , since the synthesis model of the former expression
is more efficient than that of the latter, and therefore the former expression is also
more efficient in FV than the latter.
Discussion: In our implementation, free variable start is unconstrained, and hence
it can freely oscillate on the trace. Although, as we have seen, this oscillation does
not affect FV correctness, it may affect FV performance, 10 as many redundant traces
are considered. For instance, the fourth scenario is redundant, as was explained
above. We can use the following assumption to get rid of these redundant scenarios:
m1: assume property (start |=> always !start);
This assumption says that start may be high at most in one clock tick.
We might want to get rid of other useless behaviors, those in which start does
not happen at all or in which it is not synchronized with data_ready . This can be
remedied with the following assumption:
initial
m2: assume property ( s_eventually (start && data_ready));
However, assumption m2 is likely to affect negatively the performance of some FV
tools.
t
10 This is highly dependent on the specific tool.
Search WWH ::




Custom Search