使用 Yosys 进行网表验证

Question

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

现在我想通过将一些输入插入网表并检查输出来检查此设计的验证。

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

Answer 1

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

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

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

# 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 部分），并且仅适用于在一个小范围内将所有内部状态“泄漏”到其输出的电路周期数，与输入信号的顺序无关。

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

话虽如此，您永远不应该依赖一种工具来检查输出本身产生的结果。例如。如果 Yosys Verilog 前端有 bug，那么这同样会影响合成和验证，并且永远不会检测到问题。因此，如果您使用 Yosys 来验证 Yosys 的输出，那么除了使用独立代码库的验证方案之外，您应该只这样做。例如，Icarus Verilog 或 Verilator 将是两个不与 Yosys 共享任何代码（或彼此不共享）的模拟器。另外：一般来说，形式验证不能代替模拟。 （尤其不是正式的等价检查：你怎么知道你检查等价的模型首先是正确的？）