Hardware Reference
In-Depth Information
feel similar, yet they are not equivalent. If we check their equivalence in formal
verification a counterexample explains the difference. Only the assertion comparing
the properties and wire or module input declarations of the variables used in the
assertion are required in this case; neither a model nor assumptions are needed.
Example 10.4.
Check that the properties
always nexttime
e
and
nexttime
always
e
are equivalent.
Solution:
wire
e;
initial
a:
assert property
(
(
always nexttime
e)
iff
(
nexttime always
e));
t
The following example is perhaps less evident, yet the two properties are in fact
equivalent:
Example 10.5.
property
p1;
not
(a[
*
] ##1 b);
endproperty
property
p2;
strong
(!b[+] ##0 !a);
endproperty
a1:
assert property
(p1
iff
p2);
t
If [Else]
The property
if
(b)p
is true if Boolean
b
is false or
p
is true. The property
if
(b)p
else
q
is true if Boolean
b
is true and
p
is true, or
b
is false and
q
is
true.
Note that is possible to express the same using suffix implication, as
b |-> p
, and
(b |-> p)
and
(!(
bit
'(b))|-> q)
, respectively.
Clearly, the
if
-
else
form is easier to understand than its equivalent using suffix
implication, as illustrated in the following example.
Example 10.6.
In assertions
a1
and
a2
,if
b
is true,
a
should be false or
b
should be
false one clock tick later, else if
b
is false then
a
must be true, followed by
b
true one
clock tick later. Clearly, assertion
a1
is easier to understand. Assertion
a3
uses an
if
property without the
else
clause. In that case, the equivalent formulation shown
in assertion
a4
is as easily understood, hence there is no preference between them.
a1:
assert property
(
if
(b)
not strong
(a ##1 b)
else
a ##1 b);
a2:
assert property
(
(b |->
not strong
(a ##1 b))
and
(!
bit
'(b) |-> a ##1 b));
a3:
assert property
(
if
(b) a ##1 b);
a4:
assert property
(b |-> a ##1 b);
t
Search WWH ::
Custom Search