Legal ways to specify the leading clock in SVA

SystemVerilog
,
4

In reply to ben@SystemVerilog.us:

Hi Ben,

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.

Could you point me to the section where that is explained? As 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).

EDA link : forever vs always assertion - EDA Playground

module test;

  bit clk;
  bit a,b;
  
  default clocking @(posedge clk); endclocking
  
  always #1 clk = ~clk;

  //----------------------//
  property always_pp;
    a |-> b;
  endproperty
  
  //----------------------//
  property forever_pp;
    a |-> b;
  endproperty
  
  //----------------------//
  always @(posedge clk) begin
    always_asrt: assert property(always_pp);
  end
  
  //----------------------//
  initial begin
    forever @(posedge clk)begin
      forever_asrt: assert property(forever_pp);
    end
  end
        
  //----------------------//     
  initial begin
    #2 a=1; b=0;
    #20 $finish;
  end
        
endmodule
1 Like