From 211ac730c60d1827882c3fa3bf2fe648e3d6380d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Sep 2013 18:19:36 -0700 Subject: Improvements to the new technology mapper. --- src/aig/gia/giaJf.c | 114 ++++++++++++++++++++++++++++++++++++++++-- src/misc/extra/extra.h | 7 ++- src/misc/extra/extraUtilDsd.c | 16 +++++- 3 files changed, 128 insertions(+), 9 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 53d6bfad..60a5e1ad 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -21,6 +21,7 @@ #include "gia.h" #include "misc/vec/vecSet.h" #include "misc/extra/extra.h" +#include "bool/kit/kit.h" ABC_NAMESPACE_IMPL_START @@ -74,6 +75,8 @@ static inline int Jf_ObjLit( int i, int c ) { return Abc_Var2Lit( static inline int Jf_CutSize( int * pCut ) { return pCut[0] & 0x1F; } static inline int Jf_CutFunc( int * pCut ) { return (pCut[0] >> 5) & 0x7FF; } +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_CutCost( int * pCut ) { return (pCut[0] >> 16) & 0xFFFF; } static inline int * Jf_CutLits( int * pCut ) { return pCut + 1; } static inline int Jf_CutLit( int * pCut, int i ) { assert(i);return pCut[i]; } @@ -81,8 +84,11 @@ static inline int Jf_CutLit( int * pCut, int i ) { assert(i);return pCu static inline int Jf_CutVar( int * pCut, int i ) { assert(i);return Abc_Lit2Var(pCut[i]); } #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++ ) #define Jf_CutForEachVar( pCut, Var, i ) for ( i = 1; i <= Jf_CutSize(pCut) && (Var = Jf_CutVar(pCut, i)); i++ ) +extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -161,7 +167,7 @@ void Jf_ManProfileClasses( Jf_Man_t * p ) Gia_ManForEachAnd( p->pGia, pObj, i ) if ( !Gia_ObjIsBuf(pObj) && Gia_ObjRefNumId(p->pGia, i) ) { - iFunc = Abc_Lit2Var( Jf_CutFunc( Jf_ObjCutBest(p, i) ) ); + iFunc = Jf_CutFuncClass( Jf_ObjCutBest(p, i) ); assert( iFunc < 595 ); Counts[iFunc]++; Total++; @@ -924,7 +930,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj ) assert( pSto[c]->pCut[0] <= nOldSupp ); if ( pSto[c]->pCut[0] < nOldSupp ) pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut ); - //pSto[c]->Cost = Sdm_ManReadCnfSize( p->pDsd, Abc_Lit2Var(pSto[c]->iFunc) ); + //pSto[c]->Cost = Sdm_ManReadDsdClauseNum( p->pDsd, Abc_Lit2Var(pSto[c]->iFunc) ); } else { @@ -1124,17 +1130,111 @@ void Jf_ManPropagateEla( Jf_Man_t * p, int fEdge ) CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i), fEdge, ABC_INFINITY ); 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 +// assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i)); p->pPars->Area++; } p->pPars->Delay = Jf_ManComputeDelay( p, 1 ); } + +/**Function************************************************************* + + Synopsis [Derives the result of mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vCopies = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + Vec_Int_t * vMapping = Vec_IntStart( 2 * Gia_ManObjNum(p->pGia) ); + Vec_Int_t * vMapping2 = Vec_IntStart( 1 ); + Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 ); + Vec_Int_t * vLeaves = Vec_IntAlloc( 16 ); + int i, k, iLit, * pCut; + word uTruth; + assert( p->pPars->fCutMin ); + // create new manager + pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) ); + pNew->pName = Abc_UtilStrsav( p->pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec ); + // map primary inputs + Gia_ManForEachCi( p->pGia, pObj, i ) + Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) ); + // iterate through nodes used in the mapping + Gia_ManForEachAnd( p->pGia, pObj, i ) + { + if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 ) + continue; + pCut = Jf_ObjCutBest( p, i ); + assert( Jf_CutSize(pCut) <= 6 ); + if ( Jf_CutSize(pCut) == 0 ) + { + assert( Jf_CutFuncClass(pCut) == 0 ); + Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) ); + continue; + } + if ( Jf_CutSize(pCut) == 1 ) + { + assert( Jf_CutFuncClass(pCut) == 1 ); + iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), Jf_CutLit(pCut, 1) ); + Vec_IntWriteEntry( vCopies, i, iLit ); + continue; + } + // collect leaves + Vec_IntClear( vLeaves ); + Jf_CutForEachLit( pCut, iLit, k ) + Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) ); + // create GIA + uTruth = Sdm_ManReadDsdTruth( p->pDsd, Jf_CutFuncClass(pCut) ); + iLit = Kit_TruthToGia( pNew, (unsigned *)&uTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 ); + iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) ); + Vec_IntWriteEntry( vCopies, i, iLit ); + // create mapping + Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) ); + Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) ); + Vec_IntForEachEntry( vLeaves, iLit, k ) + Vec_IntPush( vMapping2, Abc_Lit2Var(iLit) ); + Vec_IntPush( vMapping2, Abc_Lit2Var(Vec_IntEntry(vCopies, i)) ); + } + Gia_ManForEachCo( p->pGia, pObj, i ) + { + iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) ); + Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) ); + } + Vec_IntFree( vCopies ); + Vec_IntFree( vCover ); + Vec_IntFree( vLeaves ); + // finish mapping + if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) ) + Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) ); + else + Vec_IntFillExtra( vMapping, Gia_ManObjNum(pNew), 0 ); + assert( Vec_IntSize(vMapping) == Gia_ManObjNum(pNew) ); + Vec_IntForEachEntry( vMapping, iLit, i ) + if ( iLit > 0 ) + Vec_IntAddToEntry( vMapping, i, Gia_ManObjNum(pNew) ); + Vec_IntAppend( vMapping, vMapping2 ); + Vec_IntFree( vMapping2 ); + // attach mapping and packing + assert( pNew->vMapping == NULL ); + pNew->vMapping = vMapping; +// Gia_ManMappingVerify( p->pGia ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) ); + return pNew; +} void Jf_ManDeriveMapping( Jf_Man_t * p ) { Vec_Int_t * vMapping; 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 ); Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 ); Gia_ManForEachAnd( p->pGia, pObj, i ) @@ -1193,6 +1293,7 @@ void Jf_ManPrintStats( Jf_Man_t * p, char * pTitle ) } Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) { + Gia_Man_t * pNew = pGia; Jf_Man_t * p; int i; p = Jf_ManAlloc( pGia, pPars ); p->pCutCmp = pPars->fAreaOnly ? Jf_CutCompareArea : Jf_CutCompareDelay; @@ -1204,9 +1305,12 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " ); Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " ); } - Jf_ManDeriveMapping( p ); + if ( p->pPars->fCutMin ) + pNew = Jf_ManDeriveMappingGia(p); + else + Jf_ManDeriveMapping(p); Jf_ManFree( p ); - return pGia; + return pNew; } //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 4b1d38f0..f4dcd154 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -220,9 +220,12 @@ extern int Sdm_ManCanRead(); extern Sdm_Man_t * Sdm_ManRead(); extern void Sdm_ManQuit(); extern int Sdm_ManComputeFunc( Sdm_Man_t * p, int iDsdLit0, int iDsdLit1, int * pCut, int uMask, int fXor ); -extern int Sdm_ManReadCnfSize( Sdm_Man_t * p, int iDsd ); -extern char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd ); extern void Sdm_ManPrintDsdStats( Sdm_Man_t * p, int fVerbose ); +extern int Sdm_ManReadDsdVarNum( Sdm_Man_t * p, int iDsd ); +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 ); /*=== extraUtilProgress.c ================================================================*/ diff --git a/src/misc/extra/extraUtilDsd.c b/src/misc/extra/extraUtilDsd.c index 9a6d1f14..7b023d8c 100644 --- a/src/misc/extra/extraUtilDsd.c +++ b/src/misc/extra/extraUtilDsd.c @@ -990,7 +990,7 @@ Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" ); /**Function************************************************************* - Synopsis [Returns CNF size for the given DSD class.] + Synopsis [] Description [] @@ -999,10 +999,22 @@ Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" ); SeeAlso [] ***********************************************************************/ -int Sdm_ManReadCnfSize( Sdm_Man_t * p, int iDsd ) +int Sdm_ManReadDsdVarNum( Sdm_Man_t * p, int iDsd ) +{ + return p->pDsd6[iDsd].nVars; +} +int Sdm_ManReadDsdAndNum( Sdm_Man_t * p, int iDsd ) +{ + return p->pDsd6[iDsd].nAnds; +} +int Sdm_ManReadDsdClauseNum( Sdm_Man_t * p, int iDsd ) { return p->pDsd6[iDsd].nClauses; } +word Sdm_ManReadDsdTruth( Sdm_Man_t * p, int iDsd ) +{ + return p->pDsd6[iDsd].uTruth; +} char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd ) { return p->pDsd6[iDsd].pStr; -- cgit v1.2.3