fraig_store: Abc_NtkAppendToCone silently creates new PIs when input names differ

[marcelwa]

fraig_store / fraig_restore is the documented way to build a choice network out of several implementations of the same function. If those implementations disagree about their input names, the result is a well-formed network computing a different function, and nothing says so.

Abc_NtkAppendToCone() (src/base/abc/abcNtk.c, around line 1178) matches each CI of the incoming network to the accumulated one by name:

iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
if ( iNodeId == -1 )
{
    pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
    Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
}

When the name is absent, a fresh primary input is created. So a structure whose inputs are called pi0 pi1 … merged onto one whose inputs are called 1 2 3 … is not merged onto the same variables at all — it is grafted onto a disjoint set of unconstrained ones. The accumulated network's input count grows, Abc_NtkCheck() passes, fraig_restore succeeds, and the mapper then picks cuts from a "choice" that is not equivalent to anything.

Reproducing

Take any circuit, write two structurally different implementations of it, name the ports differently in each, then:

read a.aig; strash; fraig_store
read b.blif; strash; fraig_store
fraig_restore; if -K 6; write_blif out.blif
cec -n out.blif original.aig

The workaround is easy once you know: round-trip every network through write_aiger/read_aiger first, which drops the symbol table and regenerates names positionally.

The question

Is the silent-PI-creation branch deliberate? I can see it being the right behaviour for Abc_NtkAppendToCone()'s other callers, where the incoming cone genuinely may reference signals the accumulator has not seen.

If it is deliberate, would a warning be acceptable when a CI name is not found during fraig_store accumulation — or a note in the fraig_store help text that the stored networks must agree on port names? The failure is silent and produces a plausible-looking result, which is the expensive kind.

Happy to send a patch for whichever of those you'd prefer.

[marcelwa]

Correcting myself: the mechanism I described above is wrong, and I should have reproduced it before filing.

Abc_NtkAppendToCone() is not involved. Its PI-creation branch is never reached on this path, and its only caller is Abc_NtkFraigPartitioned(). I had inferred the mechanism from reading the code rather than from observing it.

What actually happens is one level up, in Abc_NtkFraigStore(). Abc_NtkCompareSignals() sorts the PIs, POs and boxes of both networks by name before comparing them — deliberately, since that is what lets fraig_store accept two networks using the same names in a different order. When the names genuinely differ the comparison fails, the store is reset, and the incoming network is kept — but it has already been sorted by the comparison that failed. So the stored network is a permutation of the one that was read in.

The sort is by name as a string, so 1, 2, …, 10 becomes 1, 10, 2, 3, …. On cavlc with its published reference netlist that gives:

$ abc -q "read_blif out.blif; print_io"
Primary inputs (10):  0=1 1=10 2=2 3=3 4=4 5=5 6=6 7=7 8=8 9=9

and cec -n then reports a counterexample.

So the behaviour is also less silent than I claimed — ABC does print "Trying to store the network with different primary inputs" and "The previously stored networks are deleted and this one is added." What it does not say is that the surviving network's interface has been reordered, which is the part that actually costs you.

That makes it a narrower and more fixable problem than the one I described, so I have opened #538 with a patch: save the three vectors before the comparison and restore them if it fails. The success path and the already-matching path are untouched.

Apologies for the noise in the original report.