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

Example 8.5.
module m;
bit clk;
logic a, b;
let x = $past(a && b);
let y = $past(a && b, , ,@( posedge clk));
always_comb begin
a1: assert #0 (x);
a2: assert #0 (y);
end
a3: assert property (@( posedge clk) a |-> x);
endmodule
In this example, let instances are used in three assertions, a1 , a2 , and a3 . While
the form of the instance is legal in a2 and a3 , it is illegal in a1 .Why?
The sampled value function requires a clocking event for updating the previous
value of its argument. There is no clocking event available and it cannot be inferred
when x is expanded in a1 . This results in an illegal use of $past .In a2 , the clocking
event is explicitly specified in the sampled value function in the definition of y .
Therefore, after substitution of y into a2 , a legal form of the deferred assertion a2
is obtained. Finally, in a3 there is no explicit clocking event in the sampled value
function, after substituting the body of x into a3 , the assertion contains the following
body:

a3: assert property (@( posedge clk) a |-> ($past(a && b)));
The property in the assertion that resulted from the substitution is perfectly legal
because the clocking event for the sampled value function is inferred from the
assertion.

t

We now examine some problematic cases. They are not explicitly identified as
illegal in the SystemVerilog LRM, but their use may lead to some unexpected results
and should be considered as illegal. The first case involves explicit or implicit form
of variable_lvalue assignment, that is, the variable or expression on the left-hand
side of an assignment.

Example 8.6.
let inc1( int x) = x++;
let inc2( bit [7:0] y) = y+=2;
let combinetwo( integer v,w)=(v=v+w);
module m;
bit clk;
integer a, b;
a1: assert property (@(clk) inc1(a));
a2: assert property (@(clk) inc2(a) == 1);
property p;
@(clk) combinetwo(a, b);
endproperty
a3: assert property (p);
endmodule