Hardware Reference
In-Depth Information
Assumptions with free variables constrain the free variable domains for all
assertions using these free variables.
Example 23.4.
Consider the following checker:
checker
check;
default clocking
@$global_clock;
endclocking
rand bit
[5:0] v;
m1:
assume property
(v>2);
m2:
assume property
(v<7);
a1:
assert property
(v>1);
a2:
assert property
(
s_eventually
v<=5);
a3:
assert property
(
s_eventually
v > 5);
endchecker
: check
Assumptions
m1
and
m2
constrain free variable
v
such that
v
may only assume values
3, 4, 5 and 6 in all global clock ticks for all assertions. For all other values of
v
, all the
assertions are understood to hold vacuously under the assumptions. This statement
means that if
v
assumes some other value violating the assumptions, then we don't
even need to check the assertions for that value.
Assertion
a1
holds since it holds for the constrained values of
v
. Assertions
a2
and
a3
fail, as explained in Example
23.3
.
t
Formal Semantics.
The formal semantics of an assertion relative to a set of
assumptions in the presence of free variables is as follows. Let
Q
be the set
of assumptions, and let Q
D
V
Q
be their conjunction. Reduced trace
w satisfies
, written
w
;
Q
ˆ
p,iff
w
ˆ
Q
implies
p, where
Q
implies
p is treated as an assertion without assumptions. From the preceding
section,
w
ˆ
Q
implies
p iff for every extended trace W such that .W /
D
w
,
W
ˆ
Q
implies
p.Now,W
ˆ
Q
implies
p means that if W
ˆ
Q, then W
ˆ
p.
We will say that an extended trace W is
Q
assertion p
relative to
Q
-
feasible
iff W
ˆ
Q, i.e., iff W
ˆ
q for
all q
2
Q
. Then we can say that
w
;
Q
ˆ
p
iff
8
Q
-feasible W s.t. .W /
D
w
W
W
ˆ
p
If the set
of assumptions is understood, it may be dropped from the notation, and
we may say more briefly that in the presence of assumptions,
Q
w
ˆ
p
iff
8
feasible W s.t. .W /
D
w
W
W
ˆ
p
23.1.3
Free Variables in Cover Statements
As defined in Sect.
21.3.3
, the property p is covered iff there is a trace that
satisfies p.Ifp depends on a free variable
v
then in order for p to be covered
Search WWH ::
Custom Search