4

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
Greg
  • 18,111
  • 5
  • 46
  • 68
WestHamster
  • 1,297
  • 2
  • 11
  • 16
  • Can you post some code? Is this all in a procedural context? –  Oct 17 '12 at 18:25
  • The properties and assertions are within a module. I think you might have to put for loops in an always block which I don't think you can put the properties in. – WestHamster Oct 18 '12 at 13:09

2 Answers2

14

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
  • That works great. Thank you very much. A follow up problem I now have is how to label these generated properties: the assertions are failing, but I can't work out which assertion has been violated by an assertion. – WestHamster Oct 19 '12 at 12:51
  • UPDATE: I can now work out what the assertion name/number is in my formal tool. However if you know of any useful assertion naming tip then I'm all ears. – WestHamster Oct 19 '12 at 13:03
  • 1
    If you want more control over reporting, you could add an action block to the assertion. Something like `assert property (...) else $display("Assertion %m failed");` If you want to use _label :_ to refer to the assertion, I recommend adding _begin : array_name ... end_ to the outer generate loop so the tool doesn't use genblkX[i]. –  Oct 19 '12 at 15:25
0

You can also try the same thing with a macro.

/*Start of macro*/
`define bb_prop(Num1, Num2) \
    property bb_``NUM1``_``NUM2``_p; \
      @(posedge clk) \
      bb_seq |=> bb_exp [``NUM1``` ][``NUM2``] == bb_rtl [``NUM1``` ][``NUM2``]; \
    endproperty \
 bb_prop_``NUM1``_``NUM2``_assert: assert property (bb_``NUM1``_``NUM2``_p) 
/* End of macro*/

`bb_prop(3,4) 
`bb_prop(3,5)
`bb_prop(3,6)
aravind_sindhey
  • 1