diff options
| -rw-r--r-- | src/aig/gia/gia.h | 9 | ||||
| -rw-r--r-- | src/aig/gia/giaJf.c | 182 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 16 | ||||
| -rw-r--r-- | src/map/if/ifTruth.c | 36 | ||||
| -rw-r--r-- | src/misc/extra/extra.h | 1 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilDsd.c | 48 |
6 files changed, 216 insertions, 76 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 35c6ebb5..1a30a95c 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -242,16 +242,19 @@ struct Jf_Par_t_ int nRounds; int DelayTarget; int fAreaOnly; + int fOptEdge; int fCoarsen; int fCutMin; int fUseTts; + int fGenCnf; int fVerbose; int fVeryVerbose; int nLutSizeMax; int nCutNumMax; - int Delay; - int Area; - int Edge; + word Delay; + word Area; + word Edge; + word Clause; }; static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index eb6278b2..ee135422 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -41,7 +41,8 @@ struct Jf_Cut_t_ float Flow; // flow int Time; // arrival time int iFunc; // function - int pCut[JF_LEAF_MAX+1]; // cut + int Cost; // cut cost + int pCut[JF_LEAF_MAX+2]; // cut }; typedef struct Jf_Man_t_ Jf_Man_t; @@ -50,6 +51,7 @@ struct Jf_Man_t_ Gia_Man_t * pGia; // user's manager Jf_Par_t * pPars; // users parameter Sdm_Man_t * pDsd; // extern DSD manager + Vec_Int_t * vCnfs; // costs of elementary CNFs Vec_Mem_t * vTtMem; // truth table memory and hash table Vec_Int_t vCuts; // cuts for each node Vec_Int_t vArr; // arrival time @@ -78,8 +80,14 @@ static inline float Jf_ObjRefs( Jf_Man_t * p, int i ) { return Vec_FltEntr //static inline int Jf_ObjLit( int i, int c ) { return i; } static inline int Jf_ObjLit( int i, int c ) { return Abc_Var2Lit( i, c ); } -static inline int Jf_CutSize( int * pCut ) { return pCut[0] & 0x1F; } -static inline int Jf_CutFunc( int * pCut ) { return (pCut[0] >> 5); } +static inline int Jf_CutSize( int * pCut ) { return pCut[0] & 0xF; } // 4 bits +static inline int Jf_CutCost( int * pCut ) { return (pCut[0] >> 4) & 0x3F; } // 6 bits +static inline int Jf_CutFunc( int * pCut ) { return (pCut[0] >> 10); } // 22 bits +static inline int Jf_CutSetAll( int f, int c, int s ) { return (f << 10) | (c << 4) | s; } +static inline void Jf_CutSetSize( int * pCut, int s ) { assert(s>=0 && s<16); pCut[0] ^= (Jf_CutSize(pCut) ^ s); } +static inline void Jf_CutSetCost( int * pCut, int c ) { assert(c>=0 && c<64); pCut[0] ^=((Jf_CutCost(pCut) ^ c) << 4); } +static inline void Jf_CutSetFunc( int * pCut, int f ) { assert(f>=0); pCut[0] ^=((Jf_CutFunc(pCut) ^ f) << 10); } + static inline int Jf_CutFuncClass( int * pCut ) { return Abc_Lit2Var(Jf_CutFunc(pCut)); } static inline int Jf_CutFuncCompl( int * pCut ) { return Abc_LitIsCompl(Jf_CutFunc(pCut)); } static inline int * Jf_CutLits( int * pCut ) { return pCut + 1; } @@ -87,9 +95,11 @@ static inline int Jf_CutLit( int * pCut, int i ) { assert(i);return p //static inline int Jf_CutVar( int * pCut, int i ) { assert(i); return pCut[i]; } static inline int Jf_CutVar( int * pCut, int i ) { assert(i);return Abc_Lit2Var(pCut[i]); } static inline int Jf_CutIsTriv( int * pCut, int i ) { return Jf_CutSize(pCut) == 1 && Jf_CutVar(pCut, 1) == i; } +static inline int Jf_CutCnfSizeF( Jf_Man_t * p, int f ) { return Vec_IntEntry( p->vCnfs, f ); } +static inline int Jf_CutCnfSize( Jf_Man_t * p, int * c ) { return Jf_CutCnfSizeF( p, Jf_CutFuncClass(c) ); } -static inline int Jf_ObjFunc0( Gia_Obj_t * p, int * q ) { return Abc_LitNotCond(Jf_CutFunc(q), Gia_ObjFaninC0(p)); } -static inline int Jf_ObjFunc1( Gia_Obj_t * p, int * q ) { return Abc_LitNotCond(Jf_CutFunc(q), Gia_ObjFaninC1(p)); } +static inline int Jf_ObjFunc0( Gia_Obj_t * p, int * c ) { return Abc_LitNotCond(Jf_CutFunc(c), Gia_ObjFaninC0(p)); } +static inline int Jf_ObjFunc1( Gia_Obj_t * p, int * c ) { return Abc_LitNotCond(Jf_CutFunc(c), Gia_ObjFaninC1(p)); } #define Jf_ObjForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Jf_CutSize(pCut) + 1 ) #define Jf_CutForEachLit( pCut, Lit, i ) for ( i = 1; i <= Jf_CutSize(pCut) && (Lit = Jf_CutLit(pCut, i)); i++ ) @@ -226,9 +236,7 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars ) p = ABC_CALLOC( Jf_Man_t, 1 ); p->pGia = pGia; p->pPars = pPars; - if ( pPars->fCutMin && !pPars->fUseTts ) - p->pDsd = Sdm_ManRead(); - else if ( pPars->fCutMin && pPars->fUseTts ) + if ( pPars->fCutMin && pPars->fUseTts ) { word uTruth; int Value; p->vTtMem = Vec_MemAlloc( 1, 12 ); // 32 KB/page for 6-var functions @@ -236,6 +244,15 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars ) uTruth = ABC_CONST(0x0000000000000000); Value = Vec_MemHashInsert( p->vTtMem, &uTruth ); assert( Value == 0 ); uTruth = ABC_CONST(0xAAAAAAAAAAAAAAAA); Value = Vec_MemHashInsert( p->vTtMem, &uTruth ); assert( Value == 1 ); } + else if ( pPars->fCutMin && !pPars->fUseTts ) + { + p->pDsd = Sdm_ManRead(); + if ( pPars->fGenCnf ) + { + p->vCnfs = Vec_IntStart( 595 ); + Sdm_ManReadCnfCosts( p->pDsd, Vec_IntArray(p->vCnfs), Vec_IntSize(p->vCnfs) ); + } + } Vec_IntFill( &p->vCuts, Gia_ManObjNum(pGia), 0 ); Vec_IntFill( &p->vArr, Gia_ManObjNum(pGia), 0 ); Vec_IntFill( &p->vDep, Gia_ManObjNum(pGia), 0 ); @@ -268,6 +285,7 @@ void Jf_ManFree( Jf_Man_t * p ) Vec_MemHashFree( p->vTtMem ); Vec_MemFree( p->vTtMem ); } + Vec_IntFreeP( &p->vCnfs ); Vec_SetFree_( &p->pMem ); Vec_IntFreeP( &p->vTemp ); ABC_FREE( p ); @@ -690,55 +708,63 @@ static inline void Jf_ObjSortCuts( Jf_Cut_t ** pSto, int nSize ) SeeAlso [] ***********************************************************************/ -int Jf_CutRef_rec( Jf_Man_t * p, int * pCut, int fEdge, int Limit ) +int Jf_CutRef_rec( Jf_Man_t * p, int * pCut ) { - int i, Var, Count = 0; - if ( Limit == 0 ) // terminal - return 0; + int i, Var, Count = Jf_CutCost(pCut); Jf_CutForEachVar( pCut, Var, i ) - if ( Gia_ObjRefIncId( p->pGia, Var ) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) ) - Count += Jf_CutRef_rec( p, Jf_ObjCutBest(p, Var), fEdge, Limit - 1 ); - return Count + (fEdge ? (1 << 5) + Jf_CutSize(pCut) : 1); -// return Count + (fEdge ? Jf_CutSize(pCut) : 1); + if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) ) + Count += Jf_CutRef_rec( p, Jf_ObjCutBest(p, Var) ); + return Count; } -int Jf_CutDeref_rec( Jf_Man_t * p, int * pCut, int fEdge, int Limit ) +int Jf_CutDeref_rec( Jf_Man_t * p, int * pCut ) { - int i, Var, Count = 0; - if ( Limit == 0 ) // terminal - return 0; + int i, Var, Count = Jf_CutCost(pCut); Jf_CutForEachVar( pCut, Var, i ) - if ( Gia_ObjRefDecId( p->pGia, Var ) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) ) - Count += Jf_CutDeref_rec( p, Jf_ObjCutBest(p, Var), fEdge, Limit - 1 ); - return Count + (fEdge ? (1 << 5) + Jf_CutSize(pCut) : 1); -// return Count + (fEdge ? Jf_CutSize(pCut) : 1); + if ( !Gia_ObjRefDecId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) ) + Count += Jf_CutDeref_rec( p, Jf_ObjCutBest(p, Var) ); + return Count; } -static inline int Jf_CutElaOld( Jf_Man_t * p, int * pCut, int fEdge ) +static inline int Jf_CutAreaOld( Jf_Man_t * p, int * pCut ) { - int Ela1 = Jf_CutRef_rec( p, pCut, fEdge, ABC_INFINITY ); - int Ela2 = Jf_CutDeref_rec( p, pCut, fEdge, ABC_INFINITY ); + int Ela1, Ela2; + assert( p->pPars->fGenCnf || Jf_CutCost(pCut) > 0 ); + Ela1 = Jf_CutRef_rec( p, pCut ); + Ela2 = Jf_CutDeref_rec( p, pCut ); assert( Ela1 == Ela2 ); return Ela1; } -int Jf_CutRef2_rec( Jf_Man_t * p, int * pCut, int fEdge, int Limit ) + +int Jf_CutAreaRef_rec( Jf_Man_t * p, int * pCut, int Limit ) +{ + int i, Var, Count = Jf_CutCost(pCut); + Jf_CutForEachVar( pCut, Var, i ) + { + if ( Gia_ObjRefIncId(p->pGia, Var) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) && Limit > 1 ) + Count += Jf_CutAreaRef_rec( p, Jf_ObjCutBest(p, Var), Limit - 1 ); + Vec_IntPush( p->vTemp, Var ); + } + return Count; +} +int Jf_CutAreaRefEdge_rec( Jf_Man_t * p, int * pCut, int Limit ) { - int i, Var, Count = 0; - if ( Limit == 0 ) // terminal - return 0; + int i, Var, Count = (Jf_CutCost(pCut) << 4) | Jf_CutSize(pCut); Jf_CutForEachVar( pCut, Var, i ) { - if ( Gia_ObjRefIncId( p->pGia, Var ) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) ) - Count += Jf_CutRef2_rec( p, Jf_ObjCutBest(p, Var), fEdge, Limit - 1 ); + if ( Gia_ObjRefIncId(p->pGia, Var) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) && Limit > 1 ) + Count += Jf_CutAreaRefEdge_rec( p, Jf_ObjCutBest(p, Var), Limit - 1 ); Vec_IntPush( p->vTemp, Var ); } - return Count + (fEdge ? (1 << 5) + Jf_CutSize(pCut) : 1); -// return Count + (fEdge ? Jf_CutSize(pCut) : 1); + return Count; } -static inline int Jf_CutEla( Jf_Man_t * p, int * pCut, int fEdge ) +static inline int Jf_CutArea( Jf_Man_t * p, int * pCut, int fEdge ) { - int nRecurLimit = ABC_INFINITY; int Ela, Entry, i; + assert( p->pPars->fGenCnf || Jf_CutCost(pCut) > 0 ); Vec_IntClear( p->vTemp ); - Ela = Jf_CutRef2_rec( p, pCut, fEdge, nRecurLimit ); + if ( fEdge ) + Ela = Jf_CutAreaRefEdge_rec( p, pCut, ABC_INFINITY ); + else + Ela = Jf_CutAreaRef_rec( p, pCut, ABC_INFINITY ); Vec_IntForEachEntry( p->vTemp, Entry, i ) Gia_ObjRefDecId( p->pGia, Entry ); return Ela; @@ -916,7 +942,7 @@ int Jf_TtComputeForCut( Jf_Man_t * p, int iFuncLit0, int iFuncLit1, int * pCut0, static inline void Jf_ObjAssignCut( Jf_Man_t * p, Gia_Obj_t * pObj ) { int iObj = Gia_ObjId(p->pGia, pObj); - int pClause[3] = { 1, (2 << 5) | 1, Jf_ObjLit(iObj, 0) }; // set function + int pClause[3] = { 1, Jf_CutSetAll(2, 0, 1), Jf_ObjLit(iObj, 0) }; // set function assert( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) ); Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend( &p->pMem, pClause, 3 ) ); } @@ -952,7 +978,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge ) int nOldSupp, Config, i, k, c = 0; // prepare cuts for ( i = 0; i <= CutNum+1; i++ ) - pSto[i] = Sto + i, pSto[i]->iFunc = 0; + pSto[i] = Sto + i, pSto[i]->Cost = 0, pSto[i]->iFunc = ~0; // compute signatures pCuts0 = Jf_ObjCuts( p, Gia_ObjFaninId0(pObj, iObj) ); Jf_ObjForEachCut( pCuts0, pCut0, i ) @@ -998,9 +1024,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge ) assert( pSto[c]->pCut[0] <= nOldSupp ); if ( pSto[c]->pCut[0] < nOldSupp ) pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut ); - //pSto[c]->Cost = Sdm_ManReadDsdClauseNum( p->pDsd, Abc_Lit2Var(pSto[c]->iFunc) ); } -// Jf_CutCheck( pSto[c]->pCut ); p->CutCount[2]++; pSto[c]->Time = p->pPars->fAreaOnly ? 0 : Jf_CutArr(p, pSto[c]->pCut); pSto[c]->Flow = Jf_CutFlow(p, pSto[c]->pCut); @@ -1013,7 +1037,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge ) if ( !Jf_ObjIsUnit(pObj) && !Jf_ObjHasCutWithSize(pSto, c, 2) ) { assert( Jf_ObjIsUnit(Gia_ObjFanin0(pObj)) && Jf_ObjIsUnit(Gia_ObjFanin1(pObj)) ); - pSto[c]->iFunc = p->pPars->fCutMin ? 4 : 0; // set function (DSD only!) + if ( p->pPars->fCutMin ) pSto[c]->iFunc = 4; // set function (DSD only!) pSto[c]->pCut[0] = 2; pSto[c]->pCut[1] = Jf_ObjLit(Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj)); pSto[c]->pCut[2] = Jf_ObjLit(Gia_ObjFaninId1(pObj, iObj), Gia_ObjFaninC1(pObj)); @@ -1022,7 +1046,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge ) // add elementary cut if ( Jf_ObjIsUnit(pObj) && !(p->pPars->fCutMin && Jf_ObjHasCutWithSize(pSto, c, 1)) ) { - pSto[c]->iFunc = p->pPars->fCutMin ? 2 : 0; // set function + if ( p->pPars->fCutMin ) pSto[c]->iFunc = 2; // set function pSto[c]->pCut[0] = 1; pSto[c]->pCut[1] = Jf_ObjLit(iObj, 0); c++; @@ -1030,22 +1054,26 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge ) // reorder cuts // Jf_ObjSortCuts( pSto + 1, c - 1 ); // Jf_ObjCheckPtrs( pSto, CutNum ); - p->CutCount[3] += c; + // find cost of the best cut + pSto[0]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[0]->iFunc)) : 1; + assert( pSto[0]->Cost >= 0 ); // save best info assert( pSto[0]->Flow >= 0 ); Vec_IntWriteEntry( &p->vArr, iObj, pSto[0]->Time ); - Vec_FltWriteEntry( &p->vFlow, iObj, (pSto[0]->Flow + (fEdge ? pSto[0]->pCut[0] : 1)) / Jf_ObjRefs(p, iObj) ); + Vec_FltWriteEntry( &p->vFlow, iObj, (pSto[0]->Flow + (fEdge ? pSto[0]->pCut[0] : pSto[0]->Cost)) / Jf_ObjRefs(p, iObj) ); // add cuts to storage cuts Vec_IntClear( p->vTemp ); Vec_IntPush( p->vTemp, c ); for ( i = 0; i < c; i++ ) { assert( pSto[i]->pCut[0] <= 6 ); - Vec_IntPush( p->vTemp, (pSto[i]->iFunc << 5) | pSto[i]->pCut[0] ); + pSto[i]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[i]->iFunc)) : 1; + Vec_IntPush( p->vTemp, Jf_CutSetAll(pSto[i]->iFunc, pSto[i]->Cost, pSto[i]->pCut[0]) ); for ( k = 1; k <= pSto[i]->pCut[0]; k++ ) Vec_IntPush( p->vTemp, pSto[i]->pCut[k] ); } Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend(&p->pMem, Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp)) ); + p->CutCount[3] += c; } void Jf_ManComputeCuts( Jf_Man_t * p, int fEdge ) { @@ -1118,7 +1146,7 @@ int Jf_ManComputeDelay( Jf_Man_t * p, int fEval ) int Jf_ManComputeRefs( Jf_Man_t * p ) { Gia_Obj_t * pObj; - float nRefsNew; int i; + float nRefsNew; int i, * pCut; float * pRefs = Vec_FltArray(&p->vRefs); float * pFlow = Vec_FltArray(&p->vFlow); assert( p->pGia->pRefs != NULL ); @@ -1131,13 +1159,18 @@ int Jf_ManComputeRefs( Jf_Man_t * p ) else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 ) { assert( Jf_ObjIsUnit(pObj) ); - Jf_CutRef( p, Jf_ObjCutBest(p, i) ); - p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i)); + pCut = Jf_ObjCutBest(p, i); + Jf_CutRef( p, pCut ); + if ( p->pPars->fGenCnf ) + p->pPars->Clause += Jf_CutCnfSize(p, pCut); + p->pPars->Edge += Jf_CutSize(pCut); p->pPars->Area++; } // blend references and normalize flow -// nRefsNew = Abc_MaxFloat( 1, 0.25 * pRefs[i] + 0.75 * p->pGia->pRefs[i] ); - nRefsNew = Abc_MaxFloat( 1, 0.9 * pRefs[i] + 0.2 * p->pGia->pRefs[i] ); + if ( p->pPars->fOptEdge ) + nRefsNew = Abc_MaxFloat( 1, 0.8 * pRefs[i] + 0.2 * p->pGia->pRefs[i] ); + else + nRefsNew = Abc_MaxFloat( 1, 0.2 * pRefs[i] + 0.8 * p->pGia->pRefs[i] ); pFlow[i] = pFlow[i] * pRefs[i] / nRefsNew; pRefs[i] = nRefsNew; assert( pFlow[i] >= 0 ); @@ -1167,13 +1200,16 @@ void Jf_ObjComputeBestCut( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge, int fEla ) Jf_ObjForEachCut( pCuts, pCut, i ) { if ( Jf_CutIsTriv(pCut, iObj) ) continue; - Area = fEla ? Jf_CutEla(p, pCut, fEdge) : Jf_CutFlow(p, pCut); + if ( fEdge && !fEla ) + Jf_CutSetCost(pCut, Jf_CutSize(pCut)); + assert( p->pPars->fGenCnf || Jf_CutCost(pCut) > 0 ); + Area = fEla ? Jf_CutArea(p, pCut, fEdge) : Jf_CutFlow(p, pCut) + Jf_CutCost(pCut); if ( pCutBest == NULL || AreaBest > Area || (AreaBest == Area && TimeBest > (Time = Jf_CutArr(p, pCut))) ) pCutBest = pCut, AreaBest = Area, TimeBest = Time; } Vec_IntWriteEntry( &p->vArr, iObj, Jf_CutArr(p, pCutBest) ); if ( !fEla ) - Vec_FltWriteEntry( &p->vFlow, iObj, (AreaBest + (fEdge ? 10 + Jf_CutSize(pCut) : 1)) / Jf_ObjRefs(p, iObj) ); + Vec_FltWriteEntry( &p->vFlow, iObj, AreaBest / Jf_ObjRefs(p, iObj) ); Jf_ObjSetBestCut( pCuts, pCutBest, p->vTemp ); // Jf_CutPrint( Jf_ObjCutBest(p, iObj) ); printf( "\n" ); } @@ -1192,21 +1228,25 @@ void Jf_ManPropagateEla( Jf_Man_t * p, int fEdge ) { Gia_Obj_t * pObj; int i, CostBef, CostAft; - p->pPars->Area = p->pPars->Edge = 0; + p->pPars->Area = p->pPars->Edge = p->pPars->Clause = 0; Gia_ManForEachObjReverse( p->pGia, pObj, i ) if ( Gia_ObjIsBuf(pObj) ) Jf_ObjPropagateBuf( p, pObj, 1 ); else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 ) { assert( Jf_ObjIsUnit(pObj) ); - CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i), fEdge, ABC_INFINITY ); + CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i) ); Jf_ObjComputeBestCut( p, pObj, fEdge, 1 ); - CostAft = Jf_CutRef_rec( p, Jf_ObjCutBest(p, i), fEdge, ABC_INFINITY ); -// assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM + CostAft = Jf_CutRef_rec( p, Jf_ObjCutBest(p, i) ); +// if ( CostBef != CostAft ) printf( "%d -> %d ", CostBef, CostAft ); + assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM + if ( p->pPars->fGenCnf ) + p->pPars->Clause += Jf_CutCnfSize(p, Jf_ObjCutBest(p, i)); p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i)); p->pPars->Area++; } p->pPars->Delay = Jf_ManComputeDelay( p, 1 ); +// printf( "\n" ); } /**Function************************************************************* @@ -1246,13 +1286,10 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 ) continue; pCut = Jf_ObjCutBest( p, i ); - Class = Jf_CutFuncClass( pCut ); - if ( p->pPars->fUseTts ) - uTruth = *Vec_MemReadEntry(p->vTtMem, Class); - else - uTruth = Sdm_ManReadDsdTruth(p->pDsd, Class); // printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut); -// assert( Sdm_ManReadDsdVarNum( p->pDsd, Class ) == Jf_CutSize(pCut) ); + Class = Jf_CutFuncClass( pCut ); + uTruth = p->pPars->fUseTts ? *Vec_MemReadEntry(p->vTtMem, Class) : Sdm_ManReadDsdTruth(p->pDsd, Class); + assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) ); if ( Jf_CutSize(pCut) == 0 ) { assert( Class == 0 ); @@ -1313,7 +1350,7 @@ void Jf_ManDeriveMapping( Jf_Man_t * p ) Gia_Obj_t * pObj; int i, k, * pCut; assert( !p->pPars->fCutMin ); - vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + p->pPars->Edge + p->pPars->Area * 2 ); + vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + (int)p->pPars->Area * 2 ); Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 ); Gia_ManForEachAnd( p->pGia, pObj, i ) { @@ -1351,9 +1388,11 @@ void Jf_ManSetDefaultPars( Jf_Par_t * pPars ) pPars->nRounds = 1; pPars->DelayTarget = -1; pPars->fAreaOnly = 1; + pPars->fOptEdge = 1; pPars->fCoarsen = 0; pPars->fCutMin = 0; pPars->fUseTts = 0; + pPars->fGenCnf = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; pPars->nLutSizeMax = JF_LEAF_MAX; @@ -1367,6 +1406,8 @@ void Jf_ManPrintStats( Jf_Man_t * p, char * pTitle ) printf( "Level =%6d ", p->pPars->Delay ); printf( "Area =%9d ", p->pPars->Area ); printf( "Edge =%9d ", p->pPars->Edge ); + if ( p->pPars->fGenCnf ) + printf( "Cnf =%9d ", p->pPars->Clause ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); fflush( stdout ); } @@ -1374,17 +1415,20 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) { Gia_Man_t * pNew = pGia; Jf_Man_t * p; int i; + assert( !pPars->fCutMin || pPars->nLutSize <= 6 ); + if ( pPars->fGenCnf ) + pPars->fCutMin = 1, pPars->fUseTts = pPars->fOptEdge = 0; if ( pPars->fCutMin && pPars->fUseTts ) pPars->fCoarsen = 0; p = Jf_ManAlloc( pGia, pPars ); p->pCutCmp = pPars->fAreaOnly ? Jf_CutCompareArea : Jf_CutCompareDelay; Jf_ManComputeCuts( p, 0 ); - Jf_ManComputeRefs( p ); Jf_ManPrintStats( p, "Start" ); + Jf_ManComputeRefs( p ); Jf_ManPrintStats( p, "Start" ); for ( i = 0; i < pPars->nRounds; i++ ) { - Jf_ManPropagateFlow( p, 1 ); Jf_ManPrintStats( p, "Flow " ); - Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " ); - Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " ); + Jf_ManPropagateFlow( p, pPars->fOptEdge ); Jf_ManPrintStats( p, "Flow " ); + Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " ); + Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " ); } if ( p->pPars->fCutMin ) pNew = Jf_ManDeriveMappingGia(p); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 475cbb5b..727107a9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29847,7 +29847,7 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Jf_ManSetDefaultPars( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDacmtvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDaekmtcvwh" ) ) != EOF ) { switch ( c ) { @@ -29904,7 +29904,10 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fAreaOnly ^= 1; break; - case 'c': + case 'e': + pPars->fOptEdge ^= 1; + break; + case 'k': pPars->fCoarsen ^= 1; break; case 'm': @@ -29913,6 +29916,9 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fUseTts ^= 1; break; + case 'c': + pPars->fGenCnf ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -29951,16 +29957,18 @@ usage: sprintf(Buffer, "best possible" ); else sprintf(Buffer, "%d", pPars->DelayTarget ); - Abc_Print( -2, "usage: &jf [-KCRD num] [-acmtvwh]\n" ); + Abc_Print( -2, "usage: &jf [-KCRD num] [-akmtcvwh]\n" ); Abc_Print( -2, "\t performs technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum ); Abc_Print( -2, "\t-R num : the number of mapping rounds [default = %d]\n", pPars->nRounds ); Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer ); Abc_Print( -2, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" ); - Abc_Print( -2, "\t-c : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" ); + Abc_Print( -2, "\t-e : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" ); + Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" ); Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" ); Abc_Print( -2, "\t-t : toggles truth tables for minimization [default = %s]\n", pPars->fUseTts? "yes": "no" ); + Abc_Print( -2, "\t-c : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : prints the command usage\n"); diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c index bdbb2e1f..e41acfd6 100644 --- a/src/map/if/ifTruth.c +++ b/src/map/if/ifTruth.c @@ -675,6 +675,42 @@ int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut return 0; } +/**Function************************************************************* + + Synopsis [Truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +int If_CutComputeTruth3( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 ) +{ + int fCompl, truthId; + int iFuncLit0 = pCut0->iDsd; + int iFuncLit1 = pCut1->iDsd; + int nWords = Abc_TtWordNum( pCut->nLimit ); + word * pTruth0s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit0) ); + word * pTruth1s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit1) ); + word * pTruth0 = (word *)p->puTemp[0]; + word * pTruth1 = (word *)p->puTemp[1]; + word * pTruth = (word *)p->puTemp[2]; + Abc_TtCopy( pTruth0, pTruth0s, nWords, fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(iFuncLit0) ); + Abc_TtCopy( pTruth1, pTruth1s, nWords, fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(iFuncLit1) ); + Abc_TtStretch( pTruth0, pCut->nLimit, pCut0->pLeaves, pCut0->nLeaves, pCut->pLeaves, pCut->nLeaves ); + Abc_TtStretch( pTruth1, pCut->nLimit, pCut1->pLeaves, pCut1->nLeaves, pCut->pLeaves, pCut->nLeaves ); + fCompl = (pTruth0[0] & pTruth1[0] & 1); + Abc_TtAnd( pTruth, pTruth0, pTruth1, nWords, fCompl ); + pCut->nLeaves = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves ); + truthId = Vec_MemHashInsert( p->vTtMem, pTruth ); + pCut->iDsd = Abc_Var2Lit( truthId, fCompl ); + assert( (pTruth[0] & 1) == 0 ); + return 1; +} +*/ //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index f4dcd154..982a6f5e 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -226,6 +226,7 @@ extern int Sdm_ManReadDsdAndNum( Sdm_Man_t * p, int iDsd ); extern int Sdm_ManReadDsdClauseNum( Sdm_Man_t * p, int iDsd ); extern word Sdm_ManReadDsdTruth( Sdm_Man_t * p, int iDsd ); extern char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd ); +extern void Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts ); /*=== extraUtilProgress.c ================================================================*/ diff --git a/src/misc/extra/extraUtilDsd.c b/src/misc/extra/extraUtilDsd.c index 1af58940..a349ff9f 100644 --- a/src/misc/extra/extraUtilDsd.c +++ b/src/misc/extra/extraUtilDsd.c @@ -1014,6 +1014,14 @@ char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd ) { return p->pDsd6[iDsd].pStr; } +void Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts ) +{ + int i; + assert( nCosts == DSD_CLASS_NUM ); + pCosts[0] = pCosts[1] = 0; + for ( i = 2; i < DSD_CLASS_NUM; i++ ) + pCosts[i] = Sdm_ManReadDsdClauseNum( p, i ); +} /**Function************************************************************* @@ -1104,6 +1112,46 @@ void Sdm_ManTest() Sdm_ManFree( p ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +void Sdm_ManCompareCnfSizes() +{ + Vec_Int_t * vMemory; + word uTruth; + int i, nSop0, nSop1, nVars, nCla, RetValue; + vMemory = Vec_IntAlloc( 1 << 16 ); + for ( i = 1; i < DSD_CLASS_NUM; i++ ) + { + uTruth = Sdm_ManReadDsdTruth( s_SdmMan, i ); + nVars = Sdm_ManReadDsdVarNum( s_SdmMan, i ); + nCla = Sdm_ManReadDsdClauseNum( s_SdmMan, i ); + + RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 ); + nSop0 = Vec_IntSize(vMemory); + + uTruth = ~uTruth; + RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 ); + nSop1 = Vec_IntSize(vMemory); + + if ( nSop0 + nSop1 != nCla ) + printf( "Class %4d : %d + %d != %d\n", i, nSop0, nSop1, nCla ); + else + printf( "Class %4d : %d + %d == %d\n", i, nSop0, nSop1, nCla ); + } + Vec_IntFree( vMemory ); +} +*/ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |