Let, Sequence and Property Declarations; Inference - SVA: The Power of Assertions in SystemVerilog - page 166

a1: assert property (@(clk) int '(a++));
a2: assert property (@(clk) ( int '(a+=1) == 1));
property p;
@(clk) ( int '(a=a+b));
endproperty
a3: assert property (p);
endmodule
The outcome of the let substitution is equally illegal or confusing as in the
preceding example.

t

Do not use expressions with side effects such as increment/decrement
and operator assignment expressions in let actual arguments and in let
definitions.

Another issue that is not sufficiently discussed in the SystemVerilog LRM is
the application of bit and part selects over let instances, part and bit selects over
formal arguments in let defining expressions, and in passing bit or part select as
actual arguments to let instances. The problem is that unless the user is aware of the
let definition details, such use may create illegal expressions once the let body is
substituted in place of the instance. We illustrate some of the problematic situations
on the following example.

Example 8.8.
typedef bit [1:0] bt_t;
module m;
logic [7:0] a;
logic [7:0] [2:0] b;
logic c, d, e, f;
let lt1(bt_t x) = x;
let lt2(x) = x[1:0];
let lt3(x) = x;
assign c = lt2(a)[0];
assign d = lt1(a[4:0])[0];
assign e = lt2(a[4:0]);
assign f = lt3(a)[0];
After substitution of let arguments and bodies into the assignments, we get the
following equivalent code:
typedef bit [1:0] bt_t;
module m;
logic [7:0] a;
logic [7:0] [2:0] b;
logic c, d, e, f;
assign c = (a[1:0])[0];
assign d = (bt_t'(a[4:0]))[0];
assign e = ((a[4:0])[1]);
assign f = (a)[0];

t