I have a sample combinatorial circult in Verilog where I can follow the instruction to do logic synthesis and generate blif file.
However, what I need is to generate the CNF formula out of the circuit. Tools such as ABC only allows to generate from combinatorial miter (i.e., with 1 output).
I tried the yosys instruction "sat -dump_cnf FILE", and indeed I am able to generate a CNF file. However, I am not sure how to map variables in the CNF with I/Os in the circuit.
Have anyone studied the feature "sat -dump_cnf" from Yosys and can give me a pointer?