使用 Yosys 进行网表验证

Question

我想问一下我是否可以在yosys中验证我的设计。我重新综合了我的网表，使用yosys来执行（拓扑顺序）。

现在我想通过向网表插入一些输入并检查输出来检查此设计的有效性。

例如，我为我的模型使用了 s27 基准，我想确保我的设计输出与 s27 基准的输出相匹配。我浏览了 yosys 手册，但无法知道执行该操作的命令是什么。此外，我还使用了其他工具，例如 Veriwell。但我真的更喜欢使用 yosys。

Answer 1

如果您想用给定的测试平台模拟 post-synthesis 网表，那么您应该为此使用模拟器。（但是，我强烈推荐 Icarus Verilog 而不是 Veriwell。）

您当然可以使用形式化方法在 Yosys 中证明两个电路的等效性，但这要复杂得多，并且在尝试更大的设计时需要一定的经验。

以下 shell 脚本演示了使用 yosys 对 post-synthesis 网表进行形式等效检查的两种不同的基本方法：

# download fiedler-cooley.v
if [ ! -f fiedler-cooley.v ]; then
    wget https://raw.githubusercontent.com/cliffordwolf/yosys/master/tests/simple/fiedler-cooley.v
fi

# synthesis for ice40
yosys -p 'synth_ice40 -top up3down5 -blif up3down5.blif' fiedler-cooley.v

# formal verification with equiv_*
yosys -l check1.log -p '
    # gold design
    read_verilog fiedler-cooley.v
    prep -top up3down5
    splitnets -ports;;
    design -stash gold

    # gate design
    read_blif up3down5.blif
    techmap -autoproc -map +/ice40/cells_sim.v
    prep -top up3down5
    design -stash gate

    # prove equivalence
    design -copy-from gold -as gold up3down5
    design -copy-from gate -as gate up3down5
    equiv_make gold gate equiv
    hierarchy -top equiv
    equiv_simple
    equiv_status -assert
'

# formal verification with BMC and temproral induction (yosys "sat" command")
yosys -l check2.log -p '
    # gold design
    read_verilog fiedler-cooley.v
    prep -top up3down5
    splitnets -ports;;
    design -stash gold

    # gate design
    read_blif up3down5.blif
    techmap -autoproc -map +/ice40/cells_sim.v
    prep -top up3down5
    design -stash gate

    # prove equivalence
    design -copy-from gold -as gold up3down5
    design -copy-from gate -as gate up3down5
    miter -equiv -flatten gold gate miter
    hierarchy -top miter
    sat -verify -tempinduct -prove trigger 0 -seq 1 -set-at 1 in_up,in_down 0
'

# formal verification with BMC+tempinduct using undef modeling
yosys -l check3.log -p '
        # gold design
        read_verilog fiedler-cooley.v
        prep -top up3down5
        splitnets -ports;;
        design -stash gold

        # gate design
        read_blif up3down5.blif
        techmap -autoproc -map +/ice40/cells_sim.v
        prep -top up3down5
        design -stash gate

        # prove equivalence
        design -copy-from gold -as gold up3down5
        design -copy-from gate -as gate up3down5
        miter -equiv -flatten -ignore_gold_x gold gate miter
        hierarchy -top miter
        sat -verify -tempinduct -prove trigger 0 -set-init-undef -set-def-inputs
'

每种形式等价性检查方法都有其优缺点。

例如，上面的第一种方法需要能够通过名称匹配足够数量的内部线路才能成功验证等价性。但它能够将大型电路分解成更小的电路，因此即使在更大的设计中也能表现良好。

第二种方法不需要通过名称匹配任何内部线路，但需要电路的重置条件（-seq 1 -set-at 1 in_up,in_down 0部分）并且仅适用于"leak"所有内部状态的电路无论输入信号的顺序如何，都可以在少量周期内将其输出。

第三种方法是第二种方法的变体，它使用 undef 状态建模来避免重置条件的要求，但会产生更复杂的 SAT 模型，因此计算效率可能较低。

话虽这么说，您永远不应该依赖一种工具来检查自己产生的输出。例如。如果 Yosys Verilog front-end 中存在错误，那么这同样会影响综合和验证，并且永远不会检测到该问题。因此，如果您使用 Yosys 来验证 Yosys 的输出，那么除了使用独立 code-base 的验证方案之外，您还应该这样做。例如 Icarus Verilog 或 Verilator 将是两个不与 Yosys（或彼此 afaict）共享任何代码的模拟器。另外：一般来说，形式验证不能代替模拟。（特别是不是正式的等价性检查：你怎么知道你检查等价性的模型首先是正确的？）

使用 Yosys 进行网表验证

Netlist validation using Yosys

verilog

yosys