Verilog にサンプルの組み合わせ回路があり、命令に従って論理合成を行い、blif ファイルを生成できます。
ただし、回路から CNF 式を生成する必要があります。ABC などのツールでは、組み合わせマイター (つまり、1 つの出力) からのみ生成できます。
yosys 命令「sat -dump_cnf FILE」を試してみたところ、実際に CNF ファイルを生成できました。ただし、CNF 内の変数を回路内の I/O にマップする方法がわかりません。
Yosys の "sat -dump_cnf" 機能を調べた人はいますか?