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