4

信号の 2 つのパック配列があり、特定の条件下で 2 つの配列が同一であることを証明するプロパティとそのプロパティに関連付けられたアサーションを作成する必要があります。私は正式に検証していますが、ツールは 1 つのプロパティで両方の完全な配列を証明できないため、個々の要素に分割する必要があります。ループを使用して配列の各要素のプロパティを生成する方法はありますか? 現時点では、私のコードは非常に冗長でナビゲートが困難です。

私のコードは現在次のようになっています。

...
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 に答える