Output corruption with SVA

I’m trying basic SystemVerilog assertions. Following is dut code:


module desig (
  input clk,
  input [3:0] uop_i,
  input flush,
  output logic[3:0] uop_r
);
  
  always_ff @ (posedge clk) begin
    if (flush)
      uop_r <= 'b0;
    else  
      uop_r <= uop_i;
  end
  
  sequence c1; 
    ((flush =='b1) ##1 (uop_r=='b0));
  endsequence

  property check;
    @(posedge clk) c1;    
  endproperty

  assert property (check)  $strobe("AP | [%4t] | uop_i=%h | flush=%b | uop_r=%h | $past(uop_i)=%h", $time, uop_i, flush, uop_r, $past(uop_i, 1));
  else $error("AF | [%4t] | uop_i=%h | flush=%b | uop_r=%h | $past(uop_i)=%h", $time, uop_i, flush, uop_r, $past(uop_i, 1));

endmodule

Following is my testbench code:


module testbench;
  reg  clk;
  reg [3:0] uop_i;
  reg flush;
  wire [3:0] uop_r;

  desig dut(clk, uop_i, flush, uop_r);

  initial begin:CLOCK
	clk = 1'b0;
		forever #10 clk = ~clk;
    // repeat(500) #10 clk = ~clk;    
	end

  initial begin
    for (int i=0;i<10;i++)  begin
      uop_i = $random;
      flush = $random;
      
      $strobe("AX | [%4t] | uop_i=%h | flush=%b | uop_r=%h", $time, uop_i, flush, uop_r);
      @(posedge clk);
      $display("");
    end
    #20 $stop;
  end
endmodule

I’m running it on Questasim and following is my output:

AX | [ 0] | uop_i=4 | flush=1 | stall=1 | uop_r=x

AX | [ 10] | uop_i=3 | flush=1 | stall=1 | uop_r=0

AP | [ 30] | uop_i=5 | flush=0 | stall=1 | uop_r=0 | $past(uop_i)=4

AX | [ 30] | uop_i=5 | flush=0 | stall=1 | uop_r=0

**# ** Error: AF | [ 50] | uop_i=d | flush=0 | stall=1 | uop_r=5 | $past(uop_i)=3

Time: 50 ns Started: 50 ns Scope: testbench.dut File: D:/gdrive_upload/Work/RV_Verif/Salman/modelsim_practice/desig.sv Line: 41

AP | [ 50] | uop_i=d | flush=0 | stall=1 | uop_r=5 | $past(uop_i)=3

AX | [ 50] | uop_i=d | flush=0 | stall=1 | uop_r=5**

** Error: AF | [ 70] | uop_i=d | flush=0 | stall=1 | uop_r=d | $past(uop_i)=5

Time: 70 ns Started: 70 ns Scope: testbench.dut File: D:/gdrive_upload/Work/RV_Verif/Salman/modelsim_practice/desig.sv Line: 41

AX | [ 70] | uop_i=d | flush=0 | stall=1 | uop_r=d

** Error: AF | [ 90] | uop_i=6 | flush=1 | stall=0 | uop_r=d | $past(uop_i)=d

Time: 90 ns Started: 90 ns Scope: testbench.dut File: D:/gdrive_upload/Work/RV_Verif/Salman/modelsim_practice/desig.sv Line: 41

AX | [ 90] | uop_i=6 | flush=1 | stall=0 | uop_r=d

# AX | [ 110] | uop_i=5 | flush=1 | stall=0 | uop_r=0

AP | [ 130] | uop_i=f | flush=0 | stall=0 | uop_r=0 | $past(uop_i)=6

AX | [ 130] | uop_i=f | flush=0 | stall=0 | uop_r=0

** Error: AF | [ 150] | uop_i=8 | flush=1 | stall=0 | uop_r=f | $past(uop_i)=5

Time: 150 ns Started: 150 ns Scope: testbench.dut File: D:/gdrive_upload/Work/RV_Verif/Salman/modelsim_practice/desig.sv Line: 41

AP | [ 150] | uop_i=8 | flush=1 | stall=0 | uop_r=f | $past(uop_i)=5

AX | [ 150] | uop_i=8 | flush=1 | stall=0 | uop_r=f

AX | [ 170] | uop_i=d | flush=1 | stall=1 | uop_r=0

AP | [ 190] | uop_i=d | flush=1 | stall=1 | uop_r=0 | $past(uop_i)=8

** Note: $stop : D:/gdrive_upload/Work/RV_Verif/Salman/modelsim_practice/testbench.sv(27)

Time: 210 ns Iteration: 0 Instance: /testbench

For now, I’m only trying to verify assertion on the flush condition.

The Question is:
[*] Why clock 50 is displayed 3 times and then missing the assertions $strobe statement in clock 110. It should show assertion pass statement at 110 and display only assertion fail at 50.

In reply to muhammadsalmanafzal:
Your assertion is not correct in that you are stating that at all cycles the sequence must be true. Also, you need to display the sampled values in your strobes.


sequence c1; 
    ((flush =='b1) ##1 (uop_r=='b0));
  endsequence
 
  property check; // <<< VERY VERY POORLY WRITTEN Assertion 
    @(posedge clk) c1;    
  endproperty

  // Note the implication operator and the use of the $sampled and $realtime
  ap_check_better: assert property(@ (posedge clk) flush =='b1 |=> uop_r=='b0) 
        $strobe("AP_BETTER | [%4t] | uop_i=%h | flush=%b | uop_r=%h | $past(uop_i)=%h", 
        $realtime, $sampled(uop_i), $past(flush), $sampled(uop_r), $past(uop_i, 1));
  else $error("AF_BETTER | [%4t] | uop_i=%h | flush=%b | uop_r=%h | $past(uop_i)=%h", 
        $realtime, $sampled(uop_i), $past(flush), $sampled(uop_r), $past(uop_i, 1));

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

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

In reply to ben@SystemVerilog.us:

Thanks for your reply and sorry for my late reply. I get what you are trying to do, but it still does not explain my query about time 50 and 110. Also, with you code, I get the following output:

# AP | [  30] | uop_i=3 | flush=1 | stall=1 | uop_r=0 | $past(uop_i)=4
# AP | [  50] | uop_i=5 | flush=1 | stall=1 | uop_r=0 | $past(uop_i)=3
# AP | [ 130] | uop_i=5 | flush=1 | stall=0 | uop_r=0 | $past(uop_i)=6
# AP | [ 150] | uop_i=f | flush=1 | stall=0 | uop_r=0 | $past(uop_i)=5
# AP | [ 190] | uop_i=d | flush=1 | stall=1 | uop_r=0 | $past(uop_i)=8

Still here, time between 50 and 130 is missing, then there is a cycle miss between 150 and 190 (assuming cycle of 20).

Also, what is wrong with

((flush =='b1) ##1 (uop_r=='b0))

. From my understanding, it states that “On the current clock cycle(take 30), check for flush==1, if it is true, then on the next clock cycle(40), check for uop_r==0. If uop_r==0 is true, then at 40, assertion should pass.”

Am I missing something in regards to sampled value, and updated value due to which I’m not getting correct assertion results?

In reply to muhammadsalmanafzal:

((flush =='b1) ##1 (uop_r=='b0))
From my understanding, it states that “On the current clock cycle(take 30), check for flush==1, if it is true, then on the next clock cycle(40), check for uop_r==0. If uop_r==0 is true, then at 40, assertion should pass.”

Not quite true, but partially. It also states that "“On the current clock cycle(take 30), if flush==0 then the assertion fails. DON’T even bother to check the rest of the sequence”. What you need is vacuity, and this is where the implication operators }-> and |=> come in.
flush =='b1 |=> uop_r=='b0) says
On the current clock cycle(take 30), check for flush==1, if it is true, then on the next clock cycle(40), check for uop_r==0. If uop_r==0 is true, then at 40, assertion should pass. However, if the antecedent is a NO MATCH (i.e., the sequence flush==0) then the property is vacuous. From my book, in the Definition section:

vacuity: (see 3.1, 3.9) A property is vacuous if it lacks serious purpose. Vacuity rules are usually applied when implication operator is used. A property succeeds vacuously if the antecedent is FALSE. A property succeeds non-vacuously only if the consequent of the implication contributes to its success. Many applications have a triggering event that causes the thread to start (in the antecedent), and if the triggering event does not occur (i.e., if false), then there is no need to further evaluate the thread (i.e., the rest of the property for that cycle), which is then considered vacuously true. Also see Success and vacuity and Fail and vacuity. .

… between 50 and 130 is missing,

It is vacuous at this times.

You need to study SVA, you are missing a lot of concepts.

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

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

In reply to ben@SystemVerilog.us:
Thanks for the great elaboration. I’ll look into the concepts.

In reply to ben@SystemVerilog.us:

I have studied about the sampled value of assertion and the preponed, observation and postponed regions too. I understand that if (e.g.) cStart = 1 and posedge clk change at the same time, the sampled value of cStart in the “preponed region” will be equal to “zero” and not “one”.

Just a quick question… What if instead of going into the abyss of this, I don’t change values of input at the same time as posedge clk is triggered, what if I change values at the previous negedge of clk or use @(negedge clk) in my property? Is this a good practice professionally to check the functionality using assertions?

In reply to muhammadsalmanafzal:

What if instead of going into the abyss of this, I don’t change values of input at the same time as posedge clk is triggered, what if I change values at the previous negedge of clk or use @(negedge clk) in my property? Is this a good practice professionally to check the functionality using assertions?

No it is NOT a good practice because 1) it is not necessary, and 2) it is misleading as to how the design operates.
Also see my diagram at


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

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: