&cec -x/-y: is the AND-free check meant to be sufficient for equivalence?

[marcelwa]

Apologies in advance if I have misread this — I would rather ask than assume.

While auditing my own results I noticed that &cec -y reported a pair of networks as equivalent that I was fairly sure were not, and following it back led me to the verdict logic in Abc_CommandAbc9Cec. I may well be missing an invariant that makes the current form correct, in which case please just close this and, if you have a moment, I would be grateful to know what I overlooked.

What I think I am seeing

In the -x and -y branches of &cec (and the corresponding branch of &icec), the verdict is taken from the swept miter having no AND nodes:

Gia_Man_t * pNew = Cec5_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
if ( Gia_ManAndNum(pNew) == 0 )
    Abc_Print( 1, "Networks are equivalent.  " );
else
    Abc_Print( 1, "Networks are UNDECIDED.  " );

My reading is that Gia_ManAndNum(pNew) == 0 is necessary but not sufficient: an AND-free GIA can still have an output that is constant 1, or a CI literal, and both of those are satisfiable miters. If that is right, the check reports equivalence for some non-equivalent pairs, and the branch has no NOT_EQUIVALENT outcome at all.

Smallest case I could reduce it to

Two 2-input AIGs, f = a & b and g = ~(a & b) — they differ on every input:

$ abc -q "&read and2.aig; &cec -y nand2.aig"
Networks are equivalent.  Time =     0.00 sec

$ abc -q "&read and2.aig; &cec -x nand2.aig"
Networks are equivalent.  Time =     0.00 sec

$ abc -q "&read and2.aig; &cec nand2.aig"
Networks are NOT EQUIVALENT. Output 0 trivially differs (different phase).

The default engine gets it right, which is why this went unnoticed on my side for a while — it only surfaced because one of my checks happened to pin -y. On a real 36 500-LUT netlist I also saw -y accept a mutant whose first output is the exact complement of the reference's, at 302 s, where cec refutes it in 1.2 s.

The change proposed here

If the reading above is correct, the smallest fix I could find is to check the outputs as well as the AND count:

• AND nodes remaining → UNDECIDED, exactly as before;
• AND-free with all outputs constant 0 → equivalent, exactly as before;
• AND-free otherwise → NOT equivalent, which seems safe to decide, since such a miter is satisfiable by inspection.

Gia_ManPoIsConst0() already exists, so the helper is four lines. Applied at all three sites, since the same idiom appears in &cec -x, &cec -y and &icec.

Behaviour on the small cases above, built from this branch:

pair	relationship	before	after
and2 vs and2	equivalent	equivalent	equivalent
and2 vs nand2	differ on every input	equivalent	NOT equivalent
and2 vs or2	differ on some inputs	UNDECIDED	UNDECIDED

The default &cec and cec paths go through Cec_ManVerify and are untouched.

Caveats I am aware of

I have only exercised this on small hand-built cases plus my own benchmark netlists, not against your regression suite, so please treat the change as a suggestion rather than a validated patch. I am also not certain whether the -x/-y branches are intended as full equivalence checks or as fast pre-filters where a caller is expected to confirm a positive result some other way — if it is the latter, then this is a documentation question rather than a bug, and I would be happy to see it closed on those grounds.

Thanks very much for ABC, and for taking a look.