Embedding concurrent assertions in procedural code

SystemVerilog
, ,
1

Hi ,
I was referring to section 16.14.6 of the LRM which mentions :

Embedding concurrent assertions in procedural code
A concurrent assertion statement can also be embedded in a procedural block. For example:
property rule;
a ## 1 b ## 1 c;
endproperty
always @(posedge clk) begin
<_statements>
assert property (rule);
end
A clock shall be inferred for the context of an always or initial procedure that satisfies the following requirements:
a) There is no blocking timing control in the procedure. // Need assistance with this
b) There is exactly one event control in the procedure.

Since in the above LRM quote the procedural statements were listed before the procedural concurrent assertion, I decided to try a few variations of procedural statements with a delay : edalink
Based on (a) cases +define+C1 , +define+C2 are illegal ( tools throw compilation error ).
However I am not clear on +define+C3 , should it be considered illegal according to the LRM ?

a) There is no blocking timing control in the procedure.

Does the above LRM quote mean that there should be no blocking construct within the entire always / initial procedural block containing a concurrent assertion ?

2

I think a) is worded rather poorly. Perhaps it would have been better to have written:

a) There shall be no blocking timing controls within the entire procedural block.

But either way, it is clear to me that a #0 anywhere within the procedure is illegal. Your unlikely case might have uncovered a tool specific issue.

3

Hi Dave,
A follow-up question on the same topic.
LRM 2017 Section 16.14.6 mentions ::

In the following example, no clock is inferred due to multiple event controls and delays in the always procedure.

property r4;
q != d;
endproperty

always @(posedge mclk) begin
#10 q <= d1; // delay prevents clock inference
@(negedge mclk) // event control prevents clock inference
#10 q1 <= !d1;
r4_p: assert property (r4); // no inferred clock
end

When simulated I observe a compilation error

The initial part of the same section mentions ::

If no clocking event is specified in a procedural concurrent assertion, the leading clocking event of the
assertion shall be inferred from the procedural context, if possible. If no clock can be inferred from the
procedural context, then the clocks shall be inferred from the default clocking (14.12), as if the assertion
were instantiated immediately before the procedure.

So if I were to add a default clocking block in the code, shouldn’t it be used as leading clock ?
I observe different results across tools currently :: edalink