sat - Yosys 指令“sat -dump_cnf”

Question

我在 Verilog 中有一个示例组合循环，我可以按照说明进行逻辑综合并生成 blif 文件。

但是，我需要的是从电路中生成 CNF 公式。ABC 等工具仅允许从组合斜接生成（即，具有 1 个输出）。

我尝试了 yosys 指令“sat -dump_cnf FILE”，确实可以生成 CNF 文件。但是，我不确定如何将 CNF 中的变量与电路中的 I/O 映射。

有没有人研究过 Yosys 的“sat -dump_cnf”功能并可以给我一个指针？