diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaIf.c | 120 |
1 files changed, 100 insertions, 20 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 ) { |