SVA

I want to code an assertion: the condition is at every posedge of clk signal, if a signal named fif0_full is set, a vector signal [31:0] tag_ram should not have any of its bits changing from 1 to 0.

In reply to 100rabhh:

Hi,
I firmly believe it’s related to an array of SVA concept. In this case, I would prefer to go with the generate-block idea.


property p1 (logic a, logic b);
@(posedge clk) a |-> $past(b) && !b ;
endproperty

genvar i;

generate 
for(i=0;i<32;i=i+1)
begin:coding
assert property(p1(fifo_full,tag_ram[i]))
$display("Okay");
else 
$display("Error seen at i = ",%0d);
end
endgenerate

Concept - at the same time we are dealing with 32 signals. A naive approach would be creating 32 assertions. The best way would be to create for loop and pass the values of each tag_ram bit as one of the arguments. All of them should happen at the same time. As per knowledge, it is possible with the help of generate-block.

Please run it with your code and let me know if it’s okay or not.

In reply to Shubhabrata:
thanks for the reply, this would work, I was thinking something like $changed could save the hastle of generate block, but $changed would mean any change in the vector.

In reply to 100rabhh:

The generate creates many assertions, and in this case, might make it hard to debug, particularly id you have to display in the waveform window 32 individual assertions.
You can use a function: Edit code - EDA Playground


module top;
   // 01   10  new
   //      01  past
   //                new >  past 
//  vector signal [31:0] tag_ram should not have any of its bits changing from 1 to 0
// i.e., $past was 1, it is now 0 

  bit[31:0] a, err; 
bit clk, cond=1; 
function automatic bit f1to0(bit[31:0] w, past);
   bit rtn=1; 
   for (int i=0; i<=31; i++ ) begin
     if(past[i] > w[i]) rtn= 0;
   end
   return rtn;  
endfunction
property p_no1to0;
   bit[31:0] v;
  (1, v=f1to0(a, $past(a))) ##0 v; 
endproperty 
   
ap_no1to0: assert property( @(posedge clk) cond |-> p_no1to0)
    else err=err+1;   
  initial forever #10 clk = !clk;
  initial begin
    $dumpfile("dump.vcd"); $dumpvars; 
    @(posedge clk) a<=0;
    @(posedge clk) a<=1;
    @(posedge clk) a<=0;
    @(posedge clk) a<=32'h00ff00ff;
    @(posedge clk) a<=32'h00001100; 
    repeat (3) @(posedge clk) a<=0;
    $finish;
  end
endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog