Hardware Reference
In-Depth Information
p1
and
p2
.If
expr
is true and
p1
is a vacuous success, the overall property is a
vacuous success; similarly, when
expr
is false,
p2
determines the result. If the
else
clause is missing then the evaluation is nonvacuous if and only if
expr
is true and
the evaluation of
p1
is nonvacuous. When
expr
is false or when
p1
is a vacuous
success, the evaluation of the overall property is a vacuous success.
Most simulation and formal verification tools report vacuous successes when the
top-level property operator is one of the cases listed above. Other more complex
forms where nested property operators are involved become computationally costly
and more importantly, seldom provide results of practical importance. Nonetheless,
the subject of vacuity has been a topic of research, so the interested reader may wish
to consult [
13
,
24
,
47
], for instance.
An alternative way to define nonvacuous execution of an assertion that is
suitable for simulation is to define it recursively for each operator. This is how the
SystemVerilog LRM defines nonvacuity. The rules first define nonvacuous attempt
evaluation for weak and strong sequences, and then for all property operators in
terms of the evaluation of their operands.
Exercises
10.1.
Rewrite Example
10.7
using a chain of
if
-
else
property operators. How
could you verify that the two forms are equivalent?
10.2.
Which properties are valid (i.e., always true)? Explain.
(a)
((
s_eventually
p1)
and
(
s_eventually
p2))
iff
s_eventually
(p1
and
p2)
(b)
((
s_eventually
p1)
or
(
s_eventually
p2))
iff
s_eventually
(p1
or
p2)
(c)
((
always
p1)
implies
(
always
p2))
iff
always
(p1
implies
p2)
(d)
1'b1
until
1'b0
(e)
1'b1
s_until
1'b0
10.3.
Write a property
never_p
that states that its argument property
p
is never
true.
10.4.
Write a property
next_ev_p(
logic
b,
property
p)
that evaluates to true
if and only if its argument
p
holds at the next occurrence of the Boolean expression
b
. If there are not enough clock ticks for
b
to evaluate to true, then the property
should fail.
10.5.
Write a property
next_ev_a_p(
logic
b,
int
m, n,
property
p)
that
generalizes the property from Exercise
10.4
in such a way that
p
must hold in
the range
[m:n]
of occurrences of
b
after the start of evaluation of
next_ev_a_p
.
The occurrences of
b
need not be consecutive. For example, if the range is
[2:4]
,
Search WWH ::
Custom Search