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