3

yosys で自分のデザインを検証できるかどうか尋ねたいと思います。ネットリストを再合成し、yosys を使用して実行 (トポロジー順序) を取得しました。

ここで、いくつかの入力をネットリストに挿入し、出力を確認して、このデザインの検証を確認したいと思います。

たとえば、モデルに s27 ベンチマークを使用しました。設計の出力が s27 ベンチマークの出力と一致することを確認したいと考えています。私はyosysマニュアルを調べましたが、それを行うコマンドを知ることができませんでした. また、Veriwell などの他のツールも使用しました。しかし、私は yosys を使用することを本当に好みます。

4

1 に答える 1

6

特定のテスト ベンチを使用して合成後のネットリストをシミュレートするだけの場合は、そのためにシミュレータを使用する必要があります。(ただし、Veriwell よりも Icarus Verilog を強くお勧めします。)

もちろん形式的な方法を使用して Yosys の 2 つの回路の同等性を証明することもできますが、これははるかに複雑であり、大規模な設計で試行する場合はある程度の経験が必要です。

次のシェル スクリプトは、yosys を使用した合成後のネットリストの正式な同等性チェックの 2 つの異なる基本的な方法を示しています。

# 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
'

正式な同等性チェックの各方法には、長所と短所があります。

たとえば、上記の最初の方法では、同等性を正しく検証するために、十分な数の内部ワイヤを名前で照合できる必要があります。しかし、大規模な回路を小さな回路に分割できるため、大規模な設計でもうまく機能します。

2 番目の方法は、内部ワイヤを名前で一致させる必要はありませんが、回路 (-seq 1 -set-at 1 in_up,in_down 0パーツ) のリセット条件が必要であり、すべての内部状態を少数のサイクル内でその出力に「リーク」する回路でのみ機能します。入力信号のシーケンス。

3 番目の方法は、undef 状態のモデリングを使用してリセット条件の要件を回避する 2 番目の方法のバリエーションですが、より複雑な SAT モデルを生成するため、計算効率が低下する可能性があります。

とはいえ、出力自体が生成されたことを確認するために、1 つのツールに頼るべきではありません。たとえば、Yosys Verilog フロントエンドにバグがある場合、これは同様に合成と検証に影響し、問題は決して検出されません。したがって、Yosys を使用して Yosys の出力を検証する場合は、独立したコードベースを使用する検証スキームに加えて、それを行う必要があります。たとえば、Icarus Verilog または Verilator は、Yosys とコードを共有しない (または相互に影響する) 2 つのシミュレーターです。また、一般に、フォーマル検証はシミュレーションの代わりにはなりません。(特に正式な等価性チェックではありません: 等価性をチェックするモデルがそもそも正しいことをどうやって知るのでしょうか?)

于 2016-01-26T09:45:30.153 に答える