SVA:Clock gating during SV assertion

Question

I have an SV assertion which checks the property as below

propert my_property;
@(posedge clk) disable iff(reset) $rose(halt) ##0 ((rx_prio) > (expec_prio)) ##[0:$] $rose(rdy) |-> ##[1:100] (my_prio[rx_prio]==1'b1);
endproperty:my_property

I have the assertion as below:

MY_PROPERTY_CHECK:assert property (my_propert)
else
$error;

Here, the scenario is that, the antecedent is true and the consequent is checked between 1 & 100 clock cycles. After the antecedent, the clock is stopped due to clock gating for some time and then the clock starts ticking again. The signal my_prio[rx_prio] is asserted after the clock gating but again within 100 clock cycles. But I still get the assertion failure.

Not able to figure out the issue of failure. Does the clock gating in between the assertion check has an issue? Or any other reason failure? Thanks.

Answer 1

There might be many threads starting. Try using local variables with display statements below. See IEEE Std 1800-2012 § 16.10 Local variables

propert my_property;
  static int prop_cnt=0; // shared
  local  int prop_id; // Note: some require the "local", other need it omitted
  @(posedge clk) disable iff(reset) 
    ($rose(halt) ##0 ((rx_prio) > (expec_prio)),
        prop_id=prop_cnt++,
        $display("Spawn prop_id:%0d prop_cnt:%0d @ %0t %m",
                   prop_id,prop_cnt,$time) )
    ##[0:$] ($rose(rdy),
        $display("Trigger prop_id:%0d prop_cnt:%0d @ %0t %m",
                     prop_id,prop_cnt,$time) )
    |-> ##[1:100] (my_prio[rx_prio]==1'b1,
        $display("Pass prop_id:%0d prop_cnt:%0d @ %0t %m",
                     prop_id,prop_cnt,$time) );
endproperty : my_property

If you see Spawn-Spawn-Trigger, or Spawn-Trigger-Trigger, our anything outside of expected (i.e. Spawn-Triger-Pass) then there are unexpected threads.

If this is the case, then look into IEEE Std 1800-2012 § 16.9.8 First_match operation

first_match(
    $rose(halt) ##0 ((rx_prio) > (expec_prio)) ##[0:$] $rose(rdy),
      $display("Spawn-Trigger prop_id:%0d prop_cnt:%0d @ %0t %m",
                   prop_id,prop_cnt,$time)

) |-> // ...

OR § 16.9.10 Sequence contained within another sequence

(
    ( $rose(halt) ##0 ((rx_prio) > (expec_prio)) ) within $rose(rdy)[->1],
      $display("Spawn-Trigger prop_id:%0d prop_cnt:%0d @ %0t %m",
                   prop_id,prop_cnt,$time)
) |-> // ...

You might want to create a sequence for the trigger.