問題タブ [yosys]

Verific パーサーと一緒に Yosys の正式な検証機能を使用しようとしています。

「read_verilog -formal」コマンドと比較して、正式な検証のために verific を使用する yosys でサポートされている機能は何ですか? たとえば、read_verilog で動作する正式なコードをすばやくコンパイルすると、「assume property」構文でエラーが発生しました。

より多くの機能をサポートするために Verific ライブラリ フラグを何らかの方法で変更する必要があるかどうか、またはそれがサポートされていないものであるかどうかはわかりません。

Verilog にサンプルの組み合わせ回路があり、命令に従って論理合成を行い、blif ファイルを生成できます。

ただし、回路から CNF 式を生成する必要があります。ABC などのツールでは、組み合わせマイター (つまり、1 つの出力) からのみ生成できます。

yosys 命令「sat -dump_cnf FILE」を試してみたところ、実際に CNF ファイルを生成できました。ただし、CNF 内の変数を回路内の I/O にマップする方法がわかりません。

Yosys の "sat -dump_cnf" 機能を調べた人はいますか?

gcc オプション -MMD に相当する依存ファイルを作成する Yosys 用のコマンドはありますか? (このオプションは、コンパイル単位に含まれるすべてのファイルをリストする小さな Makefile フラグメントを出力します。Makefile で -MMD を指定して g++ を使用して依存関係を自動的に生成する を参照してください)

背景: Yosys を使用して Verilog プロジェクトを合成する Makefile を作成しようとしています。プロジェクトは、他の verilog 依存関係が含まれている単一の最上位 verilog ファイルを使用します。これを行うには、次の make ルールを使用します。これは非常にうまく機能します。

Makefile で明示的に他の Verilog ファイルに言及したくないので、依存ファイルを使用したいと思います。これにより、依存ファイルのいずれかに適用された変更を検出し、再コンパイルをトリガーできます。

Clifford によって追加された新しい yosys -E オプションのおかげで、上記の Makefile ルールを次のように変更できました。

これで、暗黙的に参照される Verilog ファイルの 1 つが変更されるたびに、blif ファイルが生成されます。