Hardware Reference
In-Depth Information
apparently false. The important consideration here is that the formal semantics of
the free variable is obtained from a universal quantification over its domain in each
clock tick.
t
Example 23.2. Assertion a2 in the following checker passes:
checker success;
default clocking @$global_clock; endclocking
rand bit v;
a1: assert property (v || !v);
endchecker : success
The reason for the success of this assertion is that its underlying expression is a
tautology: it holds for any values of v . The formal semantics of this assertion is
8 i 8 v i
w i
ˆ v i
_: v i , and this formula is true.
t
This example illustrates the general principle that at any given time, all references
to the same free variable within the same assertion have consistent values. In FV,
references to the same free variable in different assertions need not have consistent
values, even at the same time. Put another way, referencing the same free variable in
two assertions does not introduce any relation between the assertions. 1 We have
the same situation as in first-order logic: the names of bound variables are not
important. 2 For example, both statements 8 xx 0 and 8 xx>0are false, though
there is no single x that falsifies both x 0 and x>0.
Example 23.3.
In the following checker
checker check;
default clocking @$global_clock; endclocking
rand bit v;
a1: assert property ( s_eventually v);
a2: assert property ( s_eventually !v);
endchecker : check
both assertions a1 and a2 fail. A counterexample for assertion a1 is v D 0 ; 0 ;:::,
whereas a counterexample for a2 is v D 1 ; 1 ;:::. These two assertions do not have
a common counterexample: on an infinite trace either v or !v must occur infinitely
often. This fact does not prevent failure of both assertions because the references to
v in different assertions need not have consistent values.
t
Formal Semantics. We consider here only assertions without assumptions. The
effect of assumptions is discussed in the next section. For simplicity we limit our
discussion to variables of type bit .
We partition the set V of all model variables into the subset A of regular variables
and the subset F of free variables: V D A [ F and A \ F D; . Since we have
assumed all the variables to be of type bit ,a valuation of the variables is just an
1 This is not true in simulation, where free variables are randomized and hold consistent values
across all assertion statements. See Sect. 23.3 .
2 Ironically enough, bound variables in first-order logic correspond to free variables in SVA.
Search WWH ::




Custom Search