System Verilog Assertion - SVA - All the ones on the data bus should be contiguous

SystemVerilog
,
1

I am trying to write an optimal SVA Assertion to check that all the ones on a data bus are contiguous to one another.

Any advice.

Thanks in advance

2

In reply to verification_engineer_smart:
Provide an example for your requirements. Also is this for all cycles or do you have an antecedent?


bus 1011110001101   //  pass or fail? 
    011111100001010 // ? 
    Other           // PASS 
    Other           // FAIL
3

In reply to ben@SystemVerilog.us:

In reply to verification_engineer_smart:
Provide an example for your requirements. Also is this for all cycles or do you have an antecedent?


bus 1011110001101   //  pass or fail? 
011111100001010 // ? 
Other           // PASS 
Other           // FAIL

101111001101 //fail
000111100000 //pass
000000011111 //pass
000000110001 //fail

4

In reply to verification_engineer_smart:

 
// Untested, but it looks OK
   bit[15:0] q; 
  function automatic bit contig (bit[15:0] x);
      bit gota1;
      for (int i=0; i<16; i++) begin 
        if(!gota1 && x[i]==1'b1) gota1=1'b1;
        else if(gota1 && x[i]==1'b0 ) return 0; 
        else if(i==15 && (!gota1 || x[i]==1'b1)) return 1; 
      end
   endfunction

   property p_contig; 
    bit[15:0] v;
     @ (posedge clk) $rose(a) |-> (1, v=contig(q))  ##0 v;  
   endproperty 
   ap_contig: assert property(@ (posedge clk) p_contig);

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:
5

In reply to ben@SystemVerilog.us:
Updated

6

In reply to ben@SystemVerilog.us:

Thanks Ben. Will try and let you know.

7

In reply to verification_engineer_smart:
Looking at the function again, I believe that


else if(i==15 && (!gota1 || x[i]==1'b1)) return 1; // OK
// But, it can be replaced with 
else if(i==15) return 1; 
// In other words, the 
&& (!gota1 || x[i]==1'b1) seems redundant

… A though, or more a technicality, though adding this redundancy makes the ode more readable.

8

//untested
//algorithm:
//compare 2 bits at a time such as bit[0] & bit[1] and incrementally keep comparing till
//BUS_WIDTH-1
//when contiguous 1’s are observed raise the start_flag(precondition) then check for bit[i+1] =
//1 bit [i] = 0 pattern which makes it non contiguous. Then the assertion shouts when
//continuous assign gets error in pattern.

bit start_flag, err_flag;
start_flag = 0;
err_flag = 0;
genvar i;
generate
for (i = 0; i < 32; i++) begin
assign start_flag = (bit[i+1] & bit[i]) == 1? 1 : 0;
assign err_flag = (bit[i+1] & !bit[i]) == 1? 1 : 0;
end
endgenerate
assert_contiguous: assert property( @(posedge clk) disable_iff (rst) start_flag |-> err_flag );

9

In reply to Geethanand Nagaraj:
The generate is expanded at elaboration not in simulation.
My previous property did not consider the case of a “10” sequence like 000111100000 //pass
The following does it because the loop detects that 10 case, and considers it in evaluating the return value. Hopefully, I was correct in my evaluations.


   function automatic bit contig (bit[15:0] x);
      bit gota1, gota10;
      for (int i=15; i==0; i--) begin 
        case ({i==0, gota10, gota1})
         3'b000: if(x[i]==1'b1) gota1=1'b1;  // new '1'
         3'b001: if(x[i]==1'b0) gota10=1'b1; // there was a 1, new 0
         3'b010: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
         3'b011: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
         3'b100: return 1; // last bit, x==0 -> OK, no error 
         3'b101: return 1; // was a 1, NO 10, x==0000000...10 or x==000000...11-> OK 
         3'b110: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
                 else return 1; // was a 10, now new 0 -> OK 
         3'b111: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
                 else return 1; // was a 10, now new 0 -> OK 
          
        endcase
        /* if(!gota1 && x[i]==1'b1) gota1=1'b1;
        else if(gota1 && x[i]==1'b0 ) return 0; 
        else if(i==15 && (!gota1 || x[i]==1'b1)) return 1; */ 
      end
   endfunction

   property p_contig; 
    bit[15:0] v;
     @ (posedge clk) $rose(a) |-> (1, v=contig(q))  ##0 v;  
   endproperty 
   ap_contig: assert property(@ (posedge clk) p_contig);

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:
10

In reply to ben@SystemVerilog.us:

Ben

In the property, can “a” be “clk”?

Also, can you please explain this property, in some detail :

@ (posedge clk) $rose(a) |-> (1, v=contig(q)) ##0 v;

Thanks

11

In reply to verification_engineer_smart:

You need to understand the evaluation regions in Svg.
See SVA evaluation - SystemVerilog - Verification Academy

(1, v=contig(q)) ##0 v;
Am using a sequence_match item; the 1 forces the variable v to be equal to the result of the function call. I then continue the evaluation of the consequent. If v==0, then the sequence is a no match and assertion fails.
Ben systemverilog.us

12

In reply to ben@SystemVerilog.us:

This is a model with lots of debug info.


// import sva_delay_repeat_range_pkg::*;
module top; 
  timeunit 1ns/100ps;
  `include "uvm_macros.svh"
   import uvm_pkg::*;
   bit clk, a; 
   bit[15:0] q; 
   function automatic bit contig (bit[15:0] x);
      bit gota1, gota10;
      $display("%t x= %h", $realtime, x);
      for (int i=15; i>=0; i--) begin 
         if(i!=0 && !gota1 && !gota10 && x[i]==1'b1) begin 
            $display("i=%d  (i!=0 && !gota1 && !gota10 && x[i]==1'b1 gota1", i); gota1=1'b1; end // new '1'
         if(i!=0 && !gota1 && !gota10 && x[i]==1'b0) begin 
            $display("i=%d  (i!=0 && !gota1 && !gota10 && x[i]==1'b0 bull", i);  end // there was a 1, new 0
         if(i!=0 && gota1 && x[i]==1'b0) gota10=1'b1; // there was a 1, new 0
         if(gota10 && x[i]==1'b1) begin 
            $display("gota10 && x[i]==1'b1 return 0"); return 0; end // was a 10, now new 1 -> error 
         if(i==0 && !gota10)  begin 
            $display("i==0 && !gota10) return 1"); return 1; end // last bit, no 10-> OK, no error  
         if(i==0 && x[i]==1'b1) 
            begin $display("i==0 && x[i]==1'b1) return 0"); return 0; end // was a 10, now new 1 -> error 
         if(i==0 && x[i]==1'b0) begin 
            $display("i==0 && x[i]==1'b0) return 1"); return 1; end // was a 10, now new 0 -> OK 
        /*case ({i==0, gota10, gota1})
         3'b000: if(x[i]==1'b1) gota1=1'b1;  // new '1'
         3'b001: if(x[i]==1'b0) gota10=1'b1; // there was a 1, new 0
         3'b01x: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
         //3'b011: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
         3'b10x: return 1; // last bit, no 10-> OK, no error 
         //3'b101: return 1; // was a 1, NO 10, x==0000000...10 or x==000000...11-> OK 
         3'b11x: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
                 else return 1; // was a 10, now new 0 -> OK 
         //3'b111: if(x[i]==1'b1) return 0; // was a 10, now new 1 -> error 
         //       else return 1; // was a 10, now new 0 -> OK 
          
        endcase*/
      end
   endfunction

   property p_contig; 
    bit v;
     @ (posedge clk)  (1, v=contig(q), $display("v=%b", v))  ##0 v;  
     // $rose(a) |-> (1, v=contig(q))  ##0 v;  
   endproperty 
   ap_contig: assert property(@ (posedge clk) p_contig) $display("%t PASS q=%h", $realtime, $sampled(q));
                           else $display("%t FAIL q=%h", $realtime,  $sampled(q));  

   
 // when bit "a" is high then at the next cycle 
   // bit [1:0]b ==11 ##1 b==00 ##1  b=11... Continuous, 
  // suppose in between a=0 then again whenever 'a' becomes 1 then b value is 11 and then continuous same as above??

     
   initial forever #10 clk=!clk;  
  
     initial begin 
       repeat(20) begin 
           @(posedge clk);   
           if (!randomize(q, a)  with // a dist {1'b1:=1, 1'b0:=1};
           { q dist {16'b0000111100000000:=1, 16'b0000111100011000:=1}; 
       }) `uvm_error("MYERR", "This is a randomize error");
       end 
       $finish; 
      end  
endmodule

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

** 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:
13

In reply to ben@SystemVerilog.us:

Ben

q is actually a 4 bit signal and the assertion seems to be failing when q is F, after reset_n is de asserted and then becomes 1 again.

Thanks

14

In reply to verification_engineer_smart:

Show us your model.
Also, do you find a fault in the function I wrote?
Ben systemverilog.us

15

In reply to ben@SystemVerilog.us:

Ben

In any case, your latest code PASSES now. Thanks a lot for your support.
May be, there was an issue with my environment earlier.

Thanks