4

我有两个打包的信号数组，我需要为该属性创建一个属性和相关的断言，以证明这两个数组在某些条件下是相同的。我正在正式验证，该工具无法证明单个属性中的两个完整数组，因此我需要将其拆分为单个元素。那么有没有一种方法可以使用循环为数组的每个元素生成一个属性？目前，我的代码非常冗长且难以导航。

我的代码目前如下所示：

...
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);
...

这就是我希望我的代码看起来像的样子：

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
4

2 回答 2

14

您可以尝试使用端口声明该属性，以便可以将其重用于多个断言。然后使用生成循环声明您的断言。

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

您还可以在断言中内联该属性：

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
于 2012-10-18T18:11:40.090 回答
0

您也可以使用宏尝试相同的操作。

/*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)
于 2019-10-23T12:34:54.320 回答