From 57544eb9ca04015120e589b3c80d9edc1e5a8db9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 18 Jan 2026 09:30:48 +0700 Subject: [PATCH] Add an option to unhash a mapped AIG after &satlut. --- src/aig/gia/giaIf.c | 79 +++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 16 +++++++-- 2 files changed, 93 insertions(+), 2 deletions(-) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index cfbf01a70..db4ed62d5 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -3250,6 +3250,85 @@ Gia_Man_t * Gia_ManDupHashMapping( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Uniqifies AIG nodes within each mapped cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupCollectedCutNodes_rec( Gia_Man_t * p, int iLut, Vec_Int_t * vNodes ) +{ + if ( Gia_ObjUpdateTravIdCurrentId(p, iLut) ) + return; + Gia_ManDupCollectedCutNodes_rec( p, Gia_ObjFaninId0p(p, Gia_ManObj(p, iLut)), vNodes ); + Gia_ManDupCollectedCutNodes_rec( p, Gia_ObjFaninId1p(p, Gia_ManObj(p, iLut)), vNodes ); + Vec_IntPush( vNodes, iLut ); +} +void Gia_ManDupCollectedCutNodes( Gia_Man_t * p, int iLut, Vec_Int_t * vNodes ) +{ + Gia_ManIncrementTravId(p); + Vec_IntClear( vNodes ); + int k, iFan; + Gia_LutForEachFanin( p, iLut, iFan, k ) + Gia_ObjSetTravIdCurrentId(p, iFan); + assert( !Gia_ObjIsTravIdCurrentId(p, iLut) ); + Gia_ManDupCollectedCutNodes_rec( p, iLut, vNodes ); + assert( Gia_ObjIsTravIdCurrentId(p, iLut) ); +} +Gia_Man_t * Gia_ManDupUnhashMapping( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Vec_Int_t * vMapping; + Gia_Obj_t * pObj, * pFanin; + Vec_Int_t * vNodes = Vec_IntAlloc( 100 ); + Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) ); + int i, k, iTempLit; + assert( Gia_ManHasMapping(p) ); + // copy the old manager with hashing + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachLut( p, i ) + { + Gia_ManDupCollectedCutNodes( p, i, vNodes ); + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), pObj->Value ); + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + iTempLit = Gia_ManObj(p, i)->Value; + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + pObj->Value = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) ); + Gia_ManObj(p, i)->Value = iTempLit; + } + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + // recreate mapping + vMapping = Vec_IntAlloc( Vec_IntSize(p->vMapping) ); + Vec_IntFill( vMapping, Gia_ManObjNum(pNew), 0 ); + Gia_ManForEachLut( p, i ) + { + pObj = Gia_ManObj( p, i ); + Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pObj->Value), Vec_IntSize(vMapping) ); + Vec_IntPush( vMapping, Gia_ObjLutSize(p, i) ); + Gia_LutForEachFaninObj( p, i, pFanin, k ) + Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->Value) ); + Vec_IntPush( vMapping, Abc_Lit2Var(pObj->Value) ); + } + Vec_IntFree( vMap ); + pNew->vMapping = vMapping; + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 01ec26654..0cecf8fc9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36300,6 +36300,7 @@ usage: int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Gia_ManDupMuxRestructure( Gia_Man_t * p ); + extern Gia_Man_t * Gia_ManDupUnhashMapping( Gia_Man_t * p ); Gia_Man_t * pTemp; int c, Limit = 2; int Multi = 0; @@ -36309,9 +36310,10 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAddMuxes = 0; int fStrMuxes = 0; int fRehashMap = 0; + int fUnhashMap = 0; int fInvert = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsih" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrusih" ) ) != EOF ) { switch ( c ) { @@ -36352,6 +36354,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRehashMap ^= 1; break; + case 'u': + fUnhashMap ^= 1; + break; case 's': fStrMuxes ^= 1; break; @@ -36404,6 +36409,12 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManTransferPacking( pTemp, pAbc->pGia ); Gia_ManTransferTiming( pTemp, pAbc->pGia ); } + else if ( Gia_ManHasMapping(pAbc->pGia) && fUnhashMap ) + { + pTemp = Gia_ManDupUnhashMapping( pAbc->pGia ); + Gia_ManTransferPacking( pTemp, pAbc->pGia ); + Gia_ManTransferTiming( pTemp, pAbc->pGia ); + } else if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs2 ) pTemp = (Gia_Man_t *)If_ManDeriveGiaFromCells2( pAbc->pGia ); else if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs ) @@ -36460,7 +36471,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &st [-LM num] [-bacmrsih]\n" ); + Abc_Print( -2, "usage: &st [-LM num] [-bacmrusih]\n" ); Abc_Print( -2, "\t performs structural hashing\n" ); Abc_Print( -2, "\t-b : toggle adding buffers at the inputs and outputs [default = %s]\n", fAddBuffs? "yes": "no" ); Abc_Print( -2, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" ); @@ -36470,6 +36481,7 @@ usage: Abc_Print( -2, "\t (use L = 1 to create AIG with XORs but without MUXes)\n" ); Abc_Print( -2, "\t-M num : create an AIG with additional primary inputs [default = %d]\n", Multi ); Abc_Print( -2, "\t-r : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" ); + Abc_Print( -2, "\t-u : toggle unhashing AIG while preserving mapping [default = %s]\n", fUnhashMap? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using MUX restructuring [default = %s]\n", fStrMuxes? "yes": "no" ); Abc_Print( -2, "\t-i : toggle complementing the POs of the AIG [default = %s]\n", fInvert? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n");