我可以在循環中生成多個SystemVerilog屬性嗎？

我有兩個打包的信號數組，我需要爲該屬性創建一個屬性和關聯的斷言，證明這兩個數組在特定條件下是相同的。我正式驗證並且該工具無法在單個屬性中證明全部數組，因此我需要將它分解爲單個元素。那麼有沒有一種方法可以使用循環爲數組的每個元素生成屬性？目前我的代碼非常冗長，很難瀏覽。我可以在循環中生成多個SystemVerilog屬性嗎？

我的代碼目前看起來是這樣的：

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

來源

2012-10-17 WestHamster

你可以張貼一些代碼？這全都在程序上下文中嗎？ – 2012-10-17 18:25:39

屬性和斷言在模塊內。我想你可能需要在一個總是阻塞的地方放置循環，我認爲你可以放置這些屬性。 – WestHamster

你可以嘗試用端口聲明屬性，以便您可以重複使用它進行多重斷言。然後使用生成循環聲明你的斷言。

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-18 18:11:40

這很好。非常感謝你。我現在遇到的後續問題是如何標記這些生成的屬性：斷言失敗，但我無法確定斷言違反了哪個斷言。 – WestHamster

更新：現在我可以計算出我的正式工具中的斷言名稱/編號。但是，如果你知道任何有用的斷言命名提示，那麼我都是耳朵。 – WestHamster

如果您想要更好地控制報告，您可以將一個操作塊添加到斷言中。類似'assert property（...）else $ display（「Assertion％m failed」）;'如果你想使用_label：_來引用斷言，我建議將_begin：array_name ... end_添加到外部生成循環，因此該工具不使用genblkX [i]。 – 2012-10-19 15:25:19

我可以在循環中生成多個SystemVerilog屬性嗎？

回答

相關問題