diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-19 23:42:05 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-19 23:42:05 -0800 |
commit | ffbe3bc5767c597b3ca612a12e671749f23ca34f (patch) | |
tree | 5422b46e65aef95dea810fd82965a7301ba3397b /src | |
parent | d671adbb86b241a71e15bcd67831b267d0de6abf (diff) | |
download | abc-ffbe3bc5767c597b3ca612a12e671749f23ca34f.tar.gz abc-ffbe3bc5767c597b3ca612a12e671749f23ca34f.tar.bz2 abc-ffbe3bc5767c597b3ca612a12e671749f23ca34f.zip |
DSD manager.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 14 | ||||
-rw-r--r-- | src/map/if/if.h | 6 | ||||
-rw-r--r-- | src/map/if/ifCut.c | 3 | ||||
-rw-r--r-- | src/map/if/ifMan.c | 17 | ||||
-rw-r--r-- | src/map/if/ifMap.c | 19 | ||||
-rw-r--r-- | src/misc/util/abc_global.h | 1 | ||||
-rw-r--r-- | src/opt/dau/dau.h | 6 | ||||
-rw-r--r-- | src/opt/dau/dauTree.c | 483 |
8 files changed, 525 insertions, 24 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 89d1c6dd..5fa4d7fd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -14890,6 +14890,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nLutSize = pPars->nGateSize; } + if ( pPars->fUseDsd ) + { + pPars->fTruth = 1; + pPars->fCutMin = 1; + pPars->fUsePerm = 1; + } + if ( pPars->fUserRecLib ) { if ( Abc_NtkRecIsRunning() + Abc_NtkRecIsRunning2() + Abc_NtkRecIsRunning3() != 1 ) @@ -27461,6 +27468,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nLutSize = pPars->nGateSize; } + if ( pPars->fUseDsd ) + { + pPars->fTruth = 1; + pPars->fCutMin = 1; + pPars->fUsePerm = 1; + } + // complain if truth tables are requested but the cut size is too large if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE ) { diff --git a/src/map/if/if.h b/src/map/if/if.h index e8c57998..f1d78ff4 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -35,7 +35,7 @@ #include "misc/mem/mem.h" #include "misc/tim/tim.h" #include "misc/util/utilNam.h" - +#include "opt/dau/dau.h" ABC_NAMESPACE_HEADER_START @@ -189,6 +189,7 @@ struct If_Man_t_ Vec_Int_t * vSwitching; // switching activity of each node Vec_Int_t ** pDriverCuts; // temporary driver cuts int pPerm[3][IF_MAX_LUTSIZE]; // permutations + unsigned uSharedMask; // mask of shared variables int nShared; // the number of shared variables // SOP balancing Vec_Int_t * vCover; // used to compute ISOP @@ -218,8 +219,9 @@ struct If_Man_t_ int nCutsCount[32]; int nCutsCountAll; int nCutsUselessAll; - Abc_Nam_t * pNamDsd; +// Abc_Nam_t * pNamDsd; int iNamVar; + Dss_Man_t * pDsdMan; // timing manager Tim_Man_t * pManTim; diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index 8e89977f..ca985910 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -418,11 +418,13 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC ) p->nShared = nLimit; pC->nLeaves = nLimit; pC->uSign = pC0->uSign | pC1->uSign; + p->uSharedMask = Abc_InfoMask( nLimit ); return 1; } // compare two cuts with different numbers i = k = c = s = 0; + p->uSharedMask = 0; while ( 1 ) { if ( c == nLimit ) return 0; @@ -440,6 +442,7 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC ) } else { + p->uSharedMask |= (1 << c); p->pPerm[0][i] = p->pPerm[1][k] = p->pPerm[2][s++] = c; pC->pLeaves[c++] = pC0->pLeaves[i++]; k++; if ( i == nSizeC0 ) goto FlushCut1; diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 776c5ba6..076f74d6 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -83,8 +83,10 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) p->pCutTemp = (If_Cut_t *)ABC_ALLOC( char, p->nCutBytes ); if ( pPars->fUseDsd ) { - p->pNamDsd = Abc_NamStart( 1000, 20 ); - p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL ); +// p->pNamDsd = Abc_NamStart( 1000, 20 ); +// p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL ); + p->pDsdMan = Dss_ManAlloc( pPars->nLutSize ); + p->iNamVar = 2; } // create the constant node @@ -150,8 +152,9 @@ void If_ManStop( If_Man_t * p ) Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) ); Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) ); } - if ( p->pNamDsd ) + if ( p->pPars->fUseDsd ) { +/* if ( p->pPars->fVerbose ) Abc_Print( 1, "Number of unique entries in the DSD table = %d. Memory = %.1f MB.\n", Abc_NamObjNumMax(p->pNamDsd), 1.0*Abc_NamMemAlloc(p->pNamDsd)/(1<<20) ); @@ -161,6 +164,8 @@ void If_ManStop( If_Man_t * p ) Abc_PrintTime( 1, "Time3", s_TimeComp[3] ); // Abc_NamPrint( p->pNamDsd ); Abc_NamStop( p->pNamDsd ); +*/ + Dss_ManFree( p->pDsdMan ); } // Abc_PrintTime( 1, "Truth", p->timeTruth ); // Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp ); @@ -427,7 +432,11 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId ) pCut->nLeaves = 1; pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId; pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] ); - pCut->iDsd = p->iNamVar; + if ( p->pPars->fUseDsd ) + { + pCut->iDsd = p->iNamVar; + pCut->pPerm[0] = 0; + } // set up elementary truth table of the unit cut if ( p->pPars->fTruth ) { diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 11b9449d..ad50e1cc 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -277,6 +277,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep } if ( p->pPars->fUseDsd ) { + int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) }; + int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves }; + int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] }; +/* char * pName = Dau_DsdMerge( Abc_NamStr(p->pNamDsd, pCut0->iDsd), If_CutPerm0(pCut, pCut0), @@ -284,6 +288,21 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep If_CutPerm1(pCut, pCut1), pObj->fCompl0, pObj->fCompl1, pCut->nLimit ); pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL ); +*/ + // create fanins + for ( j = 0; j < (int)pCut0->nLeaves; j++ ) + pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] ); + for ( j = 0; j < (int)pCut1->nLeaves; j++ ) + pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] ); + // canonicize + if ( iDsd[0] > iDsd[1] ) + { + ABC_SWAP( int, iDsd[0], iDsd[1] ); + ABC_SWAP( int, nFans[0], nFans[1] ); + ABC_SWAP( int *, pFans[0], pFans[1] ); + } + // derive new DSD + pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm ); } // compute the application-specific cost and depth diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 2b4e17a7..7535014b 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -257,6 +257,7 @@ static inline int Abc_LitIsCompl( int Lit ) { return Lit & 1; static inline int Abc_LitNot( int Lit ) { return Lit ^ 1; } static inline int Abc_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } static inline int Abc_LitRegular( int Lit ) { return Lit & ~01; } +static inline int Abc_Lit2Lit( int * pMap, int Lit ) { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } enum Abc_VerbLevel { diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index 782d4e89..7eb0b975 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -87,6 +87,12 @@ extern int Dau_DsdCountAnds( char * pDsd ); extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ); extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars ); +/*=== dauMerge.c ==========================================================*/ +extern Dss_Man_t * Dss_ManAlloc( int nVars ); +extern void Dss_ManFree( Dss_Man_t * p ); +extern int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPerm ); + + ABC_NAMESPACE_HEADER_END diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index 2a817f04..d8bc8473 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -20,6 +20,7 @@ #include "dauInt.h" #include "misc/mem/mem.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -27,6 +28,26 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +typedef struct Dss_Fun_t_ Dss_Fun_t; +struct Dss_Fun_t_ +{ + unsigned iDsd : 27; // DSD literal + unsigned nFans : 5; // fanin count + unsigned char pFans[0]; // fanins +}; + +typedef struct Dss_Ent_t_ Dss_Ent_t; +struct Dss_Ent_t_ +{ + Dss_Fun_t * pFunc; + Dss_Ent_t * pNext; + unsigned iDsd0 : 27; // dsd entry + unsigned nWords : 5; // total word count (struct + shared) + unsigned iDsd1 : 27; // dsd entry + unsigned nShared: 5; // shared count + unsigned char pShared[0]; // shared literals +}; + typedef struct Dss_Obj_t_ Dss_Obj_t; struct Dss_Obj_t_ { @@ -62,6 +83,8 @@ struct Dss_Man_t_ Mem_Flex_t * pMem; // memory for nodes Vec_Ptr_t * vObjs; // objects Vec_Int_t * vLeaves; // temp + Vec_Int_t * vCopies; // temp + word ** pTtElems; // elementary TTs }; static inline Dss_Obj_t * Dss_Regular( Dss_Obj_t * p ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); } @@ -72,6 +95,7 @@ static inline int Dss_IsComplement( Dss_Obj_t * p ) static inline void Dss_ObjClean( Dss_Obj_t * pObj ) { memset( pObj, 0, sizeof(Dss_Obj_t) ); } static inline int Dss_ObjId( Dss_Obj_t * pObj ) { return pObj->Id; } static inline int Dss_ObjType( Dss_Obj_t * pObj ) { return pObj->Type; } +static inline int Dss_ObjSuppSize( Dss_Obj_t * pObj ) { return pObj->nSupp; } static inline int Dss_ObjFaninNum( Dss_Obj_t * pObj ) { return pObj->nFans; } static inline int Dss_ObjFaninC( Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]); } static inline word * Dss_ObjTruth( Dss_Obj_t * pObj ) { return (word *)(pObj->pFans + pObj->nFans + (pObj->nFans & 1)); } @@ -87,12 +111,18 @@ static inline Dss_Obj_t * Dss_ObjChildNtk( Dss_Ntk_t * p, Dss_Obj_t * pObj,int static inline Dss_Obj_t * Dss_ManObj( Dss_Man_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p->vObjs, Id); } static inline Dss_Obj_t * Dss_ManConst0( Dss_Man_t * p ) { return Dss_ManObj( p, 0 ); } static inline Dss_Obj_t * Dss_ManVar( Dss_Man_t * p, int v ) { assert( v >= 0 && v < p->nVars ); return Dss_ManObj( p, v+1 ); } +static inline int Dss_ManLitSuppSize( Dss_Man_t * p, int iLit ) { return Dss_ManObj( p, Abc_Lit2Var(iLit) )->nSupp; } static inline int Dss_Obj2Lit( Dss_Obj_t * pObj ) { return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj)); } static inline Dss_Obj_t * Dss_Lit2Obj( Dss_Man_t * p, int iLit ) { return Dss_NotCond(Dss_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); } static inline Dss_Obj_t * Dss_ObjFanin( Dss_Man_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_ManObj(p, Abc_Lit2Var(pObj->pFans[i])); } static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]); } +static inline int Dss_EntWordNum( Dss_Ent_t * p ) { return sizeof(Dss_Ent_t) / 8 + p->nShared / 4 + ((p->nShared & 3) > 0); } +static inline int Dss_FunWordNum( Dss_Fun_t * p ) { assert(p->nFans >= 2); return (p->nFans + 4) / 8 + (((p->nFans + 4) & 7) > 0); } +static inline word * Dss_FunTruth( Dss_Fun_t * p ) { assert(p->nFans >= 2); return (word *)p + Dss_FunWordNum(p); } + + #define Dss_NtkForEachNode( p, pObj, i ) \ Vec_PtrForEachEntryStart( Dss_Obj_t *, p->vObjs, pObj, i, p->nVars + 1 ) #define Dss_ObjForEachFaninNtk( p, pObj, pFanin, i ) \ @@ -109,6 +139,17 @@ static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i #define Dss_ObjForEachChild( p, pObj, pFanin, i ) \ for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(p, pObj, i)); i++ ) +static inline int Dss_WordCountOnes( unsigned uWord ) +{ + uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); + uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); + uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); + uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); + return (uWord & 0x0000FFFF) + (uWord>>16); +} + +static inline int Dss_Lit2Lit( int * pMapLit, int Lit ) { return Abc_Var2Lit( Abc_Lit2Var(pMapLit[Abc_Lit2Var(Lit)]), Abc_LitIsCompl(Lit) ^ Abc_LitIsCompl(pMapLit[Abc_Lit2Var(Lit)]) ); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -116,6 +157,30 @@ static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i /**Function************************************************************* + Synopsis [Elementary truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline word ** Dss_ManTtElems() +{ + static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL}; + if ( pTtElems[0] == NULL ) + { + int v; + for ( v = 0; v <= DAU_MAX_VAR; v++ ) + pTtElems[v] = TtElems[v]; + Abc_TtElemInit( pTtElems, DAU_MAX_VAR ); + } + return pTtElems; +} + +/**Function************************************************************* + Synopsis [Creating DSD network.] Description [] @@ -387,11 +452,29 @@ void Dss_NtkCheck( Dss_Ntk_t * p ) } } } -void Dss_NtkTransform( Dss_Ntk_t * p ) +int Dss_NtkCollectPerm_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, int * pPermDsd, int * pnPerms ) +{ + Dss_Obj_t * pChild; + int k, fCompl = Dss_IsComplement(pObj); + pObj = Dss_Regular( pObj ); + if ( pObj->Type == DAU_DSD_VAR ) + { + pPermDsd[*pnPerms] = Abc_Var2Lit(pObj->iVar, fCompl); + pObj->iVar = (*pnPerms)++; + return fCompl; + } + Dss_ObjForEachChildNtk( p, pObj, pChild, k ) + if ( Dss_NtkCollectPerm_rec( p, pChild, pPermDsd, pnPerms ) ) + pObj->pFans[k] = (unsigned char)Abc_LitRegular((int)pObj->pFans[k]); + return 0; +} +void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd ) { Dss_Obj_t * pChildren[DAU_MAX_VAR]; Dss_Obj_t * pObj, * pChild; - int i, k; + int i, k, nPerms; + if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 ) + return; Dss_NtkForEachNode( p, pObj, i ) { Dss_ObjForEachChildNtk( p, pObj, pChild, k ) @@ -400,6 +483,10 @@ void Dss_NtkTransform( Dss_Ntk_t * p ) for ( k = 0; k < Dss_ObjFaninNum(pObj); k++ ) pObj->pFans[k] = Dss_Obj2Lit( pChildren[k] ); } + nPerms = 0; + if ( Dss_NtkCollectPerm_rec( p, p->pRoot, pPermDsd, &nPerms ) ) + p->pRoot = Dss_Regular(p->pRoot); + assert( nPerms == (int)Dss_Regular(p->pRoot)->nSupp ); } /**Function************************************************************* @@ -447,7 +534,7 @@ int Dss_ObjCompare( Dss_Man_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i ) return 1; return 0; } -void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes ) +void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm ) { int i, j, best_i; for ( i = 0; i < nNodes-1; i++ ) @@ -459,6 +546,8 @@ void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes ) if ( i == best_i ) continue; ABC_SWAP( Dss_Obj_t *, pNodes[i], pNodes[best_i] ); + if ( pPerm ) + ABC_SWAP( int, pPerm[i], pPerm[best_i] ); } } @@ -590,18 +679,21 @@ Dss_Man_t * Dss_ManAlloc( int nVars ) pObj->Mirror = 1; } p->vLeaves = Vec_IntAlloc( 32 ); + p->vCopies = Vec_IntAlloc( 32 ); + p->pTtElems = Dss_ManTtElems(); return p; } void Dss_ManFree( Dss_Man_t * p ) { + Vec_IntFreeP( &p->vCopies ); Vec_IntFreeP( &p->vLeaves ); Vec_PtrFreeP( &p->vObjs ); Mem_FlexStop( p->pMem, 0 ); ABC_FREE( p->pBins ); ABC_FREE( p ); } -void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) +void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits ) { char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'}; char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'}; @@ -611,20 +703,25 @@ void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) if ( pObj->Type == DAU_DSD_CONST0 ) { printf( "0" ); return; } if ( pObj->Type == DAU_DSD_VAR ) - { printf( "%c", 'a' + pObj->iVar ); return; } + { + int iPermLit = pPermLits ? pPermLits[pObj->iVar] : Abc_Var2Lit(pObj->iVar, 0); + printf( "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) ); + return; + } printf( "%c", OpenType[pObj->Type] ); Dss_ObjForEachFanin( p, pObj, pFanin, i ) { printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" ); - Dss_ManPrint_rec( p, pFanin ); + Dss_ManPrint_rec( p, pFanin, pPermLits ); } printf( "%c", CloseType[pObj->Type] ); } -void Dss_ManPrintOne( Dss_Man_t * p, Dss_Obj_t * pObj ) +void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits ) { - printf( "%6d : ", Dss_ObjId(pObj) ); - printf( "%2d ", pObj->nSupp ); - Dss_ManPrint_rec( p, pObj ); + printf( "%6d : ", Abc_Lit2Var(iDsdLit) ); + printf( "%2d ", Dss_ManLitSuppSize(p, iDsdLit) ); + printf( "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" ); + Dss_ManPrint_rec( p, Dss_ManObj(p, Abc_Lit2Var(iDsdLit)), pPermLits ); printf( "\n" ); } void Dss_ManPrintAll( Dss_Man_t * p ) @@ -636,12 +733,124 @@ void Dss_ManPrintAll( Dss_Man_t * p ) { if ( (int)pObj->nSupp < nSuppMax ) continue; - Dss_ManPrintOne( p, pObj ); + Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL ); nSuppMax = Abc_MaxInt( nSuppMax, pObj->nSupp ); } printf( "\n" ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk ) +{ + Dss_Obj_t * pObj, * pFanin, * pObjNew; + int i, k; + assert( p->nVars == pNtk->nVars ); + if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 ) + return Dss_IsComplement(pNtk->pRoot); + if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR ) + return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar, Dss_IsComplement(pNtk->pRoot) ); + Vec_IntFill( p->vCopies, Vec_PtrSize(pNtk->vObjs), -1 ); + Dss_NtkForEachNode( pNtk, pObj, i ) + { + Vec_IntClear( p->vLeaves ); + Dss_ObjForEachFaninNtk( pNtk, pObj, pFanin, k ) + if ( pFanin->Type == DAU_DSD_VAR ) + Vec_IntPush( p->vLeaves, Abc_Var2Lit(pFanin->iVar+1, 0) ); + else + Vec_IntPush( p->vLeaves, Abc_Lit2Lit(Vec_IntArray(p->vCopies), pObj->pFans[k]) ); + pObjNew = Dss_ObjCreate( p, pObj->Type, p->vLeaves ); + Vec_IntWriteEntry( p->vCopies, Dss_ObjId(pObj), Dss_ObjId(pObjNew) ); + } + return Abc_Lit2Lit( Vec_IntArray(p->vCopies), Dss_Obj2Lit(pNtk->pRoot) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits ) +{ + Dss_Obj_t * pChild; + int nWords = Abc_TtWordNum(nVars); + int i, fCompl = Dss_IsComplement(pObj); + pObj = Dss_Regular(pObj); + if ( pObj->Type == DAU_DSD_VAR ) + { + int iPermLit = pPermLits[(int)pObj->iVar]; + assert( (int)pObj->iVar < nVars ); + Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) ); + return; + } + if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR ) + { + word pTtTemp[DAU_MAX_WORD]; + if ( pObj->Type == DAU_DSD_AND ) + Abc_TtConst1( pRes, nWords ); + else + Abc_TtConst0( pRes, nWords ); + Dss_ObjForEachChild( p, pObj, pChild, i ) + { + Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits ); + if ( pObj->Type == DAU_DSD_AND ) + Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 ); + else + Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 ); + } + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; + } + if ( pObj->Type == DAU_DSD_MUX ) // mux + { + word pTtTemp[3][DAU_MAX_WORD]; + Dss_ObjForEachChild( p, pObj, pChild, i ) + Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits ); + assert( i == 3 ); + Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords ); + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; + } + if ( pObj->Type == DAU_DSD_PRIME ) // function + { + } + assert( 0 ); + +} +word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits ) +{ + int nWords = Abc_TtWordNum( nVars ); + word * pRes = p->pTtElems[DAU_MAX_VAR]; + assert( nVars <= DAU_MAX_VAR ); + if ( iDsd == 0 ) + Abc_TtConst0( pRes, nWords ); + else if ( iDsd == 1 ) + Abc_TtConst1( pRes, nWords ); + else if ( Abc_Lit2Var(iDsd) < p->nVars ) + { + int iPermLit = pPermLits[Abc_Lit2Var(iDsd)]; + Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) ); + } + else + Dss_ManComputeTruth_rec( p, Dss_Lit2Obj(p, iDsd), nVars, pRes, pPermLits ); + return pRes; +} + /**Function************************************************************* @@ -701,33 +910,64 @@ void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec /**Function************************************************************* - Synopsis [] + Synopsis [Performs DSD operation on the two literals.] - Description [] + Description [Returns the perm of the resulting literals. The perm size + is equal to the number of support variables. The perm variables are 0-based + numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].] SideEffects [] SeeAlso [] ***********************************************************************/ -int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPerm ) +int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm ) { Dss_Obj_t * pChildren[DAU_MAX_VAR]; Dss_Obj_t * pObj, * pChild; - int i, k, nChildren = 0, fCompl = 0, nSupp = 0; + int i, k, nChildren = 0, fCompl = 0; - if ( Type == DAU_DSD_AND ) + assert( Type == DAU_DSD_AND || pPerm == NULL ); + if ( Type == DAU_DSD_AND && pPerm != NULL ) { + int pBegEnd[DAU_MAX_VAR]; + int j, nSSize = 0; for ( k = 0; k < nLits; k++ ) { pObj = Dss_Lit2Obj(p, pLits[k]); if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND ) + { + pBegEnd[nChildren] = (nSSize << 16) | (nSSize + Dss_Regular(pObj)->nSupp); + nSSize += Dss_Regular(pObj)->nSupp; pChildren[nChildren++] = pObj; + } else Dss_ObjForEachChild( p, pObj, pChild, i ) + { + pBegEnd[nChildren] = (nSSize << 16) | (nSSize + Dss_Regular(pChild)->nSupp); + nSSize += Dss_Regular(pChild)->nSupp; pChildren[nChildren++] = pChild; + } } - Dss_ObjSort( p, pChildren, nChildren ); + Dss_ObjSort( p, pChildren, nChildren, pBegEnd ); + // create permutation + for ( j = i = 0; i < nChildren; i++ ) + for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ ) + pPerm[j++] = (unsigned char)Abc_Var2Lit( k, 0 ); + assert( j == nSSize ); + } + else if ( Type == DAU_DSD_AND ) + { + for ( k = 0; k < nLits; k++ ) + { + pObj = Dss_Lit2Obj(p, pLits[k]); + if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND ) + pChildren[nChildren++] = pObj; + else + Dss_ObjForEachChild( p, pObj, pChild, i ) + pChildren[nChildren++] = pChild; + } + Dss_ObjSort( p, pChildren, nChildren, NULL ); } else if ( Type == DAU_DSD_XOR ) { @@ -744,7 +984,7 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPe pChildren[nChildren++] = pChild; } } - Dss_ObjSort( p, pChildren, nChildren ); + Dss_ObjSort( p, pChildren, nChildren, NULL ); } else if ( Type == DAU_DSD_MUX ) { @@ -776,6 +1016,164 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPe pObj->Mirror = pObj->Id; return Abc_Var2Lit( pObj->Id, fCompl ); } +Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int * nFans ) +{ + static char Buffer[100]; + Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer; + pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans ); + pFun->nFans = nFans[0] + nFans[1]; + assert( (int)pFun->nFans == Dss_ManLitSuppSize(p, pFun->iDsd) ); + return pFun; +} + +/**Function************************************************************* + + Synopsis [Performs AND on two DSD functions with support overlap.] + + Description [Returns the perm of the resulting literals. The perm size + is equal to the number of support variables. The perm variables are 0-based + numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans ) +{ + static char Buffer[100]; + Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer; + Dss_Ntk_t * pNtk; + word * pTruthOne, pTruth[DAU_MAX_WORD]; + char pDsd[DAU_MAX_STR]; + int pMapDsd2Truth[DAU_MAX_VAR]; + int pPermLits[DAU_MAX_VAR]; + int pPermDsd[DAU_MAX_VAR]; + int i, nNonDec, nSuppSize = 0; + // create first truth table + for ( i = 0; i < nFans[0]; i++ ) + { + pMapDsd2Truth[nSuppSize] = i; + pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 ); + } + pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits ); + Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 ); +//Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" ); + // create second truth table + for ( i = 0; i < nFans[1]; i++ ) + pPermLits[i] = -1; + for ( i = 0; i < (int)pEnt->nShared; i++ ) + pPermLits[pEnt->pShared[2*i+0]] = pEnt->pShared[2*i+1]; + for ( i = 0; i < nFans[1]; i++ ) + if ( pPermLits[i] == -1 ) + { + pMapDsd2Truth[nSuppSize] = nFans[0] + i; + pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 ); + } + pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits ); +//Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" ); + Abc_TtAnd( pTruth, pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 ); + // perform decomposition + nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, pDsd ); + // derive network and convert it into the manager + pNtk = Dss_NtkCreate( pDsd, p->nVars ); +Dss_NtkPrint( pNtk ); + Dss_NtkCheck( pNtk ); + Dss_NtkTransform( pNtk, pPermDsd ); +Dss_NtkPrint( pNtk ); + pFun->iDsd = Dss_NtkRebuild( p, pNtk ); + Dss_NtkFree( pNtk ); + // pPermDsd maps vars of iDsdRes into literals of pTruth + // translate this map into the one that maps vars of iDsdRes into literals of cut + pFun->nFans = Dss_ManLitSuppSize( p, pFun->iDsd ); + for ( i = 0; i < (int)pFun->nFans; i++ ) + pFun->pFans[i] = (unsigned char)Abc_Lit2Lit( pMapDsd2Truth, pPermDsd[i] ); + return pFun; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// returns mapping of variables of dsd1 into literals of dsd0 +Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask ) +{ + static char Buffer[100]; + Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer; + pEnt->iDsd0 = iDsd[0]; + pEnt->iDsd1 = iDsd[1]; + pEnt->nShared = 0; + if ( uSharedMask ) + { + int i, g, pMapGtoL[DAU_MAX_VAR] = {-1}; + for ( i = 0; i < nFans[0]; i++ ) + pMapGtoL[ Abc_Lit2Var(pFans[0][i]) ] = Abc_Var2Lit( i, Abc_LitIsCompl(pFans[0][i]) ); + for ( i = 0; i < nFans[1]; i++ ) + { + g = Abc_Lit2Var( pFans[1][i] ); + if ( (uSharedMask >> g) & 1 ) + { + assert( pMapGtoL[g] >= 0 ); + pEnt->pShared[2*pEnt->nShared+0] = (unsigned char)i; + pEnt->pShared[2*pEnt->nShared+1] = (unsigned char)Abc_LitNotCond( pMapGtoL[g], Abc_LitIsCompl(pFans[1][i]) ); + pEnt->nShared++; + } + } + } + pEnt->nWords = Dss_EntWordNum( pEnt ); + return pEnt; +} +// merge two DSD functions +int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes ) +{ + Dss_Ent_t * pEnt; + Dss_Fun_t * pFun; + int i; + assert( iDsd[0] <= iDsd[1] ); + // constant argument + if ( iDsd[0] == 0 ) return 0; + if ( iDsd[0] == 1 ) return iDsd[1]; + if ( iDsd[1] == 0 ) return 0; + if ( iDsd[1] == 1 ) return iDsd[0]; + // no overlap + assert( nFans[0] == Dss_ManLitSuppSize(p, iDsd[0]) ); + assert( nFans[1] == Dss_ManLitSuppSize(p, iDsd[1]) ); + assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) ); + // create map of shared variables + pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask ); + // check cache + if ( uSharedMask == 0 ) + pFun = Dss_ManOperationFun( p, iDsd, nFans ); + else + pFun = Dss_ManBooleanAnd( p, pEnt, nFans ); + assert( (int)pFun->nFans == Dss_ManLitSuppSize(p, pFun->iDsd) ); + assert( (int)pFun->nFans <= nKLutSize ); + // create permutation + for ( i = 0; i < (int)pFun->nFans; i++ ) + printf( "%d ", pFun->pFans[i] ); + printf( "\n" ); + + for ( i = 0; i < (int)pFun->nFans; i++ ) + if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec + pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] ); + else + pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[1], pFun->pFans[i] - 2 * nFans[0] ); + + // create permutation + for ( i = 0; i < (int)pFun->nFans; i++ ) + printf( "%d ", pPermRes[i] ); + printf( "\n" ); + + return pFun->iDsd; +} + /**Function************************************************************* @@ -976,6 +1374,55 @@ void Dau_DsdTest_() } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_DsdTest444() +{ + Dss_Man_t * p = Dss_ManAlloc( 6 ); + int iLit1[3] = { 2, 4 }; + int iLit2[3] = { 2, 4, 6 }; + int iRes[5]; + int nFans[2] = { 4, 3 }; + int pPermLits1[4] = { 0, 2, 5, 6 }; + int pPermLits2[5] = { 2, 9, 10 }; + int * pPermLits[2] = { pPermLits1, pPermLits2 }; + unsigned char pPermRes[6]; + int pPermResInt[6]; + unsigned uMaskShared = 2; + int i; + + iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL ); + iRes[1] = iRes[0]; + iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL ); + iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL ); + + Dss_ManPrintOne( p, iRes[0], NULL ); + Dss_ManPrintOne( p, iRes[2], NULL ); + Dss_ManPrintOne( p, iRes[3], NULL ); + + Dss_ManPrintOne( p, iRes[2], pPermLits1 ); + Dss_ManPrintOne( p, iRes[3], pPermLits2 ); + + iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes ); + + for ( i = 0; i < 6; i++ ) + pPermResInt[i] = pPermRes[i]; + + Dss_ManPrintOne( p, iRes[4], NULL ); + Dss_ManPrintOne( p, iRes[4], pPermResInt ); + + Dss_ManFree( p ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |