Regarding assertion issue when A != $past(A)

SystemVerilog
1

Hi,

I have an assertion which checks, at every clock, if a fall on Sig_A, Sig_B is changed.

my assertion code is

//--------------------------
module sample_checker(
input logic clk,
input logic enable,
input logic Sig_A,
input logic Sig_B
);

property p_Sig_B;
@(posedge clk) disable iff(!enable)
$fell(Sig_A) |-> (Sig_B != $past(Sig_B));

endproperty : p_Sig_B

assert_p_Sig_B : assert property (p_Sig_B);

endmodule
//------------------------------

But after simulation, I am seeing the assertion is hit only onetime(for very first occurance), though there were many falling edge of Sig_A.

Just for checking the assertion behaviour, I changed the assertion to Sig_B == $past(Sig_B), like below
$fell(Sig_A) |-> (Sig_B == $past(Sig_B));

Then I am observing that assertion is hitting for every falling edge of Sig_A and all are failing as expected.
I am confused, why “!=” case is not working and hitting only once ?

I worte the assertion in different way and solved the issue. But I would like to know why the above code was not working.

Any help would be appreaciated.

2

In reply to abhilashmgopal:
The assertion $fell(Sig_A) |-> (Sig_B != $past(Sig_B)); is correct and has no issues.
Below is link to code and simulation results.
http://systemverilog.us/vf/nota.sv

1196×263 7.03 KB


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    logic clk=1'b0, enable=1'b0, Sig_A=1'b0, Sig_B=1'b0;
    event e; 
	default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  

    always_ff  @(posedge clk)  begin 
       if($fell(Sig_A)) -> e;
    end 
    
    property p_Sig_B;
        @(posedge clk) disable iff(!enable) 
        $fell(Sig_A) |-> (Sig_B != $past(Sig_B)); 
    endproperty : p_Sig_B
    
    assert_p_Sig_B : assert property (p_Sig_B);
    
    initial begin 
        bit va, vb; 
        @(posedge clk) enable <= 1'b1;
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(va, vb)  with 
            { va dist {1'b1:=1, 1'b0:=3};
            vb dist {1'b1:=1, 1'b0:=2};      
        }) `uvm_error("MYERR", "This is a randomize error")
        Sig_A <= va; 
        Sig_B <= vb;
    end 
    $stop; 
end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
3

In reply to ben@SystemVerilog.us:

Thanks Ben,
I analyzed your wave snapshot and code. There are some differences with mine,
Let me post my wavesnapot here. Could you please check this

4

In reply to abhilashmgopal:

I am sorry, how to share my snapshot here ?

5

In reply to abhilashmgopal:
On differences, I would expect different waveforms because every tool may use a different algorithm in the implementation of the randomize function. But the assertion results for the subjected conditions will be the same.

To share your images, put them in a place where you can get a link.
You can use a private site where you can upload them. You can also use google photo and get from google photo an icon that allows you to share an image. Here is an example of a pleasant photo https://photos.app.goo.gl/Rex3E9QrKxnCBgzc9
There are other sites that allow uploads.
Ben

6

In reply to ben@SystemVerilog.us:

Thanks Ben for the quick response.

Here are my wave snapshots,

1)$fell(Sig_A) |-> (Sig_B != $past(Sig_B));
image1.JPG

2)$fell(Sig_A) |-> (Sig_B == $past(Sig_B));
image2.JPG

3)zoom in
zoom in

Thanks,
Abhi

7

In reply to ben@SystemVerilog.us:

Hi Ben,

I did further investigation.

  1. At first, I used the same code which Ben shared above.
    I am seeing similar issue. For some of the $fell, event “e” is happening. But assertion is not hitting.

Ben’s_code_wavesanpshot

  1. Then, I modified Ben’s code slightly to generate Sig_A and Sig_B similar to my case.

 import uvm_pkg::*; `include "uvm_macros.svh"
module top;
    logic clk=1'b0, enable=1'b0, Sig_A=1'b0, Sig_B=1'b0;
    event e;
        default clocking @(posedge clk);
    endclocking
    initial forever #10 clk=!clk;

    always_ff  @(posedge clk)  begin
       if($fell(Sig_A)) -> e;
    end

    property p_Sig_B;
        @(posedge clk) disable iff(!enable)
        $fell(Sig_A) |-> (Sig_B != $past(Sig_B));
    endproperty : p_Sig_B

    assert_p_Sig_B : assert property (p_Sig_B);


    initial begin
        bit va, vb;
        @(posedge clk) enable <= 1'b1;
        repeat(200) begin
            @(posedge clk);     //----Changed Ben's code here. Sig_A and Sig_B to make it similar to my case
            Sig_A <= 1'b1;
            @(posedge clk);
            Sig_A <= 1'b0;
            Sig_B <= !Sig_B;
        end
    $stop;
    end
 endmodule

The result is same.
a) When $fell(Sig_A) |-> (Sig_B != $past(Sig_B))
Assertion hit only one time, eventhough there are many $fell events

 [modified_code_wavesnapshot1](https://photos.app.goo.gl/1AW6QR7hmkfzuWm17)

b) $fell(Sig_A) |-> (Sig_B == $past(Sig_B))
Assertion hit at all the $fell events.

modified_code_wavesnapshot2

Thanks,
Abhi

8

In reply to abhilashmgopal:
Because of the $past requires to a good sampled value of the data in the last clock you need to add a ##1 in the antecedent. Thus,


property p_Sig_B;
        @(posedge clk) disable iff(!enable) 
        ##1 $fell(Sig_A) |-> (Sig_B != $past(Sig_B)); 
endproperty : p_Sig_B

All that means is that the assertions start one clock after enable==1.
If you need to check values of variables when enable==1 then you’ll need additional assertions for that one test case (i.e., @rose(enable).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
9

In reply to ben@SystemVerilog.us:

Thanks Ben.
with ##1 at antecedent it is working fine.

Because of the $past requires to a good sampled value of the data in the last clock you need to add a ##1 in the antecedent.

Is it a constraint for $past usage ?
Also my expectation was, $fell at antecedent should detect irrespective of consequent part.
So, if $past sampling was not proper, then assertion is expected to fail. But here, assertion itself was not hitting.

If possible, could you please share me some more details.

Thanks,
Abhi

10

In reply to abhilashmgopal:

I don’t understand your issues when you say

a) When $fell(Sig_A) |-> (Sig_B != $past(Sig_B)) 
Assertion hit only one time, eventhough there are many $fell events

I ran your modified code, and it works as expected.

When I proposed ##1 $fell(Sig_A) |-> (Sig_B != $past(Sig_B)); it’s because you need to handle the initial state case. On the first clocking event, $past(variable) == initial value of that variable, and that can cause unexpected errors.

1800: When these functions (e.g.,**$past, $changed, $stable**) are called at or before the simulation time step in which the first clocking event occurs, the results are computed by comparing the sampled value of the expression with its default sampled value (

s it a constraint for $past usage ?

$past is just a function that returns the value of the precedent clocking event; there is no constraint.

Also my expectation was, $fell at antecedent should detect irrespective of the consequent part.

True. The antecedent is evaluated first, and if true the consequent is triggered.

So, if $past sampling was not proper, then the assertion is expected to fail. But here, assertion itself was not hitting.[

In your particular testbench the past data of sigb was correctly sampled as it is far from the 1st clocking event. Again, reread what 1800 says about the $past before the simulation time step.

Read my paper SVA Alternative for Complex Assertions at
https://s3.amazonaws.com/verificationhorizons.verificationacademy.com/volume-14_issue-1/complete-issue/stream/volume14-issue1-verification-horizons-publication-lr.pdf
In that paper, I demonstrate how assertions can be emulated with tasks and fork join_none of those tasks. Essentially, at every clocking event you fire an automatic task that represents the property.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
11

In reply to ben@SystemVerilog.us:

Thanks Ben,

I don’t understand your issues when you say
a) When $fell(Sig_A) |-> (Sig_B != $past(Sig_B))
Assertion hit only one time, eventhough there are many $fell events

Could you please check modified_code_wavesnapshot1 which I shared in my previous response.
In this snapshot, you can see event “e” and “assert_p_Sig_B”.
assert_p_Sig_B is occured only one time. Also in the assertion log, it shows assertion finish count is 1. But I expect this assertion should finish every falling edge of Sig_A. So I am expecting assertion total count = number of Sig_A fall edge.
I was asking, why the assertion finished only one time?

I ran your modified code, and it works as expected.

When I ran the modified code (without ##1 at antecedent), it is not working as expected.
refer the same modified_code_wavesnapshot1
But when I added ##1 at antecedent, it is working. I mean,total assertion hit count is as expected(number of Sig_A falling edge).

Thanks,
Abhi

12

In reply to abhilashmgopal:

Try running your simulation in edaplayground.com and add $display messages in the action blocks for pass/fail.
Ben