错误检测到 Yosys 逻辑循环

Question

我一直在测试 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
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

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

Answer 1

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

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

Answer 2

CliffordVienna给出的答案确实给出了解决方案，但我也想说明一下，并不是万能的。

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

因此，如果目的是准备验证数据库，我建议不要使用synth命令，而是使用synth命令执行的命令子集。您可以在以下位置找到这些命令： http://www.clifford.at/yosys/cmd_synth.html

总的来说，我已经使用了上面link中指定的所有不优化逻辑的命令：

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

一切都按预期进行。

错误检测到 Yosys 逻辑循环

Yosys logic loop falsely detected

yosys