Legal ways to specify the leading clock in SVA

SystemVerilog
,
8

In reply to Ahmed Kelany:

So my question is which section in the LRM says using assert property is illegal in a looping statement?

You are correct, 1800 does not specifically say that it is illegal for looping statements.
The following reasons, based on SV rules, are possibly why one vendor is enforcing this restriction:

  1. Unrolling errors:
    Concurrent asserts are essentially static objects; if they are placed in a loop, the loop would have to be either unrolled or the assertion placed in an equivalent generate loop. For example:
    Edit code - EDA Playground

always @(posedge clk) begin
for (int i=0; i<=3; i++) begin
assert property(a|-> b);
// ILLEGAL:  Range must be bounded by constant expressions.
ap_arbiter: assert property(@(posedge clk)
(req[i]==1'b1) ##0 req[i:0] !=0 |=>
grnt[i]==1'b1 ##0 $onehot(grnt) );
end
end

One could say, yah, but the following should be legal if I change req[i:0] to req[i]

2. Infinite loop in a clocking block: For example (2) - EDA Playground


always @(posedge clk) begin
while(c==1) begin  // ifinite loop
assert property(a|-> b);
end
end
// System virtual memory limit exceeded -

We have the same issue with the forever

Getting back to the question: Should looping allowed in an always, always_ff?
Maybe there is a philosophical or inference reason for a tool to put such a code constraint because it can cause trouble or implementation issues.

Ben