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/aig/gia/giaIf.c | 120 +++++++++++++++++++++++++++++++++++++++++++--------- src/base/abci/abc.c | 32 +++++++++++++- src/map/if/if.h | 3 ++ src/map/if/ifDsd.c | 91 ++++++++++++++++++++++++--------------- src/map/if/ifSat.c | 98 +++++++++++++++++++++++++++++++++++++----- 5 files changed, 278 insertions(+), 66 deletions(-) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 9ab57356..a494ca8f 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -22,6 +22,8 @@ #include "aig/aig/aig.h" #include "map/if/if.h" #include "bool/kit/kit.h" +#include "base/main/main.h" +#include "sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -1169,23 +1171,77 @@ int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, SeeAlso [] ***********************************************************************/ -static inline word Gia_ManTt6Stretch( word t, int nVars ) +int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) { - assert( nVars >= 0 ); - if ( nVars == 0 ) - nVars++, t = (t & 0x1) | ((t & 0x1) << 1); - if ( nVars == 1 ) - nVars++, t = (t & 0x3) | ((t & 0x3) << 2); - if ( nVars == 2 ) - nVars++, t = (t & 0xF) | ((t & 0xF) << 4); - if ( nVars == 3 ) - nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8); - if ( nVars == 4 ) - nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16); - if ( nVars == 5 ) - nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32); - assert( nVars == 6 ); - return t; + word uBound, uFree; + int nLutSize = (int)(pIfMan->pPars->pLutStruct[0] - '0'); + int nVarsF = 0, pVarsF[IF_MAX_FUNC_LUTSIZE]; + int nVarsB = 0, pVarsB[IF_MAX_FUNC_LUTSIZE]; + int nVarsS = 0, pVarsS[IF_MAX_FUNC_LUTSIZE]; + unsigned uSetNew, uSetOld; + int RetValue, RetValue2, k; + if ( Vec_IntSize(vLeaves) <= nLutSize ) + { + RetValue = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 ); + // write packing + if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(RetValue))) ) + { + Vec_IntPush( vPacking, 1 ); + Vec_IntPush( vPacking, Abc_Lit2Var(RetValue) ); + Vec_IntAddToEntry( vPacking, 0, 1 ); + } + return RetValue; + } + // find the bound set + uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, pCutBest->iCutDsd, nLutSize, 1, 0 ); + // remap bound set + uSetNew = 0; + for ( k = 0; k < If_CutLeaveNum(pCutBest); k++ ) + { + int iVar = Abc_Lit2Var((int)pCutBest->pPerm[k]); + int Value = ((uSetOld >> (k << 1)) & 3); + if ( Value == 1 ) + uSetNew |= (1 << (2*iVar)); + else if ( Value == 3 ) + uSetNew |= (3 << (2*iVar)); + else assert( Value == 0 ); + } + RetValue = If_ManSatCheckXY( pSat, nLutSize, If_CutTruthW(pIfMan, pCutBest), pCutBest->nLeaves, uSetNew, &uBound, &uFree, vLits ); + assert( RetValue ); + // collect variables + for ( k = 0; k < If_CutLeaveNum(pCutBest); k++ ) + { + int Value = ((uSetNew >> (k << 1)) & 3); + if ( Value == 0 ) + pVarsF[nVarsF++] = k; + else if ( Value == 1 ) + pVarsB[nVarsB++] = k; + else if ( Value == 3 ) + pVarsS[nVarsS++] = k; + else assert( Value == 0 ); + } + // collect bound set variables + Vec_IntClear( vLits ); + for ( k = 0; k < nVarsS; k++ ) + Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsS[k]) ); + for ( k = 0; k < nVarsB; k++ ) + Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsB[k]) ); + RetValue = Gia_ManFromIfLogicCreateLut( pNew, &uBound, vLits, vCover, vMapping, vMapping2 ); + // collecct free set variables + Vec_IntClear( vLits ); + Vec_IntPush( vLits, RetValue ); + for ( k = 0; k < nVarsS; k++ ) + Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsS[k]) ); + for ( k = 0; k < nVarsF; k++ ) + Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsF[k]) ); + // add packing + RetValue2 = Gia_ManFromIfLogicCreateLut( pNew, &uFree, vLits, vCover, vMapping, vMapping2 ); + // write packing + Vec_IntPush( vPacking, 2 ); + Vec_IntPush( vPacking, Abc_Lit2Var(RetValue) ); + Vec_IntPush( vPacking, Abc_Lit2Var(RetValue2) ); + Vec_IntAddToEntry( vPacking, 0, 1 ); + return RetValue2; } /**Function************************************************************* @@ -1205,8 +1261,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) If_Cut_t * pCutBest; If_Obj_t * pIfObj, * pIfLeaf; Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL; - Vec_Int_t * vLeaves, * vLeaves2, * vCover; -// word Truth = 0, * pTruthTable; + Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; + sat_solver * pSat = NULL; int i, k, Entry; assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth ); // if ( pIfMan->pPars->fEnableCheck07 ) @@ -1222,6 +1278,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) // create new manager pNew = Gia_ManStart( If_ManObjNum(pIfMan) ); // iterate through nodes used in the mapping + vLits = Vec_IntAlloc( 1000 ); vCover = Vec_IntAlloc( 1 << 16 ); vLeaves = Vec_IntAlloc( 16 ); vLeaves2 = Vec_IntAlloc( 16 ); @@ -1241,7 +1298,17 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k ) Vec_IntPush( vLeaves, pIfLeaf->iCopy ); // perform one of the two types of mapping: with and without structures - if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth ) + if ( pIfMan->pPars->fUseDsd ) + { + if ( pSat == NULL ) + pSat = (sat_solver *)If_ManSatBuildXY( (int)(pIfMan->pPars->pLutStruct[0] - '0') ); + if ( pIfMan->pPars->pLutStruct && pIfMan->pPars->fDeriveLuts ) + pIfObj->iCopy = Gia_ManFromIfLogicFindLut( pIfMan, pNew, pCutBest, pSat, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking ); + else + pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 ); + pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); + } + else if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth ) { // perform decomposition of the cut pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, If_CutTruthW(pIfMan, pCutBest), pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 ); @@ -1274,9 +1341,12 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) } else assert( 0 ); } + Vec_IntFree( vLits ); Vec_IntFree( vCover ); Vec_IntFree( vLeaves ); Vec_IntFree( vLeaves2 ); + if ( pSat != NULL ) + sat_solver_delete(pSat); // printf( "Mapping array size: IfMan = %d. Gia = %d. Increase = %.2f\n", // If_ManObjNum(pIfMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / If_ManObjNum(pIfMan) ); // finish mapping @@ -1458,8 +1528,10 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized ) If_Man_t * pIfMan; If_Par_t * pPars = (If_Par_t *)pp; // disable cut minimization when GIA strucure is needed - if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts ) +// if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts ) + if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->pLutStruct ) pPars->fCutMin = 0; + // reconstruct GIA according to the hierarchy manager assert( pPars->pTimesArr == NULL ); assert( pPars->pTimesReq == NULL ); @@ -1488,6 +1560,14 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized ) Gia_ManStop( p ); return NULL; } + // create DSD manager + if ( pPars->fUseDsd ) + { + If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd(); + assert( pPars->nLutSize <= If_DsdManVarNum(p) ); + assert( (pPars->pLutStruct == NULL && If_DsdManLutSize(p) == 0) || (pPars->pLutStruct && pPars->pLutStruct[0] - '0' == If_DsdManLutSize(p)) ); + pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd(); + } // compute switching for the IF objects if ( pPars->fPower ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5361e1b2..0c9e3098 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29244,7 +29244,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgyojikfuztvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgyojikfuztnvh" ) ) != EOF ) { switch ( c ) { @@ -29434,6 +29434,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fRepack ^= 1; break; + case 'n': + pPars->fUseDsd ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -29597,6 +29600,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nLutSize = pPars->nGateSize; } + if ( pPars->fUseDsd ) { pPars->fTruth = 1; @@ -29605,6 +29609,29 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fUsePerm = 1; } + if ( pPars->fUseDsd ) + { + int LutSize = (pPars->pLutStruct && pPars->pLutStruct[2] == 0)? pPars->pLutStruct[0] - '0' : 0; + If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd(); + if ( pPars->pLutStruct && pPars->pLutStruct[2] != 0 ) + { + printf( "DSD only works for LUT structures XY.\n" ); + return 0; + } + if ( p && pPars->nLutSize > If_DsdManVarNum(p) ) + { + printf( "DSD manager has incompatible number of variables.\n" ); + return 0; + } + if ( p && LutSize != If_DsdManLutSize(p) ) + { + printf( "DSD manager has different LUT size.\n" ); + return 0; + } + if ( p == NULL ) + Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) ); + } + // complain if truth tables are requested but the cut size is too large if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE ) { @@ -29636,7 +29663,7 @@ usage: sprintf(LutSize, "library" ); else sprintf(LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztvh]\n" ); + Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztnvh]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -29669,6 +29696,7 @@ usage: Abc_Print( -2, "\t-u : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" ); Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" ); Abc_Print( -2, "\t-t : toggles repacking LUTs into new structures [default = %s]\n", pPars->fRepack? "yes": "no" ); + Abc_Print( -2, "\t-n : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : prints the command usage\n"); return 1; 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