カテゴリインデックス：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
