/**CFile**************************************************************** FileName [giaResub.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [Resubstitution.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" #include "misc/vec/vecWec.h" #include "misc/vec/vecQue.h" #include "misc/vec/vecHsh.h" #include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Computes MFFCs of all qualifying nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ObjCheckMffc_rec( Gia_Man_t * p,Gia_Obj_t * pObj, int Limit, Vec_Int_t * vNodes ) { int iFanin; if ( Gia_ObjIsCi(pObj) ) return 1; assert( Gia_ObjIsAnd(pObj) ); iFanin = Gia_ObjFaninId0p(p, pObj); Vec_IntPush( vNodes, iFanin ); if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin0(pObj), Limit, vNodes)) ) return 0; iFanin = Gia_ObjFaninId1p(p, pObj); Vec_IntPush( vNodes, iFanin ); if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin1(pObj), Limit, vNodes)) ) return 0; if ( !Gia_ObjIsMux(p, pObj) ) return 1; iFanin = Gia_ObjFaninId2p(p, pObj); Vec_IntPush( vNodes, iFanin ); if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin2(p, pObj), Limit, vNodes)) ) return 0; return 1; } static inline int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners ) { int RetValue, iObj, i; Vec_IntClear( vNodes ); RetValue = Gia_ObjCheckMffc_rec( p, pRoot, Limit, vNodes ); if ( RetValue ) { Vec_IntClear( vLeaves ); Vec_IntClear( vInners ); Vec_IntSort( vNodes, 0 ); Vec_IntForEachEntry( vNodes, iObj, i ) if ( Gia_ObjRefNumId(p, iObj) > 0 || Gia_ObjIsCi(Gia_ManObj(p, iObj)) ) { if ( !Vec_IntSize(vLeaves) || Vec_IntEntryLast(vLeaves) != iObj ) Vec_IntPush( vLeaves, iObj ); } else { if ( !Vec_IntSize(vInners) || Vec_IntEntryLast(vInners) != iObj ) Vec_IntPush( vInners, iObj ); } Vec_IntPush( vInners, Gia_ObjId(p, pRoot) ); } Vec_IntForEachEntry( vNodes, iObj, i ) Gia_ObjRefIncId( p, iObj ); return RetValue; } Vec_Wec_t * Gia_ManComputeMffcs( Gia_Man_t * p, int LimitMin, int LimitMax, int SuppMax, int RatioBest ) { Gia_Obj_t * pObj; Vec_Wec_t * vMffcs; Vec_Int_t * vNodes, * vLeaves, * vInners, * vMffc; int i, iPivot; assert( p->pMuxes ); vNodes = Vec_IntAlloc( 2 * LimitMax ); vLeaves = Vec_IntAlloc( 2 * LimitMax ); vInners = Vec_IntAlloc( 2 * LimitMax ); vMffcs = Vec_WecAlloc( 1000 ); Gia_ManCreateRefs( p ); Gia_ManForEachAnd( p, pObj, i ) { if ( !Gia_ObjRefNum(p, pObj) ) continue; if ( !Gia_ObjCheckMffc(p, pObj, LimitMax, vNodes, vLeaves, vInners) ) continue; if ( Vec_IntSize(vInners) < LimitMin ) continue; if ( Vec_IntSize(vLeaves) > SuppMax ) continue; // improve cut // collect cut vMffc = Vec_WecPushLevel( vMffcs ); Vec_IntGrow( vMffc, Vec_IntSize(vLeaves) + Vec_IntSize(vInners) + 20 ); Vec_IntPush( vMffc, i ); Vec_IntPush( vMffc, Vec_IntSize(vLeaves) ); Vec_IntPush( vMffc, Vec_IntSize(vInners) ); Vec_IntAppend( vMffc, vLeaves ); // Vec_IntAppend( vMffc, vInners ); // add last entry equal to the ratio Vec_IntPush( vMffc, 1000 * Vec_IntSize(vInners) / Vec_IntSize(vLeaves) ); } Vec_IntFree( vNodes ); Vec_IntFree( vLeaves ); Vec_IntFree( vInners ); // sort MFFCs by their inner/leaf ratio Vec_WecSortByLastInt( vMffcs, 1 ); Vec_WecForEachLevel( vMffcs, vMffc, i ) Vec_IntPop( vMffc ); // remove those whose ratio is not good iPivot = RatioBest * Vec_WecSize(vMffcs) / 100; Vec_WecForEachLevelStart( vMffcs, vMffc, i, iPivot ) Vec_IntErase( vMffc ); assert( iPivot <= Vec_WecSize(vMffcs) ); Vec_WecShrink( vMffcs, iPivot ); return vMffcs; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManPrintDivStats( Gia_Man_t * p, Vec_Wec_t * vMffcs, Vec_Wec_t * vPivots ) { int fVerbose = 0; Vec_Int_t * vMffc; int i, nDivs, nDivsAll = 0, nDivs0 = 0; Vec_WecForEachLevel( vMffcs, vMffc, i ) { nDivs = Vec_IntSize(vMffc) - 3 - Vec_IntEntry(vMffc, 1) - Vec_IntEntry(vMffc, 2); nDivs0 += (nDivs == 0); nDivsAll += nDivs; if ( !fVerbose ) continue; printf( "%6d : ", Vec_IntEntry(vMffc, 0) ); printf( "Leaf =%3d ", Vec_IntEntry(vMffc, 1) ); printf( "Mffc =%4d ", Vec_IntEntry(vMffc, 2) ); printf( "Divs =%4d ", nDivs ); printf( "\n" ); } printf( "Collected %d (%.1f %%) MFFCs and %d (%.1f %%) have no divisors (div ave for others is %.2f).\n", Vec_WecSize(vMffcs), 100.0 * Vec_WecSize(vMffcs) / Gia_ManAndNum(p), nDivs0, 100.0 * nDivs0 / Gia_ManAndNum(p), 1.0*nDivsAll/Abc_MaxInt(1, Vec_WecSize(vMffcs) - nDivs0) ); printf( "Using %.2f MB for MFFCs and %.2f MB for pivots. ", Vec_WecMemory(vMffcs)/(1<<20), Vec_WecMemory(vPivots)/(1<<20) ); } /**Function************************************************************* Synopsis [Compute divisors and Boolean functions for the nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManAddDivisors( Gia_Man_t * p, Vec_Wec_t * vMffcs ) { Vec_Wec_t * vPivots; Vec_Int_t * vMffc, * vPivot, * vPivot0, * vPivot1; Vec_Int_t * vCommon, * vCommon2, * vMap; Gia_Obj_t * pObj; int i, k, iObj, iPivot, iMffc; //abctime clkStart = Abc_Clock(); // initialize pivots (mapping of nodes into MFFCs whose leaves they are) vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); vPivots = Vec_WecStart( Gia_ManObjNum(p) ); Vec_WecForEachLevel( vMffcs, vMffc, i ) { assert( Vec_IntSize(vMffc) == 3 + Vec_IntEntry(vMffc, 1) ); iPivot = Vec_IntEntry( vMffc, 0 ); Vec_IntWriteEntry( vMap, iPivot, i ); // iterate through the MFFC leaves Vec_IntForEachEntryStart( vMffc, iObj, k, 3 ) { vPivot = Vec_WecEntry( vPivots, iObj ); if ( Vec_IntSize(vPivot) == 0 ) Vec_IntGrow(vPivot, 4); Vec_IntPush( vPivot, iPivot ); } } Vec_WecForEachLevel( vPivots, vPivot, i ) Vec_IntSort( vPivot, 0 ); // create pivots for internal nodes while growing MFFCs vCommon = Vec_IntAlloc( 100 ); vCommon2 = Vec_IntAlloc( 100 ); Gia_ManForEachAnd( p, pObj, i ) { // find commont pivots // the slow down happens because some PIs have very large sets of pivots vPivot0 = Vec_WecEntry( vPivots, Gia_ObjFaninId0(pObj, i) ); vPivot1 = Vec_WecEntry( vPivots, Gia_ObjFaninId1(pObj, i) ); Vec_IntTwoFindCommon( vPivot0, vPivot1, vCommon ); if ( Gia_ObjIsMuxId(p, i) ) { vPivot = Vec_WecEntry( vPivots, Gia_ObjFaninId2(p, i) ); Vec_IntTwoFindCommon( vPivot, vCommon, vCommon2 ); ABC_SWAP( Vec_Int_t *, vCommon, vCommon2 ); } if ( Vec_IntSize(vCommon) == 0 ) continue; // add new pivots (this trick increased memory used in vPivots) vPivot = Vec_WecEntry( vPivots, i ); Vec_IntTwoMerge2( vPivot, vCommon, vCommon2 ); ABC_SWAP( Vec_Int_t, *vPivot, *vCommon2 ); // grow MFFCs Vec_IntForEachEntry( vCommon, iObj, k ) { iMffc = Vec_IntEntry( vMap, iObj ); assert( iMffc != -1 ); vMffc = Vec_WecEntry( vMffcs, iMffc ); Vec_IntPush( vMffc, i ); } } //Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); Vec_IntFree( vCommon ); Vec_IntFree( vCommon2 ); Vec_IntFree( vMap ); Gia_ManPrintDivStats( p, vMffcs, vPivots ); Vec_WecFree( vPivots ); // returns the modified array of MFFCs } void Gia_ManResubTest( Gia_Man_t * p ) { Vec_Wec_t * vMffcs; Gia_Man_t * pNew = Gia_ManDupMuxes( p, 2 ); abctime clkStart = Abc_Clock(); vMffcs = Gia_ManComputeMffcs( pNew, 4, 100, 8, 100 ); Gia_ManAddDivisors( pNew, vMffcs ); Vec_WecFree( vMffcs ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); Gia_ManStop( pNew ); } /**Function************************************************************* Synopsis [Resubstitution data-structure.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ typedef struct Gia_ResbMan_t_ Gia_ResbMan_t; struct Gia_ResbMan_t_ { int nWords; int nLimit; int nDivsMax; int iChoice; int fUseXor; int fDebug; int fVerbose; int fVeryVerbose; Vec_Ptr_t * vDivs; Vec_Int_t * vGates; Vec_Int_t * vUnateLits[2]; Vec_Int_t * vNotUnateVars[2]; Vec_Int_t * vUnatePairs[2]; Vec_Int_t * vBinateVars; Vec_Int_t * vUnateLitsW[2]; Vec_Int_t * vUnatePairsW[2]; Vec_Wec_t * vSorter; word * pSets[2]; word * pDivA; word * pDivB; Vec_Wrd_t * vSims; }; Gia_ResbMan_t * Gia_ResbAlloc( int nWords ) { Gia_ResbMan_t * p = ABC_CALLOC( Gia_ResbMan_t, 1 ); p->nWords = nWords; p->vUnateLits[0] = Vec_IntAlloc( 100 ); p->vUnateLits[1] = Vec_IntAlloc( 100 ); p->vNotUnateVars[0] = Vec_IntAlloc( 100 ); p->vNotUnateVars[1] = Vec_IntAlloc( 100 ); p->vUnatePairs[0] = Vec_IntAlloc( 100 ); p->vUnatePairs[1] = Vec_IntAlloc( 100 ); p->vUnateLitsW[0] = Vec_IntAlloc( 100 ); p->vUnateLitsW[1] = Vec_IntAlloc( 100 ); p->vUnatePairsW[0] = Vec_IntAlloc( 100 ); p->vUnatePairsW[1] = Vec_IntAlloc( 100 ); p->vSorter = Vec_WecAlloc( nWords*64 ); p->vBinateVars = Vec_IntAlloc( 100 ); p->vGates = Vec_IntAlloc( 100 ); p->vDivs = Vec_PtrAlloc( 100 ); p->pSets[0] = ABC_CALLOC( word, nWords ); p->pSets[1] = ABC_CALLOC( word, nWords ); p->pDivA = ABC_CALLOC( word, nWords ); p->pDivB = ABC_CALLOC( word, nWords ); p->vSims = Vec_WrdAlloc( 100 ); return p; } void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int fVeryVerbose ) { assert( p->nWords == nWords ); p->nLimit = nLimit; p->nDivsMax = nDivsMax; p->iChoice = iChoice; p->fUseXor = fUseXor; p->fDebug = fDebug; p->fVerbose = fVerbose; p->fVeryVerbose = fVeryVerbose; Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 ); Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 ); Vec_PtrClear( p->vDivs ); Vec_PtrAppend( p->vDivs, vDivs ); Vec_IntClear( p->vGates ); Vec_IntClear( p->vUnateLits[0] ); Vec_IntClear( p->vUnateLits[1] ); Vec_IntClear( p->vNotUnateVars[0] ); Vec_IntClear( p->vNotUnateVars[1] ); Vec_IntClear( p->vUnatePairs[0] ); Vec_IntClear( p->vUnatePairs[1] ); Vec_IntClear( p->vUnateLitsW[0] ); Vec_IntClear( p->vUnateLitsW[1] ); Vec_IntClear( p->vUnatePairsW[0] ); Vec_IntClear( p->vUnatePairsW[1] ); Vec_IntClear( p->vBinateVars ); } void Gia_ResbFree( Gia_ResbMan_t * p ) { Vec_IntFree( p->vUnateLits[0] ); Vec_IntFree( p->vUnateLits[1] ); Vec_IntFree( p->vNotUnateVars[0] ); Vec_IntFree( p->vNotUnateVars[1] ); Vec_IntFree( p->vUnatePairs[0] ); Vec_IntFree( p->vUnatePairs[1] ); Vec_IntFree( p->vUnateLitsW[0] ); Vec_IntFree( p->vUnateLitsW[1] ); Vec_IntFree( p->vUnatePairsW[0] ); Vec_IntFree( p->vUnatePairsW[1] ); Vec_IntFree( p->vBinateVars ); Vec_IntFree( p->vGates ); Vec_WrdFree( p->vSims ); Vec_PtrFree( p->vDivs ); Vec_WecFree( p->vSorter ); ABC_FREE( p->pSets[0] ); ABC_FREE( p->pSets[1] ); ABC_FREE( p->pDivA ); ABC_FREE( p->pDivB ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Print resubstitution.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManResubPrintNode( Vec_Int_t * vRes, int nVars, int Node, int fCompl ) { extern void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ); int iLit0 = Vec_IntEntry( vRes, 2*Node + 0 ); int iLit1 = Vec_IntEntry( vRes, 2*Node + 1 ); assert( iLit0 != iLit1 ); if ( iLit0 > iLit1 && Abc_LitIsCompl(fCompl) ) // xor { printf( "~" ); fCompl = 0; } printf( "(" ); Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit0, fCompl) ); printf( " %c ", iLit0 > iLit1 ? '^' : (fCompl ? '|' : '&') ); Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit1, fCompl) ); printf( ")" ); } void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ) { if ( Abc_Lit2Var(iLit) < nVars ) { if ( nVars < 26 ) printf( "%s%c", Abc_LitIsCompl(iLit) ? "~":"", 'a' + Abc_Lit2Var(iLit)-2 ); else printf( "%si%d", Abc_LitIsCompl(iLit) ? "~":"", Abc_Lit2Var(iLit)-2 ); } else Gia_ManResubPrintNode( vRes, nVars, Abc_Lit2Var(iLit) - nVars, Abc_LitIsCompl(iLit) ); } int Gia_ManResubPrint( Vec_Int_t * vRes, int nVars ) { int iTopLit; if ( Vec_IntSize(vRes) == 0 ) return printf( "none" ); assert( Vec_IntSize(vRes) % 2 == 1 ); iTopLit = Vec_IntEntryLast(vRes); if ( iTopLit == 0 ) return printf( "const0" ); if ( iTopLit == 1 ) return printf( "const1" ); Gia_ManResubPrintLit( vRes, nVars, iTopLit ); return 0; } /**Function************************************************************* Synopsis [Verify resubstitution.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManResubVerify( Gia_ResbMan_t * p, word * pFunc ) { int nVars = Vec_PtrSize(p->vDivs); int iTopLit, RetValue; word * pDivRes; if ( Vec_IntSize(p->vGates) == 0 ) return -1; iTopLit = Vec_IntEntryLast(p->vGates); assert( iTopLit >= 0 ); if ( iTopLit == 0 ) { if ( pFunc ) Abc_TtClear( pFunc, p->nWords ); return Abc_TtIsConst0( p->pSets[1], p->nWords ); } if ( iTopLit == 1 ) { if ( pFunc ) Abc_TtFill( pFunc, p->nWords ); return Abc_TtIsConst0( p->pSets[0], p->nWords ); } if ( Abc_Lit2Var(iTopLit) < nVars ) { assert( Vec_IntSize(p->vGates) == 1 ); pDivRes = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iTopLit) ); } else { int i, iLit0, iLit1; assert( Vec_IntSize(p->vGates) > 1 ); assert( Vec_IntSize(p->vGates) % 2 == 1 ); assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(p->vGates)/2-1 ); Vec_WrdFill( p->vSims, p->nWords * Vec_IntSize(p->vGates)/2, 0 ); Vec_IntForEachEntryDouble( p->vGates, iLit0, iLit1, i ) { int iVar0 = Abc_Lit2Var(iLit0); int iVar1 = Abc_Lit2Var(iLit1); word * pDiv0 = iVar0 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar0) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar0 - nVars)); word * pDiv1 = iVar1 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar1) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar1 - nVars)); word * pDiv = Vec_WrdEntryP(p->vSims, p->nWords*i/2); if ( iVar0 < iVar1 ) Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), p->nWords ); else if ( iVar0 > iVar1 ) { assert( !Abc_LitIsCompl(iLit0) ); assert( !Abc_LitIsCompl(iLit1) ); Abc_TtXor( pDiv, pDiv0, pDiv1, p->nWords, 0 ); } else assert( 0 ); } pDivRes = Vec_WrdEntryP( p->vSims, p->nWords*(Vec_IntSize(p->vGates)/2-1) ); } if ( Abc_LitIsCompl(iTopLit) ) RetValue = !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 1, p->nWords); else RetValue = !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 1, p->nWords); if ( pFunc ) Abc_TtCopy( pFunc, pDivRes, p->nWords, Abc_LitIsCompl(iTopLit) ); return RetValue; } /**Function************************************************************* Synopsis [Construct AIG manager from gates.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManConstructFromMap( Gia_Man_t * pNew, Vec_Int_t * vGates, int nVars, Vec_Int_t * vUsed, Vec_Int_t * vCopy, int fHash ) { int i, iLit0, iLit1, iLitRes, iTopLit = Vec_IntEntryLast( vGates ); assert( Vec_IntSize(vUsed) == nVars ); assert( Vec_IntSize(vGates) > 1 ); assert( Vec_IntSize(vGates) % 2 == 1 ); assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(vGates)/2-1 ); Vec_IntClear( vCopy ); Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i ) { int iVar0 = Abc_Lit2Var(iLit0); int iVar1 = Abc_Lit2Var(iLit1); int iRes0 = iVar0 < nVars ? Vec_IntEntry(vUsed, iVar0) : Vec_IntEntry(vCopy, iVar0 - nVars); int iRes1 = iVar1 < nVars ? Vec_IntEntry(vUsed, iVar1) : Vec_IntEntry(vCopy, iVar1 - nVars); if ( iVar0 < iVar1 ) { if ( fHash ) iLitRes = Gia_ManHashAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); else iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); } else if ( iVar0 > iVar1 ) { assert( !Abc_LitIsCompl(iLit0) ); assert( !Abc_LitIsCompl(iLit1) ); if ( fHash ) iLitRes = Gia_ManHashXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); else iLitRes = Gia_ManAppendXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); } else assert( 0 ); Vec_IntPush( vCopy, iLitRes ); } assert( Vec_IntSize(vCopy) == Vec_IntSize(vGates)/2 ); iLitRes = Vec_IntEntry( vCopy, Vec_IntSize(vGates)/2-1 ); return iLitRes; } Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nDivs ) { Vec_Int_t * vGates; int i, k, iLit; Vec_Int_t * vCopy = Vec_IntAlloc( 100 ); Vec_Int_t * vUsed = Vec_IntStartFull( nDivs ); Gia_Man_t * pNew = Gia_ManStart( 100 ); pNew->pName = Abc_UtilStrsav( "resub" ); Vec_WecForEachLevel( vFuncs, vGates, i ) { assert( Vec_IntSize(vGates) % 2 == 1 ); Vec_IntForEachEntry( vGates, iLit, k ) { int iVar = Abc_Lit2Var(iLit); if ( iVar > 0 && iVar < nDivs && Vec_IntEntry(vUsed, iVar) == -1 ) Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) ); } } Vec_WecForEachLevel( vFuncs, vGates, i ) { int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); if ( Abc_Lit2Var(iTopLit) == 0 ) iLitRes = 0; else if ( Abc_Lit2Var(iTopLit) < nDivs ) iLitRes = Vec_IntEntry( vUsed, Abc_Lit2Var(iTopLit) ); else iLitRes = Gia_ManConstructFromMap( pNew, vGates, nDivs, vUsed, vCopy, 0 ); Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ) ); } Vec_IntFree( vCopy ); Vec_IntFree( vUsed ); return pNew; } Gia_Man_t * Gia_ManConstructFromGates2( Vec_Wec_t * vFuncs, Vec_Wec_t * vDivs, int nObjs, Vec_Int_t ** pvSupp ) { Vec_Int_t * vGates; int i, k, iVar, iLit; Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); Vec_Int_t * vCopy = Vec_IntAlloc( 100 ); Vec_Wec_t * vUseds = Vec_WecStart( Vec_WecSize(vDivs) ); Vec_Int_t * vMap = Vec_IntStartFull( nObjs ); Gia_Man_t * pNew = Gia_ManStart( 100 ); pNew->pName = Abc_UtilStrsav( "resub" ); assert( Vec_WecSize(vFuncs) == Vec_WecSize(vDivs) ); Vec_WecForEachLevel( vFuncs, vGates, i ) { Vec_Int_t * vDiv = Vec_WecEntry( vDivs, i ); assert( Vec_IntSize(vGates) % 2 == 1 ); Vec_IntForEachEntry( vGates, iLit, k ) { int iVar = Abc_Lit2Var(iLit); if ( iVar > 0 && iVar < Vec_IntSize(vDiv) && Vec_IntEntry(vMap, Vec_IntEntry(vDiv, iVar)) == -1 ) Vec_IntWriteEntry( vMap, Vec_IntPushReturn(vSupp, Vec_IntEntry(vDiv, iVar)), 0 ); } } Vec_IntSort( vSupp, 0 ); Vec_IntForEachEntry( vSupp, iVar, k ) Vec_IntWriteEntry( vMap, iVar, Gia_ManAppendCi(pNew) ); Vec_WecForEachLevel( vFuncs, vGates, i ) { Vec_Int_t * vDiv = Vec_WecEntry( vDivs, i ); Vec_Int_t * vUsed = Vec_WecEntry( vUseds, i ); Vec_IntFill( vUsed, Vec_IntSize(vDiv), -1 ); Vec_IntForEachEntry( vGates, iLit, k ) { int iVar = Abc_Lit2Var(iLit); if ( iVar > 0 && iVar < Vec_IntSize(vDiv) ) { assert( Vec_IntEntry(vMap, Vec_IntEntry(vDiv, iVar)) > 0 ); Vec_IntWriteEntry( vUsed, iVar, Vec_IntEntry(vMap, Vec_IntEntry(vDiv, iVar)) ); } } } Vec_WecForEachLevel( vFuncs, vGates, i ) { Vec_Int_t * vDiv = Vec_WecEntry( vDivs, i ); Vec_Int_t * vUsed = Vec_WecEntry( vUseds, i ); int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); if ( Abc_Lit2Var(iTopLit) == 0 ) iLitRes = 0; else if ( Abc_Lit2Var(iTopLit) < Vec_IntSize(vDiv) ) iLitRes = Vec_IntEntry( vUsed, Abc_Lit2Var(iTopLit) ); else iLitRes = Gia_ManConstructFromMap( pNew, vGates, Vec_IntSize(vDiv), vUsed, vCopy, 0 ); Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ) ); } Vec_IntFree( vMap ); Vec_IntFree( vCopy ); Vec_WecFree( vUseds ); if ( pvSupp ) *pvSupp = vSupp; else Vec_IntFree( vSupp ); return pNew; } Vec_Int_t * Gia_ManToGates( Gia_Man_t * p ) { Vec_Int_t * vRes = Vec_IntAlloc( 2*Gia_ManAndNum(p) + 1 ); Gia_Obj_t * pRoot = Gia_ManCo( p, 0 ); int iRoot = Gia_ObjFaninId0p(p, pRoot) - 1; int nVars = Gia_ManCiNum(p); assert( Gia_ManCoNum(p) == 1 ); if ( iRoot == -1 ) Vec_IntPush( vRes, Gia_ObjFaninC0(pRoot) ); else if ( iRoot < nVars ) Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) ); else { Gia_Obj_t * pObj, * pLast = NULL; int i; Gia_ManForEachCi( p, pObj, i ) assert( Gia_ObjId(p, pObj) == i+1 ); Gia_ManForEachAnd( p, pObj, i ) { int iLit0 = Abc_Var2Lit( Gia_ObjFaninId0(pObj, i) - 1, Gia_ObjFaninC0(pObj) ); int iLit1 = Abc_Var2Lit( Gia_ObjFaninId1(pObj, i) - 1, Gia_ObjFaninC1(pObj) ); if ( iLit0 > iLit1 ) iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1; Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 ); pLast = pObj; } assert( pLast == Gia_ObjFanin0(pRoot) ); Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) ); } assert( Vec_IntSize(vRes) == 2*Gia_ManAndNum(p) + 1 ); return vRes; } /**Function************************************************************* Synopsis [Construct AIG manager from gates.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManInsertOrder_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs, Vec_Int_t * vNodes ) { Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); if ( iObj == 0 ) return; if ( pObj->fPhase ) { int nVars = Gia_ManObjNum(p); int k, iLit, Index = Vec_IntFind( vObjs, iObj ); Vec_Int_t * vGates = Vec_WecEntry( vFuncs, Index ); assert( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) ); Vec_IntForEachEntry( vGates, iLit, k ) if ( Abc_Lit2Var(iLit) < nVars ) Gia_ManInsertOrder_rec( p, Abc_Lit2Var(iLit), vObjs, vFuncs, vNodes ); } else if ( Gia_ObjIsCo(pObj) ) Gia_ManInsertOrder_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, vFuncs, vNodes ); else if ( Gia_ObjIsAnd(pObj) ) { Gia_ManInsertOrder_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, vFuncs, vNodes ); Gia_ManInsertOrder_rec( p, Gia_ObjFaninId1p(p, pObj), vObjs, vFuncs, vNodes ); } else assert( Gia_ObjIsCi(pObj) ); if ( !Gia_ObjIsCi(pObj) ) Vec_IntPush( vNodes, iObj ); } Vec_Int_t * Gia_ManInsertOrder( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs ) { int i, Id; Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); Gia_ManForEachCoId( p, Id, i ) Gia_ManInsertOrder_rec( p, Id, vObjs, vFuncs, vNodes ); return vNodes; } Gia_Man_t * Gia_ManInsertFromGates( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, nVars = Gia_ManObjNum(p); Vec_Int_t * vUsed = Vec_IntStartFull( nVars ); Vec_Int_t * vNodes, * vCopy = Vec_IntAlloc(100); Gia_ManForEachObjVec( vObjs, p, pObj, i ) pObj->fPhase = 1; vNodes = Gia_ManInsertOrder( p, vObjs, vFuncs ); pNew = Gia_ManStart( Gia_ManObjNum(p) + 1000 ); Gia_ManHashStart( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManForEachObjVec( vNodes, p, pObj, i ) if ( !pObj->fPhase ) { if ( Gia_ObjIsCo(pObj) ) pObj->Value = Gia_ObjFanin0Copy(pObj); else if ( Gia_ObjIsAnd(pObj) ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); else assert( 0 ); } else { int k, iLit, Index = Vec_IntFind( vObjs, Gia_ObjId(p, pObj) ); Vec_Int_t * vGates = Vec_WecEntry( vFuncs, Index ); int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); if ( Abc_Lit2Var(iTopLit) == 0 ) iLitRes = 0; else if ( Abc_Lit2Var(iTopLit) < nVars ) iLitRes = Gia_ManObj(p, Abc_Lit2Var(iTopLit))->Value; else { Vec_IntForEachEntry( vGates, iLit, k ) Vec_IntWriteEntry( vUsed, Abc_Lit2Var(iLit), Gia_ManObj(p, Abc_Lit2Var(iLit))->Value ); iLitRes = Gia_ManConstructFromMap( pNew, vGates, nVars, vUsed, vCopy, 1 ); Vec_IntForEachEntry( vGates, iLit, k ) Vec_IntWriteEntry( vUsed, Abc_Lit2Var(iLit), -1 ); } pObj->Value = Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ); } Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, pObj->Value ); Gia_ManForEachObjVec( vObjs, p, pObj, i ) pObj->fPhase = 0; Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); Vec_IntFree( vNodes ); Vec_IntFree( vUsed ); Vec_IntFree( vCopy ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); return pNew; } /**Function************************************************************* Synopsis [Perform resubstitution.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2, int fVerbose ) { int * pBeg1 = vArr1->pArray; int * pBeg2 = vArr2->pArray; int * pEnd1 = vArr1->pArray + vArr1->nSize; int * pEnd2 = vArr2->pArray + vArr2->nSize; int * pStart1 = vArr1->pArray; int * pStart2 = vArr2->pArray; int nRemoved = 0; while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) ) { if ( *pBeg1 != *pBeg2 ) return *pBeg1; else pBeg1++, pBeg2++; nRemoved++; } else if ( *pBeg1 < *pBeg2 ) *pStart1++ = *pBeg1++; else *pStart2++ = *pBeg2++; } while ( pBeg1 < pEnd1 ) *pStart1++ = *pBeg1++; while ( pBeg2 < pEnd2 ) *pStart2++ = *pBeg2++; Vec_IntShrink( vArr1, pStart1 - vArr1->pArray ); Vec_IntShrink( vArr2, pStart2 - vArr2->pArray ); //if ( fVerbose ) printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) ); return -1; } void Gia_ManFindOneUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vNotUnateVars ) { word * pDiv; int i; Vec_IntClear( vUnateLits ); Vec_IntClear( vNotUnateVars ); Vec_PtrForEachEntryStart( word *, vDivs, pDiv, i, 2 ) if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 0, nWords ) ) Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 0) ); else if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 1, nWords ) ) Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 1) ); else Vec_IntPush( vNotUnateVars, i ); } int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose ) { int n; if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { Gia_ManFindOneUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vNotUnateVars[n] ); if ( fVerbose ) printf( "U%d =%4d ", n, Vec_IntSize(vUnateLits[n]) ); } return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1], fVerbose ); } static inline int Gia_ManDivCover( word * pOff, word * pOn, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords ) { //assert( !Abc_TtIntersectOne(pOff, 0, pDivA, ComplA, nWords) ); //assert( !Abc_TtIntersectOne(pOff, 0, pDivB, ComplB, nWords) ); return !Abc_TtIntersectTwo( pOn, 0, pDivA, !ComplA, pDivB, !ComplB, nWords ); } int Gia_ManFindTwoUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, int * pnPairs ) { int i, k, iDiv0_, iDiv1_, Cover0, Cover1; int nTotal = Abc_TtCountOnesVec( pOn, nWords ); (*pnPairs) = 0; Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0_, Cover0, i ) { if ( 2*Cover0 < nTotal ) break; Vec_IntForEachEntryTwoStart( vUnateLits, vUnateLitsW, iDiv1_, Cover1, k, i+1 ) { int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); if ( Cover0 + Cover1 < nTotal ) break; (*pnPairs)++; if ( Gia_ManDivCover(pOff, pOn, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) ) return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1); } } return -1; } int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int fVerbose ) { int n, iLit, nPairs; if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { //int nPairsAll = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2; iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], &nPairs ); if ( fVerbose ) printf( "UU%d =%5d ", n, nPairs ); if ( iLit >= 0 ) return Abc_LitNotCond(iLit, n); } return -1; } void Gia_ManFindXorInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) { int i, k, iDiv0_, iDiv1_; int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) { int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 0, nWords ) ) Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 0) ); else if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 1, nWords ) ) Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) ); } } int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) { int n; if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { Vec_IntClear( vUnatePairs[n] ); Gia_ManFindXorInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); if ( fVerbose ) printf( "UX%d =%5d ", n, Vec_IntSize(vUnatePairs[n]) ); } return Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); } void Gia_ManFindUnatePairsInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) { int n, i, k, iDiv0_, iDiv1_; int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) { int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); for ( n = 0; n < 4; n++ ) { int iLit0 = Abc_Var2Lit( iDiv0, n&1 ); int iLit1 = Abc_Var2Lit( iDiv1, n>>1 ); //if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) && Abc_TtIntersectTwo( pOn, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) ); } } } void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) { int n, RetValue; if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { int nBefore = Vec_IntSize(vUnatePairs[n]); Gia_ManFindUnatePairsInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); if ( fVerbose ) printf( "UP%d =%5d ", n, Vec_IntSize(vUnatePairs[n])-nBefore ); } RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); assert( RetValue == -1 ); } void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes ) { int fComp = Abc_LitIsCompl(iDiv); int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; int iDiv1 = Abc_Lit2Var(iDiv) >> 15; word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); if ( iDiv0 < iDiv1 ) { assert( !fComp ); Abc_TtAndCompl( pRes, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords ); } else { assert( !Abc_LitIsCompl(iDiv0) ); assert( !Abc_LitIsCompl(iDiv1) ); Abc_TtXor( pRes, pDiv0, pDiv1, nWords, 0 ); } } int Gia_ManFindDivGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnateLitsW, Vec_Int_t * vUnatePairsW, word * pDivTemp ) { int i, k, iDiv0, iDiv1, Cover0, Cover1; int nTotal = Abc_TtCountOnesVec( pOn, nWords ); Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0, Cover0, i ) { word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); if ( 2*Cover0 < nTotal ) break; Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv1, Cover1, k ) { int fComp1 = Abc_LitIsCompl(iDiv1); if ( Cover0 + Cover1 < nTotal ) break; Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp ); if ( Gia_ManDivCover(pOff, pOn, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) ) return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1); } } return -1; } int Gia_ManFindDivGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnateLitsW[2], Vec_Int_t * vUnatePairsW[2], word * pDivTemp ) { int n, iLit; for ( n = 0; n < 2; n++ ) { iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], vUnateLitsW[n], vUnatePairsW[n], pDivTemp ); if ( iLit >= 0 ) return Abc_LitNotCond( iLit, n ); } return -1; } int Gia_ManFindGateGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, word * pDivTempA, word * pDivTempB ) { int i, k, iDiv0, iDiv1, Cover0, Cover1; int nTotal = Abc_TtCountOnesVec( pOn, nWords ); Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv0, Cover0, k ) { int fCompA = Abc_LitIsCompl(iDiv0); if ( 2*Cover0 < nTotal ) break; Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA ); Vec_IntForEachEntryTwoStart( vUnatePairs, vUnatePairsW, iDiv1, Cover1, i, k+1 ) { int fCompB = Abc_LitIsCompl(iDiv1); if ( Cover0 + Cover1 < nTotal ) break; Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB ); if ( Gia_ManDivCover(pOff, pOn, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1); } } return -1; } int Gia_ManFindGateGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], word * pDivTempA, word * pDivTempB ) { int n, iLit; for ( n = 0; n < 2; n++ ) { iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n], pDivTempA, pDivTempB ); if ( iLit >= 0 ) return Abc_LitNotCond( iLit, n ); } return -1; } void Gia_ManSortUnatesInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, Vec_Wec_t * vSorter ) { int i, k, iLit; Vec_Int_t * vLevel; Vec_WecInit( vSorter, nWords*64 ); Vec_IntForEachEntry( vUnateLits, iLit, i ) { word * pDiv = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iLit)); //assert( !Abc_TtIntersectOne( pOff, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) ); Vec_WecPush( vSorter, Abc_TtCountOnesVecMask(pDiv, pOn, nWords, Abc_LitIsCompl(iLit)), iLit ); } Vec_IntClear( vUnateLits ); Vec_IntClear( vUnateLitsW ); Vec_WecForEachLevelReverse( vSorter, vLevel, k ) Vec_IntForEachEntry( vLevel, iLit, i ) { Vec_IntPush( vUnateLits, iLit ); Vec_IntPush( vUnateLitsW, k ); } //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); Vec_WecClear( vSorter ); } void Gia_ManSortUnates( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) { int n; for ( n = 0; n < 2; n++ ) Gia_ManSortUnatesInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); } void Gia_ManSortPairsInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, Vec_Wec_t * vSorter ) { int i, k, iPair; Vec_Int_t * vLevel; Vec_WecInit( vSorter, nWords*64 ); Vec_IntForEachEntry( vUnatePairs, iPair, i ) { int fComp = Abc_LitIsCompl(iPair); int iLit0 = Abc_Lit2Var(iPair) & 0x7FFF; int iLit1 = Abc_Lit2Var(iPair) >> 15; word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) ); word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) ); if ( iLit0 < iLit1 ) { assert( !fComp ); //assert( !Abc_TtIntersectTwo( pOff, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) ); Vec_WecPush( vSorter, Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOn, nWords), iPair ); } else { assert( !Abc_LitIsCompl(iLit0) ); assert( !Abc_LitIsCompl(iLit1) ); //assert( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, fComp, nWords ) ); Vec_WecPush( vSorter, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOn, nWords), iPair ); } } Vec_IntClear( vUnatePairs ); Vec_IntClear( vUnatePairsW ); Vec_WecForEachLevelReverse( vSorter, vLevel, k ) Vec_IntForEachEntry( vLevel, iPair, i ) { Vec_IntPush( vUnatePairs, iPair ); Vec_IntPush( vUnatePairsW, k ); } //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); Vec_WecClear( vSorter ); } void Gia_ManSortPairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) { int n; for ( n = 0; n < 2; n++ ) Gia_ManSortPairsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); } void Gia_ManSortBinate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Wec_t * vSorter ) { Vec_Int_t * vLevel; int nMints[2] = { Abc_TtCountOnesVec(pSets[0], nWords), Abc_TtCountOnesVec(pSets[1], nWords) }; word * pBig = nMints[0] > nMints[1] ? pSets[0] : pSets[1]; word * pSmo = nMints[0] > nMints[1] ? pSets[1] : pSets[0]; int Big = Abc_MaxInt( nMints[0], nMints[1] ); int Smo = Abc_MinInt( nMints[0], nMints[1] ); int i, k, iDiv, Gain; Vec_WecInit( vSorter, nWords*64 ); Vec_IntForEachEntry( vBinateVars, iDiv, i ) { word * pDiv = (word *)Vec_PtrEntry( vDivs, iDiv ); int nInter[2] = { Abc_TtCountOnesVecMask(pBig, pDiv, nWords, 0), Abc_TtCountOnesVecMask(pSmo, pDiv, nWords, 0) }; if ( nInter[0] < Big/2 ) // complement the divisor { nInter[0] = Big - nInter[0]; nInter[1] = Smo - nInter[1]; } assert( nInter[0] >= Big/2 ); Gain = Abc_MaxInt( 0, nInter[0] - Big/2 + Smo/2 - nInter[1] ); Vec_WecPush( vSorter, Gain, iDiv ); } Vec_IntClear( vBinateVars ); Vec_WecForEachLevelReverse( vSorter, vLevel, k ) Vec_IntForEachEntry( vLevel, iDiv, i ) Vec_IntPush( vBinateVars, iDiv ); Vec_WecClear( vSorter ); if ( Vec_IntSize(vBinateVars) > 2000 ) Vec_IntShrink( vBinateVars, 2000 ); } /**Function************************************************************* Synopsis [Perform resubstitution.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManResubFindBestBinate( Gia_ResbMan_t * p ) { int nMintsAll = Abc_TtCountOnesVec(p->pSets[0], p->nWords) + Abc_TtCountOnesVec(p->pSets[1], p->nWords); int i, iDiv, iLitBest = -1, CostBest = -1; //Vec_IntPrint( p->vBinateVars ); //Dau_DsdPrintFromTruth( p->pSets[0], 6 ); //Dau_DsdPrintFromTruth( p->pSets[1], 6 ); Vec_IntForEachEntry( p->vBinateVars, iDiv, i ) { word * pDiv = (word *)Vec_PtrEntry(p->vDivs, iDiv); int nMints0 = Abc_TtCountOnesVecMask( pDiv, p->pSets[0], p->nWords, 0 ); int nMints1 = Abc_TtCountOnesVecMask( pDiv, p->pSets[1], p->nWords, 0 ); if ( CostBest < nMints0 + nMints1 ) { CostBest = nMints0 + nMints1; iLitBest = Abc_Var2Lit( iDiv, 0 ); } if ( CostBest < nMintsAll - nMints0 - nMints1 ) { CostBest = nMintsAll - nMints0 - nMints1; iLitBest = Abc_Var2Lit( iDiv, 1 ); } } return iLitBest; } int Gia_ManResubAddNode( Gia_ResbMan_t * p, int iLit0, int iLit1, int Type ) { int iNode = Vec_PtrSize(p->vDivs) + Vec_IntSize(p->vGates)/2; int fFlip = (Type == 2) ^ (iLit0 > iLit1); int iFan0 = fFlip ? iLit1 : iLit0; int iFan1 = fFlip ? iLit0 : iLit1; assert( iLit0 != iLit1 ); if ( Type == 2 ) assert( iFan0 > iFan1 ); else assert( iFan0 < iFan1 ); Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iFan0, Type==1), Abc_LitNotCond(iFan1, Type==1) ); return Abc_Var2Lit( iNode, Type==1 ); } int Gia_ManResubPerformMux_rec( Gia_ResbMan_t * p, int nLimit, int Depth ) { extern int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth ); int iDivBest, iResLit0, iResLit1, nNodes; word * pDiv, * pCopy[2]; if ( Depth == 0 ) return -1; if ( nLimit < 3 ) return -1; iDivBest = Gia_ManResubFindBestBinate( p ); if ( iDivBest == -1 ) return -1; pCopy[0] = ABC_CALLOC( word, p->nWords ); pCopy[1] = ABC_CALLOC( word, p->nWords ); Abc_TtCopy( pCopy[0], p->pSets[0], p->nWords, 0 ); Abc_TtCopy( pCopy[1], p->pSets[1], p->nWords, 0 ); pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDivBest) ); Abc_TtAndSharp( p->pSets[0], pCopy[0], pDiv, p->nWords, !Abc_LitIsCompl(iDivBest) ); Abc_TtAndSharp( p->pSets[1], pCopy[1], pDiv, p->nWords, !Abc_LitIsCompl(iDivBest) ); nNodes = Vec_IntSize(p->vGates)/2; //iResLit0 = Gia_ManResubPerform_rec( p, nLimit-3 ); iResLit0 = Gia_ManResubPerform_rec( p, nLimit, 0 ); if ( iResLit0 == -1 ) iResLit0 = Gia_ManResubPerformMux_rec( p, nLimit, Depth-1 ); if ( iResLit0 == -1 ) { ABC_FREE( pCopy[0] ); ABC_FREE( pCopy[1] ); return -1; } Abc_TtAndSharp( p->pSets[0], pCopy[0], pDiv, p->nWords, Abc_LitIsCompl(iDivBest) ); Abc_TtAndSharp( p->pSets[1], pCopy[1], pDiv, p->nWords, Abc_LitIsCompl(iDivBest) ); ABC_FREE( pCopy[0] ); ABC_FREE( pCopy[1] ); nNodes = Vec_IntSize(p->vGates)/2 - nNodes; if ( nLimit-nNodes < 3 ) return -1; //iResLit1 = Gia_ManResubPerform_rec( p, nLimit-3-nNodes ); iResLit1 = Gia_ManResubPerform_rec( p, nLimit, 0 ); if ( iResLit1 == -1 ) iResLit1 = Gia_ManResubPerformMux_rec( p, nLimit, Depth-1 ); if ( iResLit1 == -1 ) return -1; else { int iLit0 = Gia_ManResubAddNode( p, Abc_LitNot(iDivBest), iResLit0, 0 ); int iLit1 = Gia_ManResubAddNode( p, iDivBest, iResLit1, 0 ); return Gia_ManResubAddNode( p, iLit0, iLit1, 1 ); } } /**Function************************************************************* Synopsis [Perform resubstitution.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth ) { int TopOneW[2] = {0}, TopTwoW[2] = {0}, Max1, Max2, iResLit, nVars = Vec_PtrSize(p->vDivs); if ( p->fVerbose ) { int nMints[2] = { Abc_TtCountOnesVec(p->pSets[0], p->nWords), Abc_TtCountOnesVec(p->pSets[1], p->nWords) }; printf( " " ); printf( "ISF: " ); printf( "0=%5d (%5.2f %%) ", nMints[0], 100.0*nMints[0]/(64*p->nWords) ); printf( "1=%5d (%5.2f %%) ", nMints[1], 100.0*nMints[1]/(64*p->nWords) ); } if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) ) return 0; if ( Abc_TtIsConst0( p->pSets[0], p->nWords ) ) return 1; iResLit = Gia_ManFindOneUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars, p->fVerbose ); if ( iResLit >= 0 ) // buffer return iResLit; if ( nLimit == 0 ) return -1; Gia_ManSortUnates( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->vSorter ); iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->fVerbose ); if ( iResLit >= 0 ) // and { int iNode = nVars + Vec_IntSize(p->vGates)/2; int fComp = Abc_LitIsCompl(iResLit); int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; int iDiv1 = Abc_Lit2Var(iResLit) >> 15; assert( iDiv0 < iDiv1 ); Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); return Abc_Var2Lit( iNode, fComp ); } Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars ); if ( Depth ) return Gia_ManResubPerformMux_rec( p, nLimit, Depth ); if ( Vec_IntSize(p->vBinateVars) > p->nDivsMax ) Vec_IntShrink( p->vBinateVars, p->nDivsMax ); if ( p->fVerbose ) printf( " B = %3d", Vec_IntSize(p->vBinateVars) ); //Gia_ManSortBinate( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vSorter ); if ( p->fUseXor ) { iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); if ( iResLit >= 0 ) // xor { int iNode = nVars + Vec_IntSize(p->vGates)/2; int fComp = Abc_LitIsCompl(iResLit); int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; int iDiv1 = Abc_Lit2Var(iResLit) >> 15; assert( !Abc_LitIsCompl(iDiv0) ); assert( !Abc_LitIsCompl(iDiv1) ); assert( iDiv0 > iDiv1 ); Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); return Abc_Var2Lit( iNode, fComp ); } } if ( nLimit == 1 ) return -1; Gia_ManFindUnatePairs( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); Gia_ManSortPairs( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->vSorter ); iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->vUnateLitsW, p->vUnatePairsW, p->pDivA ); if ( iResLit >= 0 ) // and(div,pair) { int iNode = nVars + Vec_IntSize(p->vGates)/2; int fComp = Abc_LitIsCompl(iResLit); int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // div int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; int iDiv11 = Abc_Lit2Var(Div1) >> 15; Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) ); return Abc_Var2Lit( iNode+1, fComp ); } // if ( nLimit == 2 ) // return -1; if ( nLimit >= 3 ) { iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->pDivA, p->pDivB ); if ( iResLit >= 0 ) // and(pair,pair) { int iNode = nVars + Vec_IntSize(p->vGates)/2; int fComp = Abc_LitIsCompl(iResLit); int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // pair int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair int Div0 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) ); int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0); int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF; int iDiv01 = Abc_Lit2Var(Div0) >> 15; int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; int iDiv11 = Abc_Lit2Var(Div1) >> 15; Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 ); Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) ); return Abc_Var2Lit( iNode+2, fComp ); } } // if ( nLimit == 3 ) // return -1; if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 ) return -1; TopOneW[0] = Vec_IntSize(p->vUnateLitsW[0]) ? Vec_IntEntry(p->vUnateLitsW[0], 0) : 0; TopOneW[1] = Vec_IntSize(p->vUnateLitsW[1]) ? Vec_IntEntry(p->vUnateLitsW[1], 0) : 0; TopTwoW[0] = Vec_IntSize(p->vUnatePairsW[0]) ? Vec_IntEntry(p->vUnatePairsW[0], 0) : 0; TopTwoW[1] = Vec_IntSize(p->vUnatePairsW[1]) ? Vec_IntEntry(p->vUnatePairsW[1], 0) : 0; Max1 = Abc_MaxInt(TopOneW[0], TopOneW[1]); Max2 = Abc_MaxInt(TopTwoW[0], TopTwoW[1]); if ( Abc_MaxInt(Max1, Max2) == 0 ) return -1; if ( Max1 > Max2/2 ) { if ( nLimit >= 2 && (Max1 == TopOneW[0] || Max1 == TopOneW[1]) ) { int fUseOr = Max1 == TopOneW[0]; int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); int fComp = Abc_LitIsCompl(iDiv); word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); if ( p->fVerbose ) printf( "\n" ); iResLit = Gia_ManResubPerform_rec( p, nLimit-1, Depth ); if ( iResLit >= 0 ) { int iNode = nVars + Vec_IntSize(p->vGates)/2; if ( iDiv < iResLit ) Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); else Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_LitNot(iDiv) ); return Abc_Var2Lit( iNode, fUseOr ); } } if ( Max2 == 0 ) return -1; /* if ( Max2 == TopTwoW[0] || Max2 == TopTwoW[1] ) { int fUseOr = Max2 == TopTwoW[0]; int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); int fComp = Abc_LitIsCompl(iDiv); Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); if ( p->fVerbose ) printf( "\n " ); iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); if ( iResLit >= 0 ) { int iNode = nVars + Vec_IntSize(p->vGates)/2; int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; int iDiv1 = Abc_Lit2Var(iDiv) >> 15; Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); return Abc_Var2Lit( iNode+1, fUseOr ); } } */ } else { if ( nLimit >= 3 && (Max2 == TopTwoW[0] || Max2 == TopTwoW[1]) ) { int fUseOr = Max2 == TopTwoW[0]; int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); int fComp = Abc_LitIsCompl(iDiv); Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); if ( p->fVerbose ) printf( "\n" ); iResLit = Gia_ManResubPerform_rec( p, nLimit-2, Depth ); if ( iResLit >= 0 ) { int iNode = nVars + Vec_IntSize(p->vGates)/2; int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; int iDiv1 = Abc_Lit2Var(iDiv) >> 15; Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); return Abc_Var2Lit( iNode+1, fUseOr ); } } if ( Max1 == 0 ) return -1; /* if ( Max1 == TopOneW[0] || Max1 == TopOneW[1] ) { int fUseOr = Max1 == TopOneW[0]; int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); int fComp = Abc_LitIsCompl(iDiv); word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); if ( p->fVerbose ) printf( "\n " ); iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); if ( iResLit >= 0 ) { int iNode = nVars + Vec_IntSize(p->vGates)/2; Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); return Abc_Var2Lit( iNode, fUseOr ); } } */ } return -1; } void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int Depth ) { int Res; Gia_ResbInit( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, fVerbose ); Res = Gia_ManResubPerform_rec( p, nLimit, Depth ); if ( Res >= 0 ) Vec_IntPush( p->vGates, Res ); else Vec_IntClear( p->vGates ); if ( fVerbose ) printf( "\n" ); } Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc, int Depth ) { Vec_Int_t * vRes; Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); Gia_ManResubPerform( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, Depth ); if ( fVerbose ) Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); //if ( fVerbose ) // printf( "\n" ); if ( !Gia_ManResubVerify(p, pFunc) ) { Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); printf( "Verification FAILED.\n" ); } else if ( fDebug && fVerbose ) printf( "Verification succeeded." ); if ( fVerbose ) printf( "\n" ); vRes = Vec_IntDup( p->vGates ); Gia_ResbFree( p ); return vRes; } /**Function************************************************************* Synopsis [Top level.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static Gia_ResbMan_t * s_pResbMan = NULL; void Abc_ResubPrepareManager( int nWords ) { if ( s_pResbMan != NULL ) Gia_ResbFree( s_pResbMan ); s_pResbMan = NULL; if ( nWords > 0 ) s_pResbMan = Gia_ResbAlloc( nWords ); } int Abc_ResubComputeFunction( void ** ppDivs, int nDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int ** ppArray ) { Vec_Ptr_t Divs = { nDivs, nDivs, ppDivs }; assert( s_pResbMan != NULL ); // first call Abc_ResubPrepareManager() Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose==2, 0 ); if ( fVerbose ) { int nGates = Vec_IntSize(s_pResbMan->vGates)/2; if ( nGates ) { printf( " Gain = %2d Gates = %2d __________ F = ", nLimit+1-nGates, nGates ); Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); printf( "\n" ); } } if ( fDebug ) { if ( !Gia_ManResubVerify(s_pResbMan, NULL) ) { Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); printf( "Verification FAILED.\n" ); } //else // printf( "Verification succeeded.\n" ); } *ppArray = Vec_IntArray(s_pResbMan->vGates); assert( Vec_IntSize(s_pResbMan->vGates)/2 <= nLimit ); return Vec_IntSize(s_pResbMan->vGates); } void Abc_ResubDumpProblem( char * pFileName, void ** ppDivs, int nDivs, int nWords ) { Vec_Wrd_t * vSims = Vec_WrdAlloc( nDivs * nWords ); word ** pDivs = (word **)ppDivs; int d, w; for ( d = 0; d < nDivs; d++ ) for ( w = 0; w < nWords; w++ ) Vec_WrdPush( vSims, pDivs[d][w] ); Vec_WrdDumpHex( pFileName, vSims, nWords, 1 ); Vec_WrdFree( vSims ); } /**Function************************************************************* Synopsis [Top level.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ extern void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars ); extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit ); void Gia_ManResubTest3() { int nVars = 4; int fVerbose = 1; word Divs[6] = { 0, 0, ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xFF00FF00FF00FF00) }; Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 ); Vec_Int_t * vRes = Vec_IntAlloc( 100 ); int i, k, ArraySize, * pArray; for ( i = 0; i < 6; i++ ) Vec_PtrPush( vDivs, Divs+i ); Abc_ResubPrepareManager( 1 ); for ( i = 0; i < (1<<(1<vGates, Vec_PtrSize(vDivs) ); printf( "\n" ); //Vec_PtrFree( vDivs ); Gia_ResbFree( p ); } /**Function************************************************************* Synopsis [Top level.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManCheckResub( Vec_Ptr_t * vDivs, int nWords ) { //int i, nVars = 6, pVarSet[10] = { 2, 189, 2127, 2125, 177, 178 }; int i, nVars = 3, pVarSet[10] = { 2, 3, 4 }; word * pOff = (word *)Vec_PtrEntry( vDivs, 0 ); word * pOn = (word *)Vec_PtrEntry( vDivs, 1 ); Vec_Int_t * vValue = Vec_IntStartFull( 1 << 6 ); printf( "Verifying resub:\n" ); for ( i = 0; i < 64*nWords; i++ ) { int v, Mint = 0, Value = Abc_TtGetBit(pOn, i); if ( !Abc_TtGetBit(pOff, i) && !Value ) continue; for ( v = 0; v < nVars; v++ ) if ( Abc_TtGetBit((word *)Vec_PtrEntry(vDivs, pVarSet[v]), i) ) Mint |= 1 << v; if ( Vec_IntEntry(vValue, Mint) == -1 ) Vec_IntWriteEntry(vValue, Mint, Value); else if ( Vec_IntEntry(vValue, Mint) != Value ) printf( "Mismatch in pattern %d\n", i ); } printf( "Finished verifying resub.\n" ); Vec_IntFree( vValue ); } Vec_Ptr_t * Gia_ManDeriveDivs( Vec_Wrd_t * vSims, int nWords ) { int i, nDivs = Vec_WrdSize(vSims)/nWords; Vec_Ptr_t * vDivs = Vec_PtrAlloc( nDivs ); for ( i = 0; i < nDivs; i++ ) Vec_PtrPush( vDivs, Vec_WrdEntryP(vSims, nWords*i) ); return vDivs; } Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int iChoice, int fUseXor, int fVerbose, int fVeryVerbose ) { return NULL; } Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int iChoice, int fUseXor, int fVerbose, int fVeryVerbose ) { int nWords = 0; Gia_Man_t * pMan = NULL; Vec_Wrd_t * vSims = Vec_WrdReadHex( pFileName, &nWords, 1 ); Vec_Ptr_t * vDivs = vSims ? Gia_ManDeriveDivs( vSims, nWords ) : NULL; Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); //Gia_ManCheckResub( vDivs, nWords ); if ( Vec_PtrSize(vDivs) >= (1<<14) ) { printf( "Reducing all divs from %d to %d.\n", Vec_PtrSize(vDivs), (1<<14)-1 ); Vec_PtrShrink( vDivs, (1<<14)-1 ); } assert( Vec_PtrSize(vDivs) < (1<<14) ); Gia_ManResubPerform( p, vDivs, nWords, 100, 50, iChoice, fUseXor, 1, 1, 0 ); if ( Vec_IntSize(p->vGates) ) { Vec_Wec_t * vGates = Vec_WecStart(1); Vec_IntAppend( Vec_WecEntry(vGates, 0), p->vGates ); pMan = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) ); Vec_WecFree( vGates ); } else printf( "Decomposition did not succeed.\n" ); Gia_ResbFree( p ); Vec_PtrFree( vDivs ); Vec_WrdFree( vSims ); return pMan; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManUnivTfo_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes, Vec_Int_t * vPos ) { int i, iFan, Count = 1; if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) return 0; Gia_ObjSetTravIdCurrentId(p, iObj); if ( vNodes && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) Vec_IntPush( vNodes, iObj ); if ( vPos && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) Vec_IntPush( vPos, iObj ); Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) Count += Gia_ManUnivTfo_rec( p, iFan, vNodes, vPos ); return Count; } int Gia_ManUnivTfo( Gia_Man_t * p, int * pObjs, int nObjs, Vec_Int_t ** pvNodes, Vec_Int_t ** pvPos ) { int i, Count = 0; if ( pvNodes ) { if ( *pvNodes ) Vec_IntClear( *pvNodes ); else *pvNodes = Vec_IntAlloc( 100 ); } if ( pvPos ) { if ( *pvPos ) Vec_IntClear( *pvPos ); else *pvPos = Vec_IntAlloc( 100 ); } Gia_ManIncrementTravId( p ); for ( i = 0; i < nObjs; i++ ) Count += Gia_ManUnivTfo_rec( p, pObjs[i], pvNodes ? *pvNodes : NULL, pvPos ? *pvPos : NULL ); if ( pvNodes ) Vec_IntSort( *pvNodes, 0 ); if ( pvPos ) Vec_IntSort( *pvPos, 0 ); return Count; } /**Function************************************************************* Synopsis [Tuning resub.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManTryResub( Gia_Man_t * p ) { int nLimit = 20; int nDivsMax = 200; int iChoice = 0; int fUseXor = 1; int fDebug = 1; int fVerbose = 0; abctime clk, clkResub = 0, clkStart = Abc_Clock(); Vec_Ptr_t * vvSims = Vec_PtrAlloc( 100 ); Vec_Wrd_t * vSims; word * pSets[2], * pFunc; Gia_Obj_t * pObj, * pObj2; int i, i2, nWords, nNonDec = 0, nTotal = 0; assert( Gia_ManCiNum(p) < 16 ); Vec_WrdFreeP( &p->vSimsPi ); p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); //Vec_WrdPrintHex( p->vSimsPi, nWords ); pSets[0] = ABC_CALLOC( word, nWords ); pSets[1] = ABC_CALLOC( word, nWords ); vSims = Gia_ManSimPatSim( p ); Gia_ManLevelNum(p); Gia_ManCreateRefs(p); Abc_ResubPrepareManager( nWords ); Gia_ManStaticFanoutStart( p ); Gia_ManForEachAnd( p, pObj, i ) { Vec_Int_t vGates; int * pArray, nArray, nTfo, iObj = Gia_ObjId(p, pObj); int Level = Gia_ObjLevel(p, pObj); int nMffc = Gia_NodeMffcSizeMark(p, pObj); pFunc = Vec_WrdEntryP( vSims, nWords*iObj ); Abc_TtCopy( pSets[0], pFunc, nWords, 1 ); Abc_TtCopy( pSets[1], pFunc, nWords, 0 ); Vec_PtrClear( vvSims ); Vec_PtrPushTwo( vvSims, pSets[0], pSets[1] ); nTfo = Gia_ManUnivTfo( p, &iObj, 1, NULL, NULL ); Gia_ManForEachCi( p, pObj2, i2 ) Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); Gia_ManForEachAnd( p, pObj2, i2 ) if ( !Gia_ObjIsTravIdCurrent(p, pObj2) && !Gia_ObjIsTravIdPrevious(p, pObj2) && Gia_ObjLevel(p, pObj2) <= Level ) Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); if ( fVerbose ) printf( "%3d : Lev = %2d Mffc = %2d Divs = %3d Tfo = %3d\n", iObj, Level, nMffc, Vec_PtrSize(vvSims)-2, nTfo ); clk = Abc_Clock(); nArray = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vvSims), Vec_PtrSize(vvSims), nWords, Abc_MinInt(nMffc-1, nLimit), nDivsMax, iChoice, fUseXor, fDebug, fVerbose, &pArray ); clkResub += Abc_Clock() - clk; vGates.nSize = vGates.nCap = nArray; vGates.pArray = pArray; assert( nMffc > Vec_IntSize(&vGates)/2 ); if ( Vec_IntSize(&vGates) > 0 ) nTotal += nMffc - Vec_IntSize(&vGates)/2; nNonDec += Vec_IntSize(&vGates) == 0; } printf( "Total nodes = %5d. Non-realizable = %5d. Gain = %6d. ", Gia_ManAndNum(p), nNonDec, nTotal ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); Abc_PrintTime( 1, "Pure resub time", clkResub ); Abc_ResubPrepareManager( 0 ); Gia_ManStaticFanoutStop( p ); Vec_PtrFree( vvSims ); Vec_WrdFree( vSims ); ABC_FREE( pSets[0] ); ABC_FREE( pSets[1] ); } /**Function************************************************************* Synopsis [Deriving a subset.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManDeriveShrink( Vec_Wrd_t * vFuncs, int nWords ) { int i, k = 0, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2; assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) ); for ( i = 0; i < nFuncs; i++ ) { word * pFunc0 = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords); word * pFunc1 = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords); if ( Abc_TtIsConst0(pFunc0, nWords) || Abc_TtIsConst0(pFunc1, nWords) ) continue; if ( k < i ) Abc_TtCopy( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), pFunc0, nWords, 0 ); if ( k < i ) Abc_TtCopy( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), pFunc1, nWords, 0 ); k++; } Vec_WrdShrink( vFuncs, 2*k*nWords ); return k; } void Gia_ManDeriveCounts( Vec_Wrd_t * vFuncs, int nWords, Vec_Int_t * vCounts ) { int i, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2; assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) ); Vec_IntClear( vCounts ); for ( i = 0; i < 2*nFuncs; i++ ) Vec_IntPush( vCounts, Abc_TtCountOnesVec(Vec_WrdEntryP(vFuncs, i*nWords), nWords) ); } int Gia_ManDeriveCost( Vec_Wrd_t * vFuncs, int nWords, word * pMask, Vec_Int_t * vCounts ) { int i, Res = 0, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2; assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) ); assert( Vec_IntSize(vCounts) * nWords == Vec_WrdSize(vFuncs) ); for ( i = 0; i < nFuncs; i++ ) { int Total[2] = { Vec_IntEntry(vCounts, 2*i+0), Vec_IntEntry(vCounts, 2*i+1) }; int This[2] = { Abc_TtCountOnesVecMask(Vec_WrdEntryP(vFuncs, (2*i+0)*nWords), pMask, nWords, 0), Abc_TtCountOnesVecMask(Vec_WrdEntryP(vFuncs, (2*i+1)*nWords), pMask, nWords, 0) }; assert( Total[0] >= This[0] && Total[1] >= This[1] ); Res += This[0] * This[1] + (Total[0] - This[0]) * (Total[1] - This[1]); } return Res; } int Gia_ManDeriveSimpleCost( Vec_Int_t * vCounts ) { int i, Ent1, Ent2, Res = 0; Vec_IntForEachEntryDouble( vCounts, Ent1, Ent2, i ) Res += Ent1*Ent2; return Res; } void Gia_ManDeriveNext( Vec_Wrd_t * vFuncs, int nWords, word * pMask ) { int i, iStop = Vec_WrdSize(vFuncs); word Data; int nFuncs = Vec_WrdSize(vFuncs) / nWords / 2; assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) ); Vec_WrdForEachEntryStop( vFuncs, Data, i, iStop ) Vec_WrdPush( vFuncs, Data ); for ( i = 0; i < nFuncs; i++ ) { word * pFunc0n = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords); word * pFunc1n = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords); word * pFunc0p = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords + iStop); word * pFunc1p = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords + iStop); Abc_TtAnd( pFunc0p, pFunc0n, pMask, nWords, 0 ); Abc_TtAnd( pFunc1p, pFunc1n, pMask, nWords, 0 ); Abc_TtSharp( pFunc0n, pFunc0n, pMask, nWords ); Abc_TtSharp( pFunc1n, pFunc1n, pMask, nWords ); } } Vec_Int_t * Gia_ManDeriveSubset( Gia_Man_t * p, Vec_Wrd_t * vFuncs, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, int nWords, int fVerbose ) { int i, k, iObj, CostBestPrev, nFuncs = Vec_WrdSize(vFuncs) / nWords; Vec_Int_t * vRes = Vec_IntAlloc( 100 ); Vec_Int_t * vCounts = Vec_IntAlloc( nFuncs * 2 ); Vec_Wrd_t * vFSims = Vec_WrdDup( vFuncs ); assert( nFuncs * nWords == Vec_WrdSize(vFuncs) ); assert( Gia_ManObjNum(p) * nWords == Vec_WrdSize(vSims) ); assert( Vec_IntSize(vObjs) <= Gia_ManCandNum(p) ); nFuncs = Gia_ManDeriveShrink( vFSims, nWords ); Gia_ManDeriveCounts( vFSims, nWords, vCounts ); assert( Vec_IntSize(vCounts) * nWords == Vec_WrdSize(vFSims) ); CostBestPrev = Gia_ManDeriveSimpleCost( vCounts ); if ( fVerbose ) printf( "Processing %d functions and %d objects with cost %d\n", nFuncs, Vec_IntSize(vObjs), CostBestPrev ); for ( i = 0; nFuncs > 0; i++ ) { int iObjBest = -1, CountThis, Count0 = ABC_INFINITY, CountBest = ABC_INFINITY; Vec_IntForEachEntry( vObjs, iObj, k ) { if ( Vec_IntFind(vRes, iObj) >= 0 ) continue; CountThis = Gia_ManDeriveCost( vFSims, nWords, Vec_WrdEntryP(vSims, iObj*nWords), vCounts ); if ( CountBest > CountThis ) { CountBest = CountThis; iObjBest = iObj; } if ( !k ) Count0 = CountThis; } if ( Count0 < CostBestPrev ) { CountBest = Count0; iObjBest = Vec_IntEntry(vObjs, 0); } Gia_ManDeriveNext( vFSims, nWords, Vec_WrdEntryP(vSims, iObjBest*nWords) ); nFuncs = Gia_ManDeriveShrink( vFSims, nWords ); Gia_ManDeriveCounts( vFSims, nWords, vCounts ); assert( CountBest == Gia_ManDeriveSimpleCost(vCounts) ); Vec_IntPush( vRes, iObjBest ); CostBestPrev = CountBest; if ( fVerbose ) printf( "Iter %2d : Funcs = %6d. Object %6d. Cost %6d.\n", i, nFuncs, iObjBest, CountBest ); } Vec_IntFree( vCounts ); Vec_WrdFree( vFSims ); return vRes; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END