propertiesverilogsystem-verilogformal-verificationsystem-verilog-assertions

Can I generate a number of SystemVerilog properties within a loop?


I have two packed arrays of signals and I need to create a property and associated assertion for that property that proves that the two arrays are identical under certain conditions. I am formally verifying and the tool cannot prove both full arrays in a single property, so I need to split it up into individual elements. So is there a way I can generate a properties for each element of the array using a loop? At the moment my code is very verbose and hard to navigate.

My code currently looks like this:

...
property bb_3_4_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][4] == bb_rtl [3][4] ;
endproperty

property bb_3_5_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][5] == bb_rtl [3][5] ;
endproperty

property bb_3_6_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][6] == bb_rtl [3][6] ;
endproperty
...

...
assert_bb_3_4: assert property (bb_3_4_p);
assert_bb_3_5: assert property (bb_3_5_p);
assert_bb_3_6: assert property (bb_3_6_p);
...

This is sort of how I'd like my code to look like:

for (int i = 0; i < 8; i++) 
  for (int j = 0; j < 8; j++) 
  begin   
     property bb_[i]_[j]_p;
        @(posedge clk)
           bb_seq  
           |=>     
           bb_exp [i][j] == bb_rtl [i][j] ;
     endproperty
     assert_bb_[i]_[j]: assert property (bb_[i]_[j]_p);
  end     

Solution

  • You might try declaring the property with ports so you can reuse it for multiple assertions. Then declare your assertions using a generate loop.

    module
    ...
    property prop1(signal1,signal2); 
      @(posedge clk)
         bb_seq  
         |=>     
         signal1 == signal2 ;
    endproperty
    ...
    generate
    for (genvar i = 0; i < 8; i++) 
      for (genvar j = 0; j < 8; j++) 
        begin : assert_array
        assert property (prop1(bb_exp[i][j],bb_rtl[i][j]));
        end
    endgenerate
    ... 
    endmodule
    

    You could also inline the property in the assertion:

    module
    ...
    generate
    for (genvar i = 0; i < 8; i++) 
      for (genvar j = 0; j < 8; j++)
        begin : assert_array
        assert property (@(posedge clk) bb_seq |=> bb_exp[i][j] == bb_rtl[i][j]);
        end
    endgenerate
    ...
    endmodule