verilog - 使用 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 前端存在错误，那么这将同样影响综合和验证，并且永远不会检测到问题。因此，如果您使用 Yosys 来验证 Yosys 的输出，那么您应该只在使用独立代码库的验证方案之外执行此操作。例如，Icarus Verilog 或 Verilator 是两个模拟器，它们不与 Yosys(或彼此)共享任何代码。另外:一般来说，形式验证不能替代模拟。 (特别是不是正式的等价性检查:您如何知道检查等价性的模型首先是正确的？)