Using $past for range of cycles

SystemVerilog
1

Hello,
I am trying to write a assertion for the below scenario.

A box has 4 inputs (a,b,c,d) and a single output (ack). We need to write an assertion to make sure when output (ack) is asserted, a and b and c and d should have asserted (in any order) in the last 4 cycles.

Below is my try: I want to specify the range in the $past, can someone review the code and let me know?



module tb;
  
  bit clk,ack;
  bit req[4];
   default clocking @(posedge clk); 
     endclocking
     initial forever #10 clk=!clk; 
  
  bit was_a_req, was_b_req,was_c_req,was_d_req;
     always  @(posedge clk) begin 
       if(was_a_req)  req[0] <= 1'b1; 
       if(was_b_req)  req[1]  <= 1'b1;
       if (was_c_req) req[2] <= 1'b1;
       if (was_d_req) req[3] <=1;
     end 
 
       ap_valid_req: assert property(@ (posedge clk)  
                                     $rose(ack) |-> $past((req[3] & req[2] & req[1] & req [0]),4)) $display ("Assertion passed",$time);      
 
  
         initial begin
              $dumpfile ("hello.vcd");
           $dumpvars (0,tb);
            end
         
         
          initial begin 
     
        repeat(200) begin 
          repeat(1) @(posedge clk)#1;   
          if (!randomize(was_a_req,was_b_req,was_c_req,was_d_req,ack) with
              
             { was_a_req dist { 1'b1:=1,1'b0:=1};
               was_b_req dist { 1'b1:=1,1'b0:=1};
               was_c_req dist { 1'b1:=1,1'b0:=1};
               was_d_req dist { 1'b1:=1,1'b0:=1};
               ack dist { 1'b1:=1,1'b0:=1};
               
               
              
              }) `uvm_error("MYERR", "This is a randomize error");
        end 
        $stop; 
   end  
         
endmodule
2

In reply to rag123:
You need to consider the best structure for your support logic.
In this case, to test for a a past of a, b, c, d, you can use a 4-bit shift register where at every clock you do a shift-right with the input=OR(a, b, c, d). Thus,


 bit a, b, c, d;  
  bit[3:0] was_abcd;  // the shift reg 
  always  @(posedge clk) begin 
        if(a || b || c || d) was_abcd <= {1'b1, was_abcd[3:1]}; 
        else was_abcd <= {1'b0, was_abcd[3:1]};  
  end 
 
  ap_valid_req: assert property(@ (posedge clk)  
                     $rose(ack) |-> was_abcd >= 1) $display ("Assertion passed",$time);

The testbench, modify as needed.


/ A box has 4 inputs (a,b,c,d) and a single output (ack). 
// We need to write an assertion to make sure when output (ack) is asserted, 
// a and b and c and d should have asserted (in any order) in the last 4 cycles. w?

module tb;
    `include "uvm_macros.svh"
    import uvm_pkg::*;
  bit clk,ack;
  bit a, b, c, d;  
  bit[3:0] was_abcd; 

   default clocking @(posedge clk); 
     endclocking
     initial forever #10 clk=!clk; 
 
    
     always  @(posedge clk) begin 
        if(a || b || c || d) was_abcd <= {1'b1, was_abcd[3:1]}; 
        else was_abcd <= {1'b0, was_abcd[3:1]};  
     end 
 
    ap_valid_req: assert property(@ (posedge clk)  
                     $rose(ack) |-> was_abcd >= 1) $display ("Assertion passed",$time);      
 
 
         initial begin
              $dumpfile ("hello.vcd");
           $dumpvars (0,tb);
            end
 
 
          initial begin 
 
        repeat(200) begin 
          repeat(1) @(posedge clk)#1;   
          if (!randomize(a, b,c, d, ack) 
              ) `uvm_error("MYERR", "This is a randomize error");
        end 
        $stop; 
   end  
 
endmodule

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

//untested
//Pipelining may solve but may not be the best solution
//algorithm:
//in past 4 cycles at least once the a && b && c && d should be 1 to satisfy your problem //statement.
reg [3:0]pipe1;
reg [3:0]pipe2;
reg [3:0]pipe3;
reg [3:0]pipe4;
always @posedge clk begin
if(rst) begin
pipe1 <= 0;
pipe2 <= 0;
pipe3 <= 0;
pipe4 <= 0;
end else begin
pipe1 <= {a,b,c,d};
pipe2 <= pipe1;
pipe3 <= pipe2;
pipe4 <= pipe3;
end
end
property p_ack_check;
((pipe1[0] | pipe2[0] | pipe3[0] | pipe4[0]) &&
(pipe1[1] | pipe2[1] | pipe3[1] | pipe4[1]) &&
(pipe1[2] | pipe2[2] | pipe3[2] | pipe4[2]) &&
(pipe1[3] | pipe2[3] | pipe3[3] | pipe4[3])) |-> (ack == 1);
endproperty

assert_abcd: assert property @posedge(clk) disable_iff rst p_ack_check;