lutpack transforms a mapped LUT-6 netlist into one that is not equivalent to its input.
Split out from #540, which is now blocked on this: that PR removes an assertion that turns out to be accidentally guarding this bug, so merging it alone would convert a loud abort into a silent wrong answer.
Reproduction
Input is a 24694-node mapped LUT-6 sqrt netlist (EPFL suite), produced by an area-oriented flow.
read_blif lutpack-miscompare-input.blif
lutpack
write_blif out.blif
- input: 24694 nodes, equivalent to
sqrt.aig
- output: 24635 nodes, not equivalent
Verified two independent ways: cec -n against the original benchmark, and a separate simulator that shares no code with ABC — 0 mismatches on the input, 46 on the output, with a reproducible input witness. So this is not a SAT-engine artefact and not a port-naming artefact.
The defect is not in the MUX decomposition path
Three builds:
| build |
behaviour |
| upstream, unpatched |
aborts on Lpk_MuxSplit: iVarVac < p->nVars (that assertion is #540's subject) |
| upstream + #540 |
completes, result is wrong |
| upstream + a change declining every MUX decomposition before any scratch slot is touched |
completes, result is still wrong |
With MUX decomposition disabled entirely the miscompile persists, so the bug lies elsewhere in lutpack — the assertion merely stops execution before it is reached on this input.
Note on the input
This netlist reaches lutpack from a flow using the delay-driven LUT-decomposition mapper (if -K k -Z n), so it may have structural properties an ordinary if -K 6 output does not. I mention it in case it narrows the search; the miscompile itself is in lutpack, which is handed a plain mapped netlist.
I can attach the reproducer netlist (about 400 kB gzipped) or make it available however is most convenient — please say which you prefer.
Related: #539 (uninitialised bestPerm read in ACD), #541 (64-bit shift UB in ACD), #540 (the assertion, now blocked on this).
lutpacktransforms a mapped LUT-6 netlist into one that is not equivalent to its input.Split out from #540, which is now blocked on this: that PR removes an assertion that turns out to be accidentally guarding this bug, so merging it alone would convert a loud abort into a silent wrong answer.
Reproduction
Input is a 24694-node mapped LUT-6
sqrtnetlist (EPFL suite), produced by an area-oriented flow.sqrt.aigVerified two independent ways:
cec -nagainst the original benchmark, and a separate simulator that shares no code with ABC — 0 mismatches on the input, 46 on the output, with a reproducible input witness. So this is not a SAT-engine artefact and not a port-naming artefact.The defect is not in the MUX decomposition path
Three builds:
Lpk_MuxSplit: iVarVac < p->nVars(that assertion is #540's subject)With MUX decomposition disabled entirely the miscompile persists, so the bug lies elsewhere in
lutpack— the assertion merely stops execution before it is reached on this input.Note on the input
This netlist reaches
lutpackfrom a flow using the delay-driven LUT-decomposition mapper (if -K k -Z n), so it may have structural properties an ordinaryif -K 6output does not. I mention it in case it narrows the search; the miscompile itself is inlutpack, which is handed a plain mapped netlist.I can attach the reproducer netlist (about 400 kB gzipped) or make it available however is most convenient — please say which you prefer.
Related: #539 (uninitialised
bestPermread in ACD), #541 (64-bit shift UB in ACD), #540 (the assertion, now blocked on this).