Hardware Reference
In-Depth Information
After substitution of let , we obtain the following code:
module m;
bit clk;
integer a, b;
a1: assert property (@(clk) ( int '(a)++));
a2: assert property (@(clk) ((( type bit [7:0])'a+=2) == 1));
property p;
@(clk) ((a =a+b));
endproperty
a3: assert property (p);
endmodule
Assertion a1 contains an illegal form— int '(a) is an expression, not a variable,
hence the increment operator cannot be applied to it.
Assertion a2 results in an illegal form because type cast is applied to the whole
implicit assignment, and it is not clear how the type cast is to be interpreted.
Assertion a3 is seemingly legal, but there is a side effect of replacing the current
value of a by its sampled value summed with b . The SystemVerilog LRM does
forbid assignment expressions in Boolean expressions in sequences and properties,
but not let statements. Even if supported by a simulator, the outcome may be
rather unexpected and difficult to understand. Which value is compared with 1 in
assertion a2 ? The old one or the new one? It would appear that it should be the
old sampled value, but is it? Is the sampled expression just $sampled(a) or is it
$sampled(a + b) in assertion a3 ?
If the let definitions were written by the same person who writes the assertions,
perhaps the expected outcome is clear to that person. However, if the let declara-
tions are part of a package and the user knows little about its contents, then usage of
such forms with side effects becomes problematic and should be illegal.
t
A similar recommendation applies to passing such expressions as actual argu-
ments to otherwise simple innocuous let definitions. This is illustrated on the next
example.
Example 8.7.
let inc( int x) = x;
module m;
bit clk;
integer a, b;
a1: assert property (@(clk) inc(a++));
a2: assert property (@(clk) inc(a+=1) == 1);
property p;
@(clk) inc((a=a+b));
endproperty
a3: assert property (p);
endmodule
After substitution, the code is as follows
module m;
bit clk;
integer a, b;
Search WWH ::




Custom Search