System and method for compacting X-pessimism fixes for gate-level logic simulation
A computer executable tool analyzes Boolean logic in a gate-level netlist responsible for generating false Xs due to X-pessimism in logic simulation to produce a compact fix that corrects the X-pessimism problem. The fix restores logic simulation value from X to hardware-accurate non-X value and solves X-pessimism issues in logic simulation.
1. A method of generating minimized false-X fixes in a netlist, comprising:
inserting at least one multiplexer (MUX) at at least one output wire of a gate;
converting the netlist, including the inserted MUX, into a conjunctive normal form (CNF) netlist;
constraining an output exhibiting a false-X of the CNF netlist to an opposite value of the false-X, wherein the CNF must be unsatisfiable;
identifying a compact unsatisfiable core to reduce X-pessimism fix complexity;
traversing the netlist; and
collecting fanin frontier variables closest to the output of the netlist for each MUX select line that is not in the unsatisfiable core.
2. The method of claim 1 , wherein inserting at least one multiplexer (MUX) at at least one output wire of a gate comprises inserting at least one MUX at each output wire of every gate.
3. The method of claim 1 , further comprising assuming each select line is 0 and solving the CNF netlist.
4. The method of claim 1 , further comprising adding all wires with MUX select lines not in the unsatisfiable core into a hash table.
5. The method of claim 1 , wherein:
if a MUX select line is 0 a MUX input comes from an original output wire,
if the MUX select line is 1 the MUX input comes from a new primary input.
6. A system for generating minimized false-X fixes in a netlist, the system comprising:
a processor; and
a memory having executable instructions stored there on such that, when executed by the processor, result in the processor being configured to:
insert at least one multiplexer (MUX) at at least one output wire of a gate;
convert the netlist, including the inserted MUX, into a conjunctive normal form (CNF) netlist;
constrain an output exhibiting a false-X of the CNF netlist to an opposite value of the false-X, wherein the CNF must be unsatisfiable;
identify a compact unsatisfiable core to reduce X-pessimism fix complexity;
traverse the netlist; and
collect fanin frontier variables closest to the output of the netlist for each MUX select line that is not in the unsatisfiable core.
7. The system of claim 6 , wherein inserting at least one multiplexer (MUX) comprises inserting at least one MUX at each output wire of every gate.
8. The system of claim 6 , further comprising assuming each select line is 0 and solving the CNF netlist.
9. The system of claim 6 , further comprising adding all wires with MUX select lines not in the unsatisfiable core into a hash table.
10. The system of claim 6 , wherein:
if a MUX select line is 0 a MUX input comes from an original output wire,
if the MUX select line is 1 the MUX input comes from a new primary input.