0

我一直在为一些用例测试 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

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

4

2 回答 2

3

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

gray2bin 字宽异或

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

gray2bin 单比特异或

于 2017-06-30T12:36:19.227 回答
-1

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

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

因此，如果目的是准备验证数据库，我建议不要使用该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-30T17:12:35.580 回答