From b4ca3e7f520fcb8f21553f20b7fd6dec8321490d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 29 Jun 2026 22:51:13 -0700 Subject: [PATCH] Adding &put -i to preserve special LUT mapping. --- src/base/abci/abc.c | 14 ++++++-- src/base/abci/abcDar.c | 75 +++++++++++++++++++++++++++++++++++++++--- src/map/if/ifDec07.c | 6 ++-- 3 files changed, 84 insertions(+), 11 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 11d90c4fc..68dd9b097 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35234,16 +35234,18 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkRedirectCiCo( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs ); extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs ); + extern Abc_Ntk_t * Abc_NtkFromMappedGiaAnd5( Gia_Man_t * p, int fFindEnables, int fUseBuffs ); Aig_Man_t * pMan; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int fStatusClear = 1; int fFindEnables = 0; int fUseBuffs = 0; + int fCheckAnd5 = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "seovh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "seiovh" ) ) != EOF ) { switch ( c ) { @@ -35253,6 +35255,9 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'e': fFindEnables ^= 1; break; + case 'i': + fCheckAnd5 ^= 1; + break; case 'o': fUseBuffs ^= 1; break; @@ -35275,7 +35280,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) else if ( Gia_ManHasCellMapping(pAbc->pGia) ) pNtk = Abc_NtkFromCellMappedGia( pAbc->pGia, fUseBuffs ); else if ( Gia_ManHasMapping(pAbc->pGia) || pAbc->pGia->pMuxes ) - pNtk = Abc_NtkFromMappedGia( pAbc->pGia, 0, fUseBuffs ); + pNtk = fCheckAnd5 ? Abc_NtkFromMappedGiaAnd5( pAbc->pGia, 0, fUseBuffs ) : Abc_NtkFromMappedGia( pAbc->pGia, 0, fUseBuffs ); else if ( Gia_ManHasDangling(pAbc->pGia) == 0 ) { pMan = Gia_ManToAig( pAbc->pGia, 0 ); @@ -35298,6 +35303,8 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkDelete( pNtkNoCh ); Aig_ManStop( pMan ); } + if ( pNtk == NULL ) + return 1; // transfer the spec name to the pNtk if( pAbc->pGia->pSpec ) { @@ -35364,10 +35371,11 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &put [-seovh]\n" ); + Abc_Print( -2, "usage: &put [-seiovh]\n" ); Abc_Print( -2, "\t transfer the current network into the old ABC\n" ); Abc_Print( -2, "\t-s : toggle clearning verification status [default = %s]\n", fStatusClear? "yes": "no" ); Abc_Print( -2, "\t-e : toggle extracting MUXes for flop enables [default = %s]\n", fFindEnables? "yes": "no" ); + Abc_Print( -2, "\t-i : toggle AND-decomposable polarity for 5-input LUTs [default = %s]\n", fCheckAnd5? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", fUseBuffs? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 6b0322361..18d9b2bbc 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -38,6 +38,7 @@ #include "opt/csw/csw.h" #include "proof/pdr/pdr.h" #include "sat/bmc/bmc.h" +#include "misc/util/utilTruth.h" #include "map/mio/mio.h" #include "misc/vec/vecMem.h" @@ -757,7 +758,7 @@ Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, V Vec_PtrWriteEntry( vCopies, Id, gFunc ); return gFunc; } -Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies ) +static Hop_Obj_t * Abc_ObjHopFromGia2( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies, Vec_Bit_t * vCompls ) { int k, iFan; assert( Gia_ObjIsLut(p, GiaId) ); @@ -766,10 +767,31 @@ Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Ve Gia_LutForEachFanin( p, GiaId, iFan, k ) { Gia_ObjSetTravIdCurrentId(p, iFan); - Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) ); + Vec_PtrWriteEntry( vCopies, iFan, Hop_NotCond(Hop_IthVar(pHopMan, k), vCompls && Vec_BitEntry(vCompls, iFan)) ); } return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies ); } +Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies ) +{ + return Abc_ObjHopFromGia2( pHopMan, p, GiaId, vCopies, NULL ); +} + +static int Abc_Tt5HasAndDec( word Truth ) +{ + int v; + for ( v = 0; v < 5; v++ ) + if ( Abc_Tt6Cofactor0(Truth, v) == 0 || Abc_Tt6Cofactor1(Truth, v) == 0 ) + return 1; + return 0; +} +static int Abc_Tt5AndDecPolarity( word Truth ) +{ + if ( Abc_Tt5HasAndDec(Truth) ) + return 0; + if ( Abc_Tt5HasAndDec(~Truth) ) + return 1; + return -1; +} /**Function************************************************************* @@ -804,7 +826,7 @@ Abc_Obj_t * Abc_NtkFromMappedGia_rec( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, int iO pObjNew = Abc_NtkCreateNodeInv(pNtkNew, pObjNew); return pObjNew; } -Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs ) +Abc_Ntk_t * Abc_NtkFromMappedGiaInt( Gia_Man_t * p, int fFindEnables, int fUseBuffs, int fCheckAnd5 ) { int fVerbose = 0; int fDuplicate = 0; @@ -812,6 +834,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL; Gia_Obj_t * pObj, * pObjLi, * pObjLo; Vec_Ptr_t * vReflect; + Vec_Bit_t * vCompls = NULL; int i, k, iFan, nDupGates, nCountMux = 0; assert( Gia_ManHasMapping(p) || p->pMuxes || fFindEnables ); assert( !fFindEnables || !p->pMuxes ); @@ -820,6 +843,8 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs pNtkNew->pName = Extra_UtilStrsav(p->pName); pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec); Gia_ManFillValue( p ); + if ( fCheckAnd5 ) + vCompls = Vec_BitStart( Gia_ManObjNum(p) ); // create constant pConst0 = Abc_NtkCreateNodeConst0( pNtkNew ); Gia_ManConst0(p)->Value = Abc_ObjId(pConst0); @@ -917,6 +942,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs vReflect = Vec_PtrStart( Gia_ManObjNum(p) ); Gia_ManForEachLut( p, i ) { + Hop_Obj_t * pFunc; pObj = Gia_ManObj(p, i); assert( pObj->Value == ~0 ); if ( Gia_ObjLutSize(p, i) == 0 ) @@ -924,10 +950,36 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs pObj->Value = Abc_ObjId(pConst0); continue; } + pFunc = Abc_ObjHopFromGia2( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect, vCompls ); + if ( fCheckAnd5 && Gia_ObjLutSize(p, i) == 5 ) + { + word Truth = Hop_ManComputeTruth6( (Hop_Man_t *)pNtkNew->pManFunc, pFunc, 5 ); + int fCompl = Abc_Tt5AndDecPolarity( Truth ); + if ( fCompl < 0 ) + { + Abc_Print( -1, "Abc_NtkFromMappedGia(): 5-input node %d does not have AND-decomposition in either polarity.\n", i ); + Vec_PtrFree( vReflect ); + Vec_BitFreeP( &vCompls ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + pFunc = Hop_NotCond( pFunc, fCompl ); + Truth = fCompl ? ~Truth : Truth; + assert( Abc_Tt5HasAndDec(Truth) ); + if ( !Abc_Tt5HasAndDec(Truth) ) + { + Abc_Print( -1, "Abc_NtkFromMappedGia(): Internal error: 5-input node %d failed AND-decomposition check.\n", i ); + Vec_PtrFree( vReflect ); + Vec_BitFreeP( &vCompls ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + Vec_BitWriteEntry( vCompls, i, fCompl ); + } pObjNew = Abc_NtkCreateNode( pNtkNew ); Gia_LutForEachFanin( p, i, iFan, k ) Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) ); - pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect ); + pObjNew->pData = pFunc; pObjNew->fPersist = Gia_ObjLutIsMux(p, i) && Gia_ObjLutSize(p, i) == 3; pObj->Value = Abc_ObjId( pObjNew ); } @@ -939,8 +991,12 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs if ( !fFindEnables ) Gia_ManForEachCo( p, pObj, i ) { + int iFanin = Gia_ObjFaninId0p(p, pObj); + int fCompl = Gia_ObjFaninC0(pObj) ^ (vCompls && Vec_BitEntry(vCompls, iFanin)); pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); - Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) ); + if ( fCheckAnd5 && fCompl && Gia_ObjIsLut(p, iFanin) && Gia_ObjLutSize(p, iFanin) == 5 ) + pObjNew = Abc_NtkCreateNodeInv( pNtkNew, pObjNew ), fCompl = 0; + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, fCompl ) ); } // create names Abc_NtkAddDummyPiNames( pNtkNew ); @@ -967,8 +1023,17 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs // check the resulting AIG if ( !Abc_NtkCheck( pNtkNew ) ) Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" ); + Vec_BitFreeP( &vCompls ); return pNtkNew; } +Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs ) +{ + return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, 0 ); +} +Abc_Ntk_t * Abc_NtkFromMappedGiaAnd5( Gia_Man_t * p, int fFindEnables, int fUseBuffs ) +{ + return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, 1 ); +} /**Function************************************************************* diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c index 6311df6d1..145817598 100644 --- a/src/map/if/ifDec07.c +++ b/src/map/if/ifDec07.c @@ -1127,9 +1127,10 @@ int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, cha } int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ) { - if ( nLeaves < nVars ) + if ( nLeaves < p->pPars->nLutSize ) return 1; - assert( nLeaves == nVars ); + assert( nLeaves == p->pPars->nLutSize ); + assert( nLeaves <= nVars ); if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) ) return 1; return 0; @@ -1141,4 +1142,3 @@ int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, cha ABC_NAMESPACE_IMPL_END -