$past with gating signal assertion

SystemVerilog
1

I am trying to comprehend how the assertion is passing at certain time stamps in my simulation. Here’s the code I am running -

//-------------------------------------------------------------------------
//						www.verificationguide.com
//-------------------------------------------------------------------------
module asertion_ex;
  bit clk,a,b,c;
  
  always #5 clk = ~clk; //clock generation
  
  //generating 'a'
  initial begin 
        a=1; b=1;
    #15 a=0; b=0; c=$urandom();
    #10 a=1; b=0; c=$urandom();
    #10 a=0; b=0; c=$urandom();
    #10 a=1; b=1; c=$urandom();
    #10; a=$urandom(); b=$urandom(); c=$urandom();
    #10; a=$urandom(); b=$urandom(); c=$urandom();
    #10; a=$urandom(); b=$urandom(); c=$urandom();
    #10; a=$urandom(); b=$urandom(); c=$urandom();
    #10; a=$urandom(); b=$urandom(); c=$urandom();
    $finish;
  end
  
  property p;
    @(posedge clk) b |-> ($past(a,2,c) == 1);
  endproperty
  
  //calling assert property
  a_1: assert property(p)  $display("PASS at %t", $realtime());
    
  //wave dump
  initial begin 
    $dumpfile("dump.vcd"); $dumpvars;
  end
endmodule

Attaching the waveform for one of my runs on EDAP below -

past_assertion
past_assertion1864×233 46.4 KB

The simulation says that the assertion is passing at 55ns, 65ns and 85ns. Here’s what I think is happening at each of these timestamps.

  • At 55ns: ‘b’ is high. 2 clocks earlier (i.e at 35ns) ‘c’ has transitioned to ‘1’ and ‘a’ is high. I thought the simulator would see ‘c’ as 0 at 35ns, but since the assertion has passed I believe the simulator takes the post-transition value of c (i.e, 1). But if this is the expected behavior of the simulator, then it contradicts the result seen at 65ns and 85ns (mentioned below).

  • At 65ns: ‘b’ is high. 2 clocks earlier (i.e at 45ns) ‘c’ is transitioning to ‘0’ and ‘a’ is low. Why did the assertion pass when ‘a’ is low?

  • At 85ns: ‘b’ is high. 2 clocks earlier (i.e at 65ns) ‘c’ is transitioning to ‘0’ and ‘a’ is seen as high. The assertion passes.

Can anyone please explain how the simulator sees the value of the gating signal (i.e ‘c’) and also ‘a’ in the above concurrent assertion.

2

Two problems with the code in your question.

We cannot reproduce your issues using random values. Different tools, or different versions of the same tool can produce divergent results. Please edit your testcase giving the actual values needed.

Because of the #15 in the initial block, the blocking assignments to a, b, and c coincide with the posdege clk. This makes it difficult to understand the timing of the gating signal. It is also a general stimulus problem that creates race conditions between the testbench and RTL. Offset your stimulus to the negedge or some delay that moves it away from the active edge of the clock.

3

$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
expression2 is used as a gating expression for the clocking event. The value returned for $past is expression1 sampled number_of_ticks gated cycles ago. In other words, for: $past(data, 3, load_enable, @(posedge clk)) the returned value is the sampled value of data in the 3rd prior cycle in which load_enable was true.

// Edit code - EDA Playground code
// EPWave Waveform Viewer wave


module asertion_ex;
bit clk,a,b,c;
int p1, f1;  
always #5 clk = ~clk; //clock generation

//generating 'a'
initial begin 
      a=1; b=1;
  #17 a=0; b=1; c=0;
  #10 a=1; b=1; c=1;
  #10 a=0; b=1; c=0;
  #10 a=1; b=1; c=1;
  #10 a=0; b=1; c=0;
  #10 a=1; b=1; c=1;
  #10 a=0; b=1; c=0;
  #10 a=1; b=1; c=1;
  #100;
  /*#10; a=$urandom(); b=$urandom(); c=$urandom();
  #10; a=$urandom(); b=$urandom(); c=$urandom();
  #10; a=$urandom(); b=$urandom(); c=$urandom();
  #10; a=$urandom(); b=$urandom(); c=$urandom();
  #10; a=$urandom(); b=$urandom(); c=$urandom(); */
  $finish;
end

property p;
  @(posedge clk) b |-> ($past(a,2,c) == 1);
endproperty

//calling assert property
a_1: assert property(p) p1++; else f1++;  // $display("PASS at %t", $realtime());
  
//wave dump
initial begin 
  $dumpfile("dump.vcd"); $dumpvars;
  
end
endmodule
4

Added annotated image at

I cold not upload the image here, sorry!

5

Yes, agreed with what you said regarding $urandom(). I have removed the $urandom() and assigned values to a,b,c. And also I have made sure that any of these 3 signals do not get driven at the rising edge of ‘clk’.

Here’s the updated code -

module asertion_ex;
  bit clk,a,b,c;
  
  always #5 clk = ~clk; //clock generation
  
  //generating 'a'
  initial begin 
        a=1; b=1;
    #17 a=0; b=0; c=1;
    #10 a=1; b=0; c=1;
    #10 a=0; b=0; c=0;
    #10 a=1; b=1; c=0;
    #10; a=0; b=1; c=1;
    #10; a=1; b=1; c=1;
    #10; a=0; b=1; c=0;
    #10; a=0; b=1; c=0;
    #10; a=1; b=1; c=1;
    $finish;
  end
  
  property p;
    @(posedge clk) b |-> ($past(a,2,c) == 1);
  endproperty
  
  //calling assert property
  a_1: assert property(p)  $display("PASS at %t", $realtime());
    
  //wave dump
  initial begin 
    $dumpfile("dump.vcd"); $dumpvars;
  end
endmodule

I ran this on EDAP and the simulation prints say that the above assertion has passed at 75ns. How can it pass at 75ns if ‘c’ is low 2 clock cycles prior (i.e at 55ns)?

Attached is a snapshot of my new run -

past_assertion
past_assertion1854×179 37.9 KB

6

$past(a,2,c) says take the sampled value of a from the previous 2 clock cycles earlier when c was true. At time 75, those 2 previous cycles came at time 65 and time 35. At time 35, a is 1'b1.

7

If the expression 2 is false in
$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
in original poster’s case it is c, will property
b |-> $past(a,2,c) fail ?

Thanks

8

I had misunderstood how $past(a,2,c) evaluates to. Thanks for clarifying.

9

Thanks for clarifying. Appreciate it!

10

@VE1 $past looks at expression2 at each previous clock tick. If there are not enough clock ticks when c is true (as in the attempts at time 25 and 35) $past returns the default initial value of a, which is 0. So the assertion fails.