In reply to Ahmed Kelany:
I couldn’t find anything in the 2017 LRM that justifies your comment in number [5]
// Procedural assertion ( i.e., assert, assume or cover property) is not
// allowed in looping statement.
1800’21017: 16.16
— Contextually inferred clock from a procedural block, for example:
always @(posedge clk) assert property (not (a ##2 b));
1800:2017 Clause 9 describes the SystemVerilog **procedural blocks**:
initial, always, always_comb, always_ff, always_latch, and final.
9.2 Structured procedures All structured procedures in SystemVerilog are specified within one of the following constructs:
— initial procedure, denoted with the keyword initial (see 9.2.1 )
— always procedure, denoted with the keywords: • always (see 9.2.2.1 )
• always_comb (see 9.2.2.2 )
• always_latch (see 9.2.2.3 )
• always_ff (see 9.2.2.4 )
— final procedure, denoted with the keyword final (see 9.2.3)
— Task
— Function
The syntax for these structured procedures is shown in Syntax 9-1 )
I’ve tried the following code and it seems like it’s legal. in the below code always_asrt (defined in always block) is equivalent to forever_asrt (defined in a loop).
You touched on tool issues, and we don’t discuss tools in this forum.
If you have a problem, contact your vendor.
In any case, 1800 is specific as to what is a procedural block.
//----------------------//
initial begin
forever @(posedge clk)begin
forever_asrt: assert property(forever_pp); // line 28
end
end
sim: Error-[PAOCNAILS] Procedural assertion in a loop
testbench.sv, 28
test, "assert property(forever_pp);"
Procedural assertion ( i.e., assert, assume or cover property) is not
allowed in looping statement.Only immediate assertions are allowed in this
context.
Ben