From 24f63cf92cf26378f8f57ba171f541631577726e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 11 Apr 2014 09:53:19 -0700 Subject: Correcting internal check. --- src/aig/gia/giaIf.c | 3 ++- src/map/if/if.h | 2 +- src/map/if/ifDsd.c | 67 ++++++++++++++++++++++++++++++----------------------- 3 files changed, 41 insertions(+), 31 deletions(-) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 7e3462f8..cb470e06 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1201,7 +1201,8 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p } assert( If_DsdManSuppSize(pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest)) == (int)pCutBest->nLeaves ); // find the bound set - uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest), nLutSize, 1, 1, 0 ); +// uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest), nLutSize, 1, 0, 1, 0 ); + uSetOld = pCutBest->uMaskFunc; // remap bound set uSetNew = 0; for ( k = 0; k < If_CutLeaveNum(pCutBest); k++ ) diff --git a/src/map/if/if.h b/src/map/if/if.h index 4b955478..7be9f145 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -540,7 +540,7 @@ extern int If_DsdManVarNum( If_DsdMan_t * p ); extern int If_DsdManLutSize( If_DsdMan_t * p ); extern int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd ); extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); -extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose ); +extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose ); extern int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig ); extern int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm ); /*=== ifLib.c =============================================================*/ diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 6eb59675..317ceac5 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -835,14 +835,8 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut pObj->pFans[i] = pLits[i]; pObj->nSupp += If_DsdVecLitSuppSize(&p->vObjs, pLits[i]); } -/* - if ( Abc_Var2Lit(pObj->Id, 0) == 3274 || Abc_Var2Lit(pObj->Id, 0) == 1806 ) - { - If_DsdManPrintOne( stdout, p, pObj->Id, NULL, 1 ); - } -*/ // check decomposability - if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0, 0) ) + if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0, 0, 0) ) If_DsdVecObjSetMark( &p->vObjs, pObj->Id ); return pObj->Id; } @@ -1513,10 +1507,11 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) pSSizes[i] = If_DsdObjSuppSize(pFanin); } // checks if there is a way to package some fanins -unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR]; + unsigned uRes; assert( pObj->nFans > 2 ); assert( If_DsdObjSuppSize(pObj) > LutSize ); If_DsdManGetSuppSizes( p, pObj, pSSizes ); @@ -1532,8 +1527,11 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | + uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0); + if ( uRes & ~(uRes >> 1) & uMaskNot ) + continue; + return uRes; } if ( pObj->nFans == 3 ) return 0; @@ -1548,9 +1546,12 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | + uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0); + if ( uRes & ~(uRes >> 1) & uMaskNot ) + continue; + return uRes; } if ( pObj->nFans == 4 ) return 0; @@ -1566,17 +1567,21 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | + uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], iFirst + pFirsts[i[3]], 0); + if ( uRes & ~(uRes >> 1) & uMaskNot ) + continue; + return uRes; } return 0; } // checks if there is a way to package some fanins -unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; + unsigned uRes; assert( If_DsdObjFaninNum(pObj) == 3 ); assert( If_DsdObjSuppSize(pObj) > LutSize ); If_DsdManGetSuppSizes( p, pObj, pSSizes ); @@ -1590,7 +1595,9 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0); + uRes = If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0); + if ( (uRes & ~(uRes >> 1) & uMaskNot) == 0 ) + return uRes; } // second input SizeIn = pSSizes[0] + pSSizes[2]; @@ -1600,12 +1607,14 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0); + uRes = If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0); + if ( (uRes & ~(uRes >> 1) & uMaskNot) == 0 ) + return uRes; } return 0; } // checks if there is a way to package some fanins -unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; int truthId = If_DsdObjTruthId(p, pObj); @@ -1641,10 +1650,9 @@ Dau_DecPrintSets( vSets, nFans ); } if ( v == nFans ) { - unsigned uSign; + unsigned uRes = 0; if ( !fDerive ) return ~0; - uSign = 0; If_DsdManComputeFirst( p, pObj, pFirsts ); for ( v = 0; v < nFans; v++ ) { @@ -1652,17 +1660,19 @@ Dau_DecPrintSets( vSets, nFans ); if ( Value == 0 ) {} else if ( Value == 1 ) - uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0); + uRes |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0); else if ( Value == 3 ) - uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1); + uRes |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1); else assert( 0 ); } - return uSign; + if ( uRes & ~(uRes >> 1) & uMaskNot ) + continue; + return uRes; } } return 0; } -unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fVerbose ) { If_DsdObj_t * pObj, * pTemp; int i, Mask, iFirst; @@ -1689,7 +1699,7 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i ) if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) + if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1703,7 +1713,7 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i ) if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) + if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1717,7 +1727,7 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i ) if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) + if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1733,9 +1743,9 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri // If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); return 0; } -unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose ) +unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose ) { - unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose ); + unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, uMaskNot, fVerbose ); if ( uSet == 0 && fHighEffort ) { // abctime clk = Abc_Clock(); @@ -2059,7 +2069,7 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec if ( fAdd && !pObj->fMark ) continue; pObj->fMark = 0; - if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0, 0) ) + if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0, 0, 0) ) continue; if ( fFast ) Value = 0; @@ -2072,8 +2082,7 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec continue; If_DsdVecObjSetMark( &p->vObjs, i ); } - if ( pProgress ) - Extra_ProgressBarStop( pProgress ); + Extra_ProgressBarStop( pProgress ); If_ManSatUnbuild( pSat ); Vec_IntFree( vLits ); if ( fVerbose ) -- cgit v1.2.3