错误检测到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$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

我是不是遗漏了某种标志或合成选项？

Answer 1

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

​

​

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

​

​

Answer 2

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

我的分析是为了正式验证的目的。由于我将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

一切都像预期的那样工作。