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逻辑循环虚假检测

回答

相关问题