错误检测到 Yosys 逻辑回路答案

【问题标题】：Yosys logic loop falsely detected错误检测到 Yosys 逻辑回路
【发布时间】：2017-07-01 01:12:35
【问题描述】：

我一直在测试 yosys 的一些用例。版本：Yosys 0.7+200 (git sha1 155a80d, gcc-6.3 6.3.0 -fPIC -Os)

我写了一个将格雷码转换为二进制的简单块：

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

我是否缺少某种标志或综合选项？

【问题讨论】：

标签： yosys

【解决方案1】：

使用全字运算符，这个电路显然有一个循环（使用yosys -p 'prep; show' gray2bin.v 生成）：

您必须将电路合成为门级表示以获得无循环版本（使用yosys -p 'synth; splitnets -ports; show' gray2bin.v 生成，对splitnets 的调用只是为了更好的可视化）：

【讨论】：

感谢您的快速回复！我不确定它是否有帮助 - 我的主要兴趣是 Yosys 的 FV 功能。 SMT2 后端给出“错误：在模块中找到逻辑循环”消息。是否可以向 SMT 后端提供网表？
我已经检查过了 - 在 write_smt2 工作之前运行 synth; splitnets -ports，并且 SMT 工具不会给出错误消息。谢谢！
一个问题得到修复，另一个问题弹出:) 运行 synth; splitnets -ports 后，write_smt2 没有给出错误消息。但是，在添加这些行之前，BMC 找到了一个反例，但现在它没有（并且结束得非常快）。所以我猜我不能在write_smt2 之前使用“合成器”，对吧？
如果你的设计有层次结构，那么 splitnets 可以打破它。正如我所说，我只是将它包含在脚本之上以创建更好的示意图。应该没有什么可以阻止 write_smt2 使用synth 的输出。如果出现问题，您应该为此创建另一个问题，并确保包含重现问题所需的代码和脚本。

【解决方案2】：

CliffordVienna 给出的答案确实给出了解决方案，但我也想澄清一下，它并不适合所有用途。

我的分析是为了形式验证。由于我将prep 替换为synth 以解决错误识别的逻辑循环，因此我的正式代码得到了优化。我创建的仅由assume property pragma 驱动的连线已被删除——这使得许多断言变得多余。为了行为验证而减少任何逻辑是不正确的。

因此，如果目的是准备验证数据库，我建议不要使用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

一切都按预期进行。

【讨论】：