Lets say I have a black box circuit with N inputs and 1 output.
I want to fix the value of M inputs and find the value of rest of the inputs (N-M) for which the circuit is satisfiable. If I manually fix the M inputs in the verilog RTL, and convert it to CNF (using abc), will this yield the correct result? Is it the right approach to this kind of problem?
The original search space of your problem has 2^N entries. By fixing M inputs, the search space is reduced by a factor of 2^M and has 2^(N-M) entries.
Depending on your choice of the fixed M input values, you can either simplify the search or reduce the search space too much and end up without a solution.
Your black box is a combinatorial circuit, where the output solely depends on the current state of the inputs? In a RTL (register transfer level/language) setting, you could also describe a sequential mechanism, where the output also depends on previous inputs.
To take into account fixed inputs is called Boolean Constraint Propagation. This basically simplifies your circuit, as all elements can be removed which have a predetermined output. Examples: An AND with one or more false input has a false output. An OR with one or more true input has a true output, and so forth. Other simplifications include removal of double negations and of inverted input pairs to XOR/XNOR gates.
You could have a look at bc2cnf, a translator from a Boolean netlist format to a SAT solver digestible DIMACS/CNF file. Similarly to ABC, bc2cnf will propagate constant inputs and deliver a fairly optimized CNF.
