luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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.
This commit is contained in:
Marcel Walter 2026-08-07 20:54:11 +02:00
parent 8e224cd794
commit 4d504f20ba
No known key found for this signature in database
GPG Key ID: 2979DB71A0C2C23D
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/base/abci/abcFraig.c
View File

@ -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 );