From 5f9ca14a7f3635bda76dbc137811b26a00816bcf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 4 Mar 2014 14:48:36 -0800 Subject: Changes to LUT mappers. --- src/map/if/if.h | 3 ++ src/map/if/ifDsd.c | 91 ++++++++++++++++++++++++++++++++------------------ src/map/if/ifSat.c | 98 ++++++++++++++++++++++++++++++++++++++++++++++++------ 3 files changed, 148 insertions(+), 44 deletions(-) (limited to 'src/map') diff --git a/src/map/if/if.h b/src/map/if/if.h index c8b04ef1..cf26c53c 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -572,6 +572,9 @@ extern void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, int fFirst, char * pLabel ); /*=== ifReduce.c ==========================================================*/ extern void If_ManImproveMapping( If_Man_t * p ); +/*=== ifSat.c ==========================================================*/ +extern void * If_ManSatBuildXY( int nLutSize ); +extern int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ); /*=== ifSeq.c =============================================================*/ extern int If_ManPerformMappingSeq( If_Man_t * p ); /*=== ifTime.c ============================================================*/ diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index af586ce2..63341ad3 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -62,7 +62,8 @@ struct If_DsdMan_t_ Mem_Flex_t * pMem; // memory for nodes Vec_Ptr_t * vObjs; // objects Vec_Int_t * vNexts; // next pointers - Vec_Int_t * vNodes; // temp + Vec_Int_t * vTemp1; // temp + Vec_Int_t * vTemp2; // temp word ** pTtElems; // elementary TTs Vec_Mem_t * vTtMem; // truth table memory and hash table Vec_Ptr_t * vTtDecs; // truth table decompositions @@ -198,7 +199,8 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) p->vNexts = Vec_IntAlloc( 10000 ); If_DsdObjAlloc( p, IF_DSD_CONST0, 0 ); If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1; - p->vNodes = Vec_IntAlloc( 32 ); + p->vTemp1 = Vec_IntAlloc( 32 ); + p->vTemp2 = Vec_IntAlloc( 32 ); p->pTtElems = If_ManDsdTtElems(); p->vTtDecs = Vec_PtrAlloc( 1000 ); p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 ); @@ -227,7 +229,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) Vec_VecFree( (Vec_Vec_t *)p->vTtDecs ); Vec_MemHashFree( p->vTtMem ); Vec_MemFreeP( &p->vTtMem ); - Vec_IntFreeP( &p->vNodes ); + Vec_IntFreeP( &p->vTemp1 ); + Vec_IntFreeP( &p->vTemp2 ); Vec_IntFreeP( &p->vNexts ); Vec_PtrFreeP( &p->vObjs ); Mem_FlexStop( p->pMem, 0 ); @@ -662,20 +665,29 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) SeeAlso [] ***********************************************************************/ -void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) +void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts, int * pnSupp ) { - int i, iFanin; + int i, iFanin, iFirst; If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id ); - if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) + if ( If_DsdObjType(pObj) == IF_DSD_CONST0 ) + return; + if ( If_DsdObjType(pObj) == IF_DSD_VAR ) + { + (*pnSupp)++; return; + } + iFirst = *pnSupp; If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) - If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes ); + If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes, vFirsts, pnSupp ); Vec_IntPush( vNodes, Id ); + Vec_IntPush( vFirsts, iFirst ); } -void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) +void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts ) { + int nSupp = 0; Vec_IntClear( vNodes ); - If_DsdManCollect_rec( p, Id, vNodes ); + Vec_IntClear( vFirsts ); + If_DsdManCollect_rec( p, Id, vNodes, vFirsts, &nSupp ); } /**Function************************************************************* @@ -1129,7 +1141,7 @@ 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, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, 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]; @@ -1148,7 +1160,8 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0); + return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | + If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0); } if ( pObj->nFans == 3 ) return 0; @@ -1163,7 +1176,9 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0); + return 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 ( pObj->nFans == 4 ) return 0; @@ -1179,12 +1194,15 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], pFirsts[i[3]], 0); + return 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); } return 0; } // checks if there is a way to package some fanins -unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; assert( If_DsdObjFaninNum(pObj) == 3 ); @@ -1194,28 +1212,28 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, i assert( LimitOut < LutSize ); // first input SizeIn = pSSizes[0] + pSSizes[1]; - SizeOut = pSSizes[2]; + SizeOut = pSSizes[0] + pSSizes[2] + 1; if ( SizeIn <= LutSize && SizeOut <= LimitOut ) { if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 1, pFirsts[1], 0); + return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0); } // second input SizeIn = pSSizes[0] + pSSizes[2]; - SizeOut = pSSizes[1]; + SizeOut = pSSizes[0] + pSSizes[1] + 1; if ( SizeIn <= LutSize && SizeOut <= LimitOut ) { if ( !fDerive ) return ~0; If_DsdManComputeFirst( p, pObj, pFirsts ); - return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 2, pFirsts[2], 0); + return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0); } return 0; } // checks if there is a way to package some fanins -unsigned If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) +unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, 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 ); @@ -1245,7 +1263,7 @@ Dau_DecPrintSets( vSets, nFans ); SizeIn += pSSizes[v]; SizeOut += pSSizes[v]; } - else assert( Value == 0 ); + else assert( 0 ); if ( SizeIn > LutSize || SizeOut > LimitOut ) break; } @@ -1262,10 +1280,10 @@ Dau_DecPrintSets( vSets, nFans ); if ( Value == 0 ) {} else if ( Value == 1 ) - uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 0); + uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0); else if ( Value == 3 ) - uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 1); - else assert( Value == 0 ); + uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1); + else assert( 0 ); } return uSign; } @@ -1274,7 +1292,13 @@ Dau_DecPrintSets( vSets, nFans ); } unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose ) { - If_DsdObj_t * pObj, * pTemp; int i, Mask; + If_DsdObj_t * pObj, * pTemp; + int i, Mask, iFirst; + if ( 193 == iDsd ) + { + int s = 0; + If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); + } pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) ); if ( fVerbose ) If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 ); @@ -1284,20 +1308,21 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, printf( " Trivial\n" ); return ~0; } - If_DsdManCollect( p, pObj->Id, p->vNodes ); - If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + If_DsdManCollect( p, pObj->Id, p->vTemp1, p->vTemp2 ); + If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i ) if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 ) { if ( fVerbose ) printf( " Dec using node " ); if ( fVerbose ) If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 ); - return ~0; + iFirst = Vec_IntEntry(p->vTemp2, i); + return If_DsdSign_rec(p, pTemp, &iFirst); } - If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + 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, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) + if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1308,10 +1333,10 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, return Mask; } } - If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i ) if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) + if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1322,10 +1347,10 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, return Mask; } } - If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i ) if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) + if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 3fec34e0..cfce7369 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -sat_solver * If_ManSatBuildXY( int nLutSize ) +void * If_ManSatBuildXY( int nLutSize ) { int nMintsL = (1 << nLutSize); int nMintsF = (1 << (2 * nLutSize - 1)); @@ -57,6 +57,54 @@ sat_solver * If_ManSatBuildXY( int nLutSize ) return p; } +/**Function************************************************************* + + Synopsis [Verification for 6-input function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static word If_ManSat6ComposeLut4( int t, word f[4], int k ) +{ + int m, v, nMints = (1 << k); + word c, r = 0; + assert( k <= 4 ); + for ( m = 0; m < nMints; m++ ) + { + if ( !((t >> m) & 1) ) + continue; + c = ~(word)0; + for ( v = 0; v < k; v++ ) + c &= ((m >> v) & 1) ? f[v] : ~f[v]; + r |= c; + } + return r; +} +word If_ManSat6Truth( word uBound, word uFree, int * pBSet, int nBSet, int * pSSet, int nSSet, int * pFSet, int nFSet ) +{ + word r, q, f[4]; + int i, k = 0; + // bound set vars + for ( i = 0; i < nSSet; i++ ) + f[k++] = s_Truths6[pSSet[i]]; + for ( i = 0; i < nBSet; i++ ) + f[k++] = s_Truths6[pBSet[i]]; + q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k ); + // free set vars + k = 0; + f[k++] = q; + for ( i = 0; i < nSSet; i++ ) + f[k++] = s_Truths6[pSSet[i]]; + for ( i = 0; i < nFSet; i++ ) + f[k++] = s_Truths6[pFSet[i]]; + r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k ); + return r; +} + /**Function************************************************************* Synopsis [Returns config string for the given truth table.] @@ -68,14 +116,16 @@ sat_solver * If_ManSatBuildXY( int nLutSize ) SeeAlso [] ***********************************************************************/ -int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ) +int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ) { - int iBSet, nBSet = 0; - int iSSet, nSSet = 0; - int iFSet, nFSet = 0; + sat_solver * p = (sat_solver *)pSat; + int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE]; + int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE]; + int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE]; int nMintsL = (1 << nLutSize); int nMintsF = (1 << (2 * nLutSize - 1)); int v, Value, m, mNew, nMintsFNew, nMintsLNew; + word Res; // collect variable sets Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet ); assert( nBSet + nSSet + nFSet == nVars ); @@ -94,13 +144,13 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un if ( Value == 0 ) // FS { if ( ((m >> v) & 1) ) - mNew |= 1 << (nLutSize + nSSet + iFSet); + mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v; iFSet++; } else if ( Value == 1 ) // BS { if ( ((m >> v) & 1) ) - mNew |= 1 << (nSSet + iBSet); + mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v; iBSet++; } else if ( Value == 3 ) // SS @@ -109,6 +159,7 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un { mNew |= 1 << iSSet; mNew |= 1 << (nLutSize + iSSet); + pSSet[iSSet] = v; } iSSet++; } @@ -143,11 +194,36 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un // collect configs assert( nSSet + nFSet + 1 <= nLutSize ); *pTFree = 0; - nMintsLNew = (1 << (nSSet + nFSet + 1)); + nMintsLNew = (1 << (1 + nSSet + nFSet)); for ( m = 0; m < nMintsLNew; m++ ) if ( sat_solver_var_value(p, nMintsL+m) ) Abc_TtSetBit( pTFree, m ); - *pTFree = Abc_Tt6Stretch( *pTFree, nSSet + nFSet + 1 ); + *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet ); + if ( nVars != 6 ) + return 1; + // verify the result + Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet ); + if ( pTruth[0] != Res ) + { + Dau_DsdPrintFromTruth( pTruth, nVars ); + Dau_DsdPrintFromTruth( &Res, nVars ); + Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet ); + Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 ); + printf( "Verification failed!\n" ); + } +/* + else + { +// Kit_DsdPrintFromTruth( (unsigned*)pTBound, nSSet+nBSet ); printf( "\n" ); +// Kit_DsdPrintFromTruth( (unsigned*)pTFree, nSSet+nFSet+1 ); printf( "\n" ); + + Dau_DsdPrintFromTruth( pTruth, nVars ); + Dau_DsdPrintFromTruth( &Res, nVars ); + Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet ); + Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 ); + printf( "Verification OK!\n" ); + } +*/ return 1; } @@ -166,7 +242,7 @@ void If_ManSatTest2() { int nVars = 6; int nLutSize = 4; - sat_solver * p = If_ManSatBuildXY( nLutSize ); + sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize ); // char * pDsd = "(abcdefg)"; // char * pDsd = "([a!bc]d!e)"; char * pDsd = "0123456789ABCDEF{abcdef}"; @@ -194,7 +270,7 @@ void If_ManSatTest() { int nVars = 4; int nLutSize = 3; - sat_solver * p = If_ManSatBuildXY( nLutSize ); + sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize ); word t = 0x183C, * pTruth = &t; word uBound, uFree; unsigned uSet; -- cgit v1.2.3