Clock Inference for Embedded concurrent assertion

SystemVerilog
, , ,
1

Hi All,
Consider a concurrent assertion with an explicit clocking event ‘@(posedge) clk2’ embedded within an always procedural block with a different clocking event ‘@(posedge clk1)’ :: edalink

I have three questions related to it

(Q1) Which clock would the concurrent assertion consider as leading clock ? Would it be equivalent to ::

 ap1:assert  property( @(posedge clk1)  @(posedge clk2) req );

(Q2) How would the code work in the 3 cases ? ( I observe that the o/p differs across tools )

For (Q2) shouldn’t the concurrent assertion execute on the posedge of clk2 immediately following the posedge of clk1 ?

Here is my expectation ::

(a) For +define+M1 , as the always block is triggered at T:10 , 30 , 50
‘ap1’ should execute at T:15 , 35 , 55 respectively

(b) For +define+M2 , as the always block is triggered at T:05 , 15 , 25 , 35 , 45 , 55
‘ap1’ should execute at T:10 , 30 , 50 respectively

(c) For +define+M3 , as the always block is triggered at T:05 , 15 , 25 , 35 , 45 , 55
‘ap1’ should execute at T:05 , 15 , 25 , 35 , 45 , 55 respectively

(Q3) Would the addition of a default clocking block ( using @(posedge clk3) ), change anything ?

2

the_LCE
the_LCE1353×719 41.2 KB

3

Thanks Ben.
(1) For (2) (b) the output should be ::

TIME:10 Assertion PASSes
TIME:30 Assertion PASSes
TIME:30 Assertion PASSes
TIME:50 Assertion PASSes
TIME:50 Assertion PASSes

I later found that the LRM 2017 does mention this in Section 16.14.6 Embedding concurrent assertions in procedural code

For example, in the following code fragment, the clocking event @(posedge mclk)  is inferred as the
clocking event of r1_p1, while r1_p2 is clocked by @(posedge scanclk)  as written:

property r1;
  q != d;
endproperty

always @(posedge mclk) begin
   q <= d1;
  r1_p1: assert property (r1);
  r1_p2: assert property (@(posedge scanclk) r1);
end

The resulting behavior of the preceding assertion r1_p2 depends on the relative frequencies of mclk and scanclk. For example:
— If scanclk runs at twice the frequency ofmclk, only every other posedge of scanclk will result in an evaluation of r1_p2. 
  It is only queued when reached during procedural execution, which happens on a rising edge of mclk.
— If mclk runs at twice the frequency of scanclk, then by every posedge of scanclk, two pending procedural instances of r1_p2 will mature. 
  Thus every posedge of scanclk will see r1_p2 evaluated and results reported twice.

(2) For (3) the clock inference for procedural concurrent assertions
would be in following priority order ::
(a) It has it’s own explicit clock ( like r1_p2 above )
(b) In absence of (a), the clock is inferred via procedural block ( like r1_p1 above )
(c) Only when both (a) & (b) are false, clock is inferred from default clocking block ( if it exists )