1
\$\begingroup\$

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?

enter image description here

`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
\$\endgroup\$
4
  • \$\begingroup\$ 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. \$\endgroup\$ Jul 18, 2022 at 13:59
  • \$\begingroup\$ What I want is a way to take the previous clock value in an assertion when the assertion starts @(posedge clk). \$\endgroup\$ Jul 18, 2022 at 14:00
  • \$\begingroup\$ If what I am saying for $past is correct then I think I should not see passes. \$\endgroup\$ Jul 18, 2022 at 14:08
  • \$\begingroup\$ 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. \$\endgroup\$ Jul 18, 2022 at 16:51

2 Answers 2

0
\$\begingroup\$

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

See also: $display vs $strobe

\$\endgroup\$
0
0
\$\begingroup\$

Taking into consideration that an assertion is evaluated in the preponed region, to be able to check if the value of data_out has been incremented between to clocks the appropriate code is:

    property check_increment;
    @(posedge clk) disable iff(!rst_) (ld_cnt && count_enb && updn_cnt)|=>($past(data_out)+1 == data_out);
    endproperty
  • => This says that the consequent must be evaluated after one clock
  • $past(data_out) returns the value of the data_out before 2 clocks
  • data_out returns the value of data_out which is the value in the previous clock

If $past(data_out) = data_out - 1 is TRUE, then the assertions has passed, else has failed.

\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.