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