カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000

SymbiYosysのBMCモードにおけるエンジンとオプション

SymbiYosys（sby）のBMCモードでは、様々なエンジンとオプションを使用することができる。

BMCモードの基本設定

BMCモードを使用する場合は、以下のように設定する。

[options]
mode bmc

利用可能なエンジン

BMCモードでは、以下のエンジンが使用可能である。

[engines]
smtbmc [all solvers] 
btor btormc
btor pono
abc bmc3
abc sim3
aiger aigbmc

smtbmcエンジンの詳細

smtbmcエンジンは、最も柔軟性の高いエンジンであり、様々なオプションとソルバーをサポートしている。

主要なオプション

• --nomem: SMTの配列理論を使用せず、メモリをレジスタとアドレス論理に合成する
• --syn: ワードレベルのSMT演算子の代わりに、ゲートレベル表現に合成する
• --stbv: 状態表現に大きなビットベクタを使用する
• --stdt: SMT-LIB 2.6のデータ型を使用して状態を表現する
• --nopresat: 仮定の矛盾チェックをスキップする
• --keep-going: 最初の失敗後も検証を継続する
• --unroll, --nounroll: SMT問題のアンロールを制御する
• --dumpsmt2: SMT2のトレースを出力ファイルに保存する
• --progress: Yosys-SMTBMCタイマー表示を有効にする

サポートされているSMT2ソルバー

• yices
• boolector
• bitwuzla
• z3
• mathsat
• cvc4
• cvc5

btorエンジンの詳細

btorエンジンは、btor2ファイル形式をサポートするハードウェアモデルチェッカー用のエンジンである。btor2は、ハードウェアのビット精密なモデルを表現するためのワードレベルモデル検査フォーマットである。

サポートされているソルバー

• btormc
• pono

abcエンジンの詳細

abcエンジンは、Berkeley ABCの機能をフロントエンドとして提供する。ABCは、論理合成と検証のためのツールセットである。

サポートされているソルバー

• bmc3
• sim3

aigerエンジンの詳細

aigerエンジンは、AIGERファイルを処理するハードウェアモデルチェッカー用の汎用フロントエンドである。AIGERは、And-Inverter Graph形式のファイルフォーマットである。

サポートされているソルバー

• aigbmc