$past is not working as expected in SystemVerilog

Question

I am implementing a counter in SystemVerilog. To check the proper functionality of the circuit (if the increment happened correctly), I have the assertion below:

property check_increment;
    @(posedge clk)  disable iff(!rst_) (ld_cnt && count_enb && updn_cnt)|-> ($past(data_out) == data_out-1);
endproperty
control_increment: assert property (check_increment) 
    $display("3-PASS: INCREMENT WORKS %d %t\n",data_out,$time);
else 
    $display("3-FAIL:INCREMENT DOES NOT WORK past=%d present=%d %t\n",$past(data_out,1),data_out,$time);

The simulation is shown in the picture below.

When assertion FAILS/PASSES, $past(data_out) outputs not the previous value but the value that was 2 clocks before. I understand that $past and all the values are sampled in the Preponed region, so it is logical to have the FAILS when you get the value before 2 clocks. Why when I print the values do they have difference = 2 but the assertions pass? What's the proper solution to take the previous value of the previous clock in an assertion?

`timescale 1us/1ns
module test;
logic [15:0]data_in;
logic rst_,ld_cnt,updn_cnt,count_enb,clk;
logic [15:0]data_out;

Counter counter (data_in,rst_,ld_cnt,updn_cnt,count_enb,clk,data_out);

property check_increment;
    @(posedge clk)  disable iff(!rst_) (ld_cnt && count_enb && updn_cnt)|-> ($past(data_out)+1 == data_out);
endproperty


control_increment: assert property (check_increment) $display("3-PASS: INCREMENT WORKS past=%d present=%d %t\n",$past(data_out),data_out,$time);
                else $display("3-FAIL:INCREMENT DOES NOT WORK past=%d present=%d %t\n",$past(data_out),data_out,$time);

always #10 clk = ~ clk;

initial begin
    clk = 0;
    data_in = 10;
    rst_ = 0;
    ld_cnt = 1;
    updn_cnt = 1;
    count_enb = 1;
    
    #29;
    data_in = 5;
    rst_ = 1;
    ld_cnt = 1;
    updn_cnt = 1;
    count_enb = 1;
@(posedge clk);
    
    #19
    data_in = 10;
    rst_ = 1;
    ld_cnt = 1;
    updn_cnt = 1;
    count_enb = 1;
@(posedge clk);

    #19
    data_in = 7;
    rst_ = 1;
    ld_cnt = 1;
    updn_cnt = 1;
    count_enb = 1;
    
end 
endmodule


module Counter
(input [15:0]data_in,
input rst_,ld_cnt,updn_cnt,count_enb,clk,
output logic [15:0]data_out);

logic [15:0] data;

always_ff @(posedge clk,negedge rst_) begin
    
    priority if (!rst_) data = 0;
    
    else if (!ld_cnt) data = data_in;
    
    else if(count_enb)begin
        if(updn_cnt) data = data + 1;
        else data = data - 1;
    end
end

assign data_out = data;
endmodule

I have reconstructed the question. I think $past is calculated in preponed region (Before going the the new clock). This makes it seem that $past is taking the value of 2 clocks before, when in reality it is not. — Xhulio Xhelilai, Jul 18 '22 at 13:59
What I want is a way to take the previous clock value in an assertion when the assertion starts @(posedge clk). — Xhulio Xhelilai, Jul 18 '22 at 14:00
If what I am saying for $past is correct then I think I should not see passes. — Xhulio Xhelilai, Jul 18 '22 at 14:08
Somehow, I believe I solved the issue. In the assertions i wrote |=> instead of |->. In this way, the consequent is evaluated after +1 clock. The $past gives me as expected the value before 2 clocks and the data_out is the value before 1 clock. — Xhulio Xhelilai, Jul 18 '22 at 16:51

toolic · Answer 1 · 2022-07-18T17:06:48.837

When I run your code on VCS, I see messages like:

3-PASS: INCREMENT WORKS past=    0 present=    2                50000

3-PASS: INCREMENT WORKS past=    1 present=    3                70000

3-PASS: INCREMENT WORKS past=    2 present=    4                90000

I agree that this is misleading since it shows "past" is 2 less than "present".

Change $display to $strobe. This gives the expected messages:

3-PASS: INCREMENT WORKS past=    1 present=    2                50000

3-PASS: INCREMENT WORKS past=    2 present=    3                70000

3-PASS: INCREMENT WORKS past=    3 present=    4                90000

$past is not working as expected in SystemVerilog

2 Answers2