Hardware Reference
In-Depth Information
it should be possible to choose values of
v
in each position on the trace so that
p becomes satisfied. Therefore, we come to the following characterization of free
variables in the coverage context:
The behavior of a free variable in a coverage context is obtained from
existential quantification over its domain in each clock tick.
Example 23.5.
Consider the following checker:
checker
check(
bit
a);
default clocking
@$global_clock;
endclocking
rand bit
v;
c1:
cover property
((a&&v)[
*
2]);
c2:
cover property
((a||v)[
*
2]);
endchecker
: check
If
a
is always low,
c1
is not covered, while
c2
is. There are no values of
v
that could
cause sequence
(a && v)[
*
2]
to match. If
v
is
1
in clock ticks 0 and 1, sequence
(a || v)[
*
2]
has a match in clock tick 1.
t
If free variables are constrained with assumptions, these assumptions should be
taken into account when evaluating the coverage.
Example 23.6.
Consider the following checker:
checker
check;
default clocking
@$global_clock;
endclocking
rand bit
v;
m1:
assume property
($steady_gclk(v));
c1:
cover property
(v ##1 !v);
endchecker
: check
Cover statement
c1
cannot be satisfied because of assumption
m1
imposed on free
variable
v
, which requires it to keep the same value all the time. Without
m1
,
c1
is
covered in clock tick 1: it is sufficient to choose the value of
v
to be
1
in clock tick
0 and
0
in clock tick 1.
t
Formal Semantics.
Cover statement c is
satisfied
on reduced trace
w
iff there exists
a feasible extended trace W that projects to
w
and satisfies c. In other words,
w
ˆ
c
iff
9
feasible W
W
.W /
D
w
and W
ˆ
p
This existential quantification over extended traces makes precise the sense in which
free variables are existentially quantified over their domains in the semantics of a
cover statement.
Search WWH ::
Custom Search