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