lutpack: assertion failure in Lpk_MuxSplit from an approximate cofactor support

[marcelwa]

Symptom

lutpack aborts on some networks with

abc: src/opt/lpk/lpkAbcMux.c:192: Lpk_MuxSplit:
     Assertion `iVarVac < (int)p->nVars' failed.

Reproducible in about 10 s on a 24.7k-LUT sqrt netlist produced by if -K 10 -Z 6:

read_blif sqrt-mapped.blif; lutpack

Root cause

Lpk_MuxSplit() stores the new component in a vacant fanin slot of the retained function:

p->uSupp  = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
p->uSupp |= (1 << Var);
iVarVac   = Kit_WordFindFirstBit( ~p->uSupp );
assert( iVarVac < (int)p->nVars );

A vacant slot is supposed to be guaranteed by Lpk_MuxAnalize(), which rejects a candidate variable when nSuppSizeL > p->nVars. But it reads nSuppSize0/nSuppSize1 out of the cached p->puSupps[], which Lpk_ComputeSupports() derives from two opposite-order BDDs and stitches together. That estimate can be a strict subset of the true cofactor support, so the feasibility test passes on a candidate whose real cofactor has no vacant fanin, and the assertion then fires in Lpk_MuxSplit.

Measured on the failing instance: at the failing call the cached support is 0x3f7 (9 variables) against a true 0xff7 (11). Across the same run, 484 of 101970 cached supports disagree with the recomputed value, 352 of them narrower — so this is a systematic property of the estimate, not a one-off.

Fix

Re-derive that one support after the candidate has been chosen, rather than trusting the cached estimate at the point where correctness depends on it. Recomputing everything would also work but is far more expensive; re-deriving the single support reaches the same answer.

On the reproducer, lutpack then completes normally and gives the same result as recomputing every support (24694 → 24635 nodes, 237 levels).

Testing

Built clean. if -K 10 -Z 6 on cavlc is unchanged (nd = 121, lev = 4), i.e. no behavioural change on paths that already worked.

[marcelwa]

Please do not merge this as it stands — I have found evidence that the assertion this PR removes is guarding a real miscompile elsewhere in lutpack, and that fixing it in isolation converts a loud abort into a silent wrong answer.

I am reporting this against my own patch as soon as I found it.

What happened

Running lutpack on a large mapped sqrt netlist, the output is not equivalent to the input: 24694 nodes in (equivalent), 24635 nodes out (not equivalent). Localised to the final lutpack invocation by a staged re-run, and confirmed independently of any SAT engine by a separate simulator — 0 mismatches on the input, 46 on the output, with a reproducible witness.

Three builds isolate the blame, and it is not this patch

build	behaviour
upstream, unpatched	aborts on the Lpk_MuxSplit: iVarVac < p->nVars assertion
upstream + this PR	completes, and the result is wrong
upstream + a change that declines every MUX decomposition before touching any scratch slot	completes, and the result is still wrong

The third row is the decisive one: with the MUX decomposition path disabled entirely, the miscompile still occurs. So the defect is not in the MUX split path, this patch does not introduce it, and the support-estimate problem the patch describes is real and separate.

What the patch does do is let execution proceed far enough to reach the underlying bug. The assertion was acting as an accidental guard.

What I would suggest

Treat this PR as blocked on the underlying lutpack miscompile rather than merging it. I am happy to (a) hold it open while the real defect is found, (b) withdraw it, or (c) re-scope it to fail loudly rather than silently, whichever you prefer — please say which and I will do it.

I will open a separate issue for the miscompile itself with the reproducer netlist and the exact command, and link it here.

Apologies for the noise; better to flag it against my own patch now than to have it merged and mask a correctness bug.

[marcelwa]

Filed the underlying miscompile as #542, with the three-build isolation and the verification detail. This PR is blocked on it.

[marcelwa]

One more correction to this PR's own description, which I should have caught before opening it.

The description says:

On the reproducer, lutpack then completes normally and gives the same result as recomputing every support (24694 → 24635 nodes, 237 levels).

That 24635-node netlist is precisely the non-equivalent output reported in #542. So the sentence I offered as evidence that the patch behaves correctly is in fact describing the miscompile. "Completes normally" was measured as terminates without aborting and matches an alternative implementation of the same support computation — both of which are true, and neither of which implies the output is correct. I did not check equivalence at that point, and I should have.

To be explicit about what the patch is and is not supported by:

• Still supported: the support-estimate analysis itself — Lpk_MuxAnalize reads the cached p->puSupps[], that estimate can be a strict subset of the true cofactor support (484 of 101970 disagreed on this instance, 352 of them narrower), and that is why the assertion fires. That part was measured directly and does not depend on the output netlist.
• No longer supported: any claim that the patched lutpack produces a correct result on this input. It does not.

Given #542, the honest status of this PR is that it removes a symptom whose underlying cause is unfixed. I would rather it not be merged in that state. Happy to withdraw it, or to hold it until #542 is understood and then rebase whatever part still applies — your call.