Yosys邏輯循環虛假檢測

我一直在測試yosys的一些用例。版本：Yosys 0.7 + 200（GIT SHA1 155a80d，GCC-6.3 6.3.0 -fPIC -Os）Yosys邏輯循環虛假檢測

我寫了一個簡單的塊，其格雷碼轉換爲二進制：

module gray2bin (gray, bin); 

parameter WDT = 3; 

input [WDT-1:0] gray; 
output [WDT-1:0] bin; 

assign bin = {gray[WDT-1], bin[WDT-1:1]^gray[WDT-2:0]}; 

endmodule

這是一個可接受的和verilog中的有效代碼，並且沒有循環。它通過編譯和綜合，沒有任何其他工具的警告。但是，當我在yosys運行下命令：

read_verilog gray2bin.v 
scc

我得到一個邏輯循環中發現：

Found an SCC: $xor$gray2bin.v:11$1 
Found 1 SCCs in module gray2bin. 
Found 1 SCCs.

下一個代碼，相當於，通過檢查：

module gray2bin2 (
    gray, 
    bin 
); 

parameter WDT = 3; 

input [WDT-1:0] gray; 
output [WDT-1:0] bin; 

assign bin[WDT-1] = gray[WDT-1]; 

genvar i; 
generate 
    for (i = WDT-2; i>=0; i=i-1) begin : gen_serial_xor 
      assign bin[i] = bin[i+1]^gray[i]; 
    end 
endgenerate 

endmodule

我是否缺少某種標誌或合成選項？

來源

2017-06-29 EEliaz

用字寬的運營商這個電路顯然有一個循環（與yosys -p 'prep; show' gray2bin.v生成）：

你要合成電路門級表示得到一個無環路的版本（與yosys -p 'synth; splitnets -ports; show' gray2bin.v生成，調用splitnets只是有更好的可視化）：

來源

2017-06-30 12:36:19 CliffordVienna

感謝您的快速響應！雖然我不確定它有幫助 - 我的主要興趣是Yosys的FV功能。 SMT2後端給出「錯誤：發現模塊中的邏輯循環」消息。是否有可能向SMT後端交付網表？ – EEliaz

我檢查過它 - 運行'synth; 'write_smt2'前的splitnets -ports，SMT工具不提供ERROR消息。謝謝！ – EEliaz

一個問題得到修復，另一個問題彈出:)運行'synth; splitnets -ports' write_smt2'不會給出ERROR消息。但是，在添加這些行之前，BMC發現了一個計數器示例，但現在它沒有（並且非常快速地結束）。所以我猜我不能在'write_smt2'之前使用「合成器」，對吧？ – EEliaz

答案摹由克利福德維也納確實給出了一個解決方案，但我也想澄清，它不適合所有目的。

我的分析是爲了正式驗證而完成的。由於我將prep替換爲synth以解決虛假識別的邏輯循環，我的正式代碼得到了優化。我創建的電線僅由assume property編譯指示驅動，已被刪除 - 這使得許多斷言變得多餘。爲了行爲驗證的目的，減少任何邏輯是不正確的。

因此，如果目的是準備驗證數據庫，我建議不要使用synth命令，而是使用synth命令執行的命令子集。下可以找到這些命令： http://www.clifford.at/yosys/cmd_synth.html

一般情況下，我用在不優化的邏輯上面鏈接中指定的所有命令：

hierarchy -check 
proc 
check 
wreduce 
alumacc 
fsm 
memory -nomap 
memory_map 
techmap 
abc -fast 
hierarchy -check 
stat 
check

而且一切正常。

來源

2017-06-30 17:12:35 EEliaz

Yosys邏輯循環虛假檢測

回答

相關問題