From 4d504f20ba273434f4cabbb974763187dc0e94e6 Mon Sep 17 00:00:00 2001 From: Marcel Walter Date: Fri, 7 Aug 2026 20:54:11 +0200 Subject: [PATCH] fraig_store: restore the PI order when the name comparison fails Abc_NtkCompareSignals() sorts the PIs, POs and boxes of both networks by name before comparing them. That is deliberate and is what lets fraig_store accept two networks that use the same names in a different order. When the names do not match, though, the comparison fails, Abc_NtkFraigStore() resets the store and keeps the incoming network -- which by then has already been sorted. The network that ends up in the store is a permutation of the one the caller read in, and nothing reports it. The two lines printed on that path say the store was reset; they do not say the interface changed. Sorting is by name as a string, so numeric port names are where it shows up worst: 1, 2, ..., 10 sort as 1, 10, 2, 3, ... With the EPFL cavlc benchmark and its published reference netlist, whose ports are named "1".."10", read_aiger cavlc.aig; strash; fraig_store read_blif cavlc_size.blif; strash; fraig_store fraig_restore; write_blif out.blif gives an out.blif whose inputs are ordered 1, 10, 2, 3, ... instead of 1, 2, 3, ..., 10. It has the right number of inputs and outputs, it passes Abc_NtkCheck(), and "cec -n out.blif cavlc.aig" reports a counterexample. Save the three vectors before the comparison and put them back if it fails, then rebuild vCis/vCos with Abc_NtkOrderCisCos(). The success path is untouched, and so is every path where the names already agree -- those never reach Abc_NtkCompareSignals(), since Abc_NodeCompareCiCo() has already returned 1. --- src/base/abci/abcFraig.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 2cfb46bb0..bf40bd582 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -670,13 +670,29 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd ) extern int Abc_NodeCompareCiCo( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ); if ( !Abc_NodeCompareCiCo(pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0)) ) { + // Abc_NtkCompareSignals() sorts the PIs/POs/boxes of both networks by name as a + // side effect, which is what makes the comparison meaningful when the two do use + // the same names. When they do not, the comparison fails, the store is reset and + // this network is kept -- so the sort has to be undone here. Otherwise the stored + // network is a permutation of the one the caller read in, and everything after it + // is off by that permutation with nothing to indicate it. + Vec_Ptr_t * vPis = Vec_PtrDup( pNtk->vPis ); + Vec_Ptr_t * vPos = Vec_PtrDup( pNtk->vPos ); + Vec_Ptr_t * vBoxes = Vec_PtrDup( pNtk->vBoxes ); // reorder PIs of pNtk2 according to pNtk1 if ( !Abc_NtkCompareSignals( pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0), 1, 1 ) ) { + Vec_PtrFree( pNtk->vPis ); pNtk->vPis = vPis; vPis = NULL; + Vec_PtrFree( pNtk->vPos ); pNtk->vPos = vPos; vPos = NULL; + Vec_PtrFree( pNtk->vBoxes ); pNtk->vBoxes = vBoxes; vBoxes = NULL; + Abc_NtkOrderCisCos( pNtk ); printf( "Trying to store the network with different primary inputs.\n" ); printf( "The previously stored networks are deleted and this one is added.\n" ); Abc_NtkFraigStoreClean(); } + if ( vPis ) Vec_PtrFree( vPis ); + if ( vPos ) Vec_PtrFree( vPos ); + if ( vBoxes ) Vec_PtrFree( vBoxes ); } } Vec_PtrPush( vStore, pNtk );