Can I generate multiple SystemVerilog properties in a loop?

Question

I have two packed arrays of signals, and I need to create a property and a statement associated with it for this property, which proves that the two arrays are the same under certain conditions. I formally check, and the tool cannot prove how complete arrays are in one property, so I need to split it into separate elements. So, is there a way to generate properties for each element of the array using a loop? At the moment, my code is very detailed and difficult to navigate.

Currently my code is as follows:

... 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 how I want my code to look like this:

 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 

Answer 1

You can try declaring a property with ports so that you can reuse it for multiple statements. Then declare your statements using the generation 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 can also embed a property in a statement:

 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