Clock Inference for following Procedural Concurrent Assertion

SystemVerilog
1

Hi All,
Consider the following code ::

default clocking @(posedge clk); endclocking
always @(a) begin : b1
  a2: assert property (<some_seq_expression>);
end

As there is a default clocking block as well as clocking event associated with always block,
I am confused on the clocking event inferred by ‘a2’

As per LRM 16.14.6

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.
b) There is exactly one event control in the procedure.

Since there is no violation of (a) & (b), would ‘a2’ infer @(a) as the clocking event ?

2

Yes, a is the clocking event.

3

Hi Dave,
Seeking your further inputs on this topic
I tried it on edalink where I observe different results across the 3 main tools
Tool 1 throws a compilation error

Inferred clocking expression for a procedural assertion must be ‘posedge’ or ‘negedge’ expression.

Tools 2 & 3 infer default clocking ‘@(posedge) clk’ ( and not ‘a’ ) as the clocking event

For the 1st change in ‘a’ at T:9 there are 2 assertion attempts queued till the posedge of clk occurs next i.e T:15

Note: Although ‘a’ is 0 at T:9, the sampled value of ‘a’ at T:15 would determine pass/fail

For the 2nd change in ‘a’ at T:11 there are again 2 assertion attempts queued till the posedge of clk occurs next i.e T:15

Tool 2 gives two pass reports for a2 ( as ‘a’ is true at T:15 ) and 2 fail reports for a3 ( as ‘b’ is false )
Tool 3 gives only 1 pass for ‘a2’ and 1 fail for ‘a3’

[Q1] I am confused with the different output. What is the ideal output as per LRM ?

The above quote from LRM 16.14.6 has an additional point (c) as well

c) One and only one event expression within the event control of the procedure satisfies both of the following conditions:

1) The event expression consists solely of an event variable, solely of a clocking block identifier, or is of the form edge_identifier expression1 [ iff expression2 ] and is not a proper subexpression of an event expression of this form.

2) If the event expression consists solely of an event variable or clocking block identifier, it does not appear anywhere else in the body of the procedure other than as a reference to a clocking
block signal, as a clocking event or within assertion statements. 
If the event expression is of the form edge_identifier expression1 [ iff expression2 ], no term in expression1 appears anywhere else in the body of the procedure other than as a clocking event or within assertion statements.

LRM has an example for the same

property r3;
q != d;
endproperty

always_ff @(clock iff reset == 0 or posedge reset) begin
  cnt <= reset ? 0 : cnt + 1; // My Comment :: reset referenced within procedural block
  q <= $past(d1); // no inferred clock
  r3_p: assert property (r3); // no inferred clock
end

The edge expression posedge reset cannot be inferred because reset is referenced within the procedure,and the expression clock iff reset == 0 cannot be inferred because it does not have an edge identifier.
In the absence of default clocking, the code above results in an error.

This tells me that as ‘reset’ is referenced within the procedural code it isn’t inferred as clocking event !!

In my code ‘a’ is referenced within the assertion statement ( which is legal as per c)2) )

[Q2] What does the following quote from c)1) imply ?

The event expression consists solely of an event variable, solely of a clocking block identifier,

Does it mean that always block can use a clocking block identifier as an event control ?

default clocking cb @(posedge clk); endclocking
  
always @(cb) begin : 
   a2: assert property (<some_seq_expression>); 
end

[Q3] For the following quote from c)2)

If the event expression consists solely of an event variable or clocking block identifier, it does not appear anywhere else in the body of the procedure other than as a reference to a clocking
block signal, as a clocking event or within assertion statements.

As ‘a’ is not referenced within the procedure other than within assertion statement ‘a2’,
Doesn’t this confirm that always@(a) is legal for ‘a2’ and ‘a3’ to infer ‘@(a)’ as clocking event ?

[Q4] Is it necessary for event control of the procedure to have an edge_identifer in order for clock inference for the embedded concurrent assertion ?

Eg: always@( posedge a ) begin // Has edge_identifier as 'posedge'

4

You can tell that no one uses embedded concurrent assertions in procedural code because no tool provides the correct results, which should be assertion failures at times 9 and 11. The LRM doesn’t place any restrictions on edge qualifiers, so you shouldn’t have to use pos/negedge.

Default clock in block only applies if there is no other explicit leading clock event in the assertion property.

1 Like
5

Thanks Dave for your insightful inputs

On replacing with always@(edge a) ( as always@(a) is essentially equivalent to always@(edge a)) the tools correctly infer @(a) as the clocking event