diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-20 21:34:40 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-20 21:34:40 -0800 |
commit | b2fd119933166ad7d9e4132ebb8aaf422bfcdb8a (patch) | |
tree | f41993309b2f4a791e92b581562e24e462096bc6 /src/opt | |
parent | ffbe3bc5767c597b3ca612a12e671749f23ca34f (diff) | |
download | abc-b2fd119933166ad7d9e4132ebb8aaf422bfcdb8a.tar.gz abc-b2fd119933166ad7d9e4132ebb8aaf422bfcdb8a.tar.bz2 abc-b2fd119933166ad7d9e4132ebb8aaf422bfcdb8a.zip |
DSD manager.
Diffstat (limited to 'src/opt')
-rw-r--r-- | src/opt/dau/dau.h | 11 | ||||
-rw-r--r-- | src/opt/dau/dauDsd.c | 37 | ||||
-rw-r--r-- | src/opt/dau/dauMerge.c | 2 | ||||
-rw-r--r-- | src/opt/dau/dauTree.c | 494 |
4 files changed, 418 insertions, 126 deletions
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index 7eb0b975..f80b599e 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -77,20 +77,23 @@ static inline int Dau_DsdReadVar( char * p ) { if ( *p == '!' ) p++; return *p /*=== dauCanon.c ==========================================================*/ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ); /*=== dauDsd.c ==========================================================*/ -extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes ); +extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes ); +extern void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit ); extern word * Dau_DsdToTruth( char * p, int nVars ); extern word Dau_Dsd6ToTruth( char * p ); extern void Dau_DsdNormalize( char * p ); extern int Dau_DsdCountAnds( char * pDsd ); +extern void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR ); /*=== dauMerge.c ==========================================================*/ 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 ); +/*=== dauTree.c ==========================================================*/ +extern Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit ); 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 ); +extern int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPerm, word * pTruth ); +extern void Dss_ManPrint( Dss_Man_t * p ); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index df3dac3c..d9401895 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -896,7 +896,7 @@ int Dau_DsdCheck1Step( word * pTruth, int nVarsInit ) int nWords = Abc_TtWordNum(nVarsInit); int nSizeNonDec, nSizeNonDec0, nSizeNonDec1; int v, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs; - nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, NULL ); + nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, 0, NULL ); if ( nSizeNonDec == 0 ) return -1; assert( nSizeNonDec > 0 ); @@ -905,11 +905,11 @@ int Dau_DsdCheck1Step( word * pTruth, int nVarsInit ) // try first cofactor Abc_TtCofactor0p( pCofTemp, pTruth, nWords, v ); nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit ); - nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL ); + nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL ); // try second cofactor Abc_TtCofactor1p( pCofTemp, pTruth, nWords, v ); nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit ); - nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL ); + nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL ); // compare cofactors if ( nSizeNonDec0 || nSizeNonDec1 ) continue; @@ -943,6 +943,7 @@ struct Dau_Dsd_t_ int nConsts; // the number of constant decompositions int uConstMask; // constant decomposition mask int fSplitPrime; // represent prime function as 1-step DSD + int fWriteTruth; // writing truth table as a hex string char pVarDefs[32][8]; // variable definitions char Cache[32][32]; // variable cache char pOutput[DAU_MAX_STR]; // output stream @@ -1023,19 +1024,19 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, Dau_DsdWriteVar( p, pVars[vBest], 0 ); // split decomposition Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest ); - nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes ); + nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes ); assert( nNonDecSize == 0 ); Dau_DsdWriteString( p, pRes ); // split decomposition Abc_TtCofactor0p( pCofTemp, pTruth, nWords, vBest ); - nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes ); + nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes ); assert( nNonDecSize == 0 ); Dau_DsdWriteString( p, pRes ); Dau_DsdWriteString( p, ">" ); RetValue = 1; } } - else + else if ( p->fWriteTruth ) p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars ); Dau_DsdWriteString( p, "{" ); for ( v = 0; v < nVars; v++ ) @@ -1333,11 +1334,15 @@ static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTrut Dau_DsdDecomposeInt( p1, &tCof1, nVars - 1 ); Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput ); p->nSizeNonDec = p1->nSizeNonDec; + if ( p1->nSizeNonDec ) + *pTruth = tCof1; // split decomposition Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 ); Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput ); Dau_DsdWriteString( p, ">" ); p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec ); + if ( p1->nSizeNonDec ) + *pTruth = tCof0; return 0; } static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports ) @@ -1693,6 +1698,7 @@ static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth word pTtCof[2][DAU_MAX_WORD]; int nWords = Abc_TtWordNum(nVars); p1->fSplitPrime = 0; + p1->fWriteTruth = p->fWriteTruth; // move this variable to the top ABC_SWAP( int, pVars[v], pVars[nVars-1] ); Abc_TtSwapVars( pTruth, nVars, v, nVars-1 ); @@ -1708,11 +1714,15 @@ static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth Dau_DsdDecomposeInt( p1, pTtCof[1], nVars - 1 ); Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput ); p->nSizeNonDec = p1->nSizeNonDec; + if ( p1->nSizeNonDec ) + Abc_TtCopy( pTruth, pTtCof[1], Abc_TtWordNum(p1->nSizeNonDec), 0 ); // split decomposition Dau_DsdDecomposeInt( p1, pTtCof[0], nVars - 1 ); Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput ); Dau_DsdWriteString( p, ">" ); p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec ); + if ( p1->nSizeNonDec ) + Abc_TtCopy( pTruth, pTtCof[0], Abc_TtWordNum(p1->nSizeNonDec), 0 ); return 0; } static inline int Dau_DsdDecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports ) @@ -1863,10 +1873,11 @@ int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ) Dau_DsdFinalize( p ); return Status; } -int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes ) +int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes ) { Dau_Dsd_t P, * p = &P; p->fSplitPrime = fSplitPrime; + p->fWriteTruth = fWriteTruth; p->nSizeNonDec = 0; if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) ) { if ( pRes ) pRes[0] = '0', pRes[1] = 0; } @@ -1885,6 +1896,12 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes // assert( p->nSizeNonDec == 0 ); return p->nSizeNonDec; } +void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit ) +{ + char pRes[DAU_MAX_STR]; + Dau_DsdDecompose( pTruth, nVarsInit, 0, 1, pRes ); + fprintf( pFile, "%s\n", pRes ); +} void Dau_DsdTest44() { @@ -1899,7 +1916,7 @@ void Dau_DsdTest44() // char * pStr3; word t = Dau_Dsd6ToTruth( pStr ); // return; - int nNonDec = Dau_DsdDecompose( &t, 6, 1, pRes ); + int nNonDec = Dau_DsdDecompose( &t, 6, 1, 1, pRes ); // Dau_DsdNormalize( pStr2 ); // Dau_DsdExtract( pStr, 2, 0 ); t = 0; @@ -1937,7 +1954,7 @@ void Dau_DsdTest888() Dau_DsdPrintSupports( uSupp, nVars ); } */ - Status = Dau_DsdDecompose( pTruth, nVars, 0, pDsd ); + Status = Dau_DsdDecompose( pTruth, nVars, 0, 0, pDsd ); i = 0; } @@ -1973,7 +1990,7 @@ void Dau_DsdTest555() Abc_TtCopy( Tru[0], pTruth, nWords, 0 ); Abc_TtCopy( Tru[1], pTruth, nWords, 0 ); clk2 = clock(); - nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, pRes ); + nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, 1, pRes ); clkDec += clock() - clk2; Dau_DsdNormalize( pRes ); // pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0; diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c index 2ce113be..08eaff73 100644 --- a/src/opt/dau/dauMerge.c +++ b/src/opt/dau/dauMerge.c @@ -717,7 +717,7 @@ Dau_DsdMergeStorePrintDefs( pS ); // assert( nVarsTotal <= 6 ); sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 ); pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal ); - Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, pS->pOutput ); + Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, pS->pOutput ); //printf( "%d ", Status ); if ( Status == -1 ) // did not find 1-step DSD return NULL; diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index d8bc8473..9e94ba29 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -58,7 +58,7 @@ struct Dss_Obj_t_ unsigned fMark1 : 1; // user mark unsigned iVar : 8; // variable unsigned nSupp : 8; // variable - unsigned Data : 8; // variable + unsigned nWords : 8; // variable unsigned Type : 3; // node type unsigned nFans : 5; // fanin count unsigned pFans[0]; // fanins @@ -70,7 +70,7 @@ struct Dss_Ntk_t_ int nVars; // the number of variables int nMem; // memory used int nMemAlloc; // memory allocated - Dss_Obj_t * pMem; // memory array + word * pMem; // memory array Dss_Obj_t * pRoot; // root node Vec_Ptr_t * vObjs; // internal nodes }; @@ -78,6 +78,7 @@ struct Dss_Ntk_t_ struct Dss_Man_t_ { int nVars; // variable number + int nNonDecLimit; // limit on non-dec size int nBins; // table size unsigned * pBins; // hash table Mem_Flex_t * pMem; // memory for nodes @@ -98,7 +99,9 @@ static inline int Dss_ObjType( Dss_Obj_t * pObj ) 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)); } + +static inline int Dss_ObjWordNum( int nFans ) { return sizeof(Dss_Obj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); } +static inline word * Dss_ObjTruth( Dss_Obj_t * pObj ) { return (word *)pObj + pObj->nWords; } static inline Dss_Obj_t * Dss_NtkObj( Dss_Ntk_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p->vObjs, Id); } static inline Dss_Obj_t * Dss_NtkConst0( Dss_Ntk_t * p ) { return Dss_NtkObj( p, 0 ); } @@ -192,24 +195,25 @@ static inline word ** Dss_ManTtElems() ***********************************************************************/ Dss_Obj_t * Dss_ObjAllocNtk( Dss_Ntk_t * p, int Type, int nFans, int nTruthVars ) { - int nStructs = 1 + (nFans / sizeof(Dss_Obj_t)) + (nFans % sizeof(Dss_Obj_t) > 0); - Dss_Obj_t * pObj = p->pMem + p->nMem; - p->nMem += nStructs; - assert( p->nMem < p->nMemAlloc ); + Dss_Obj_t * pObj; + pObj = (Dss_Obj_t *)(p->pMem + p->nMem); Dss_ObjClean( pObj ); - pObj->Type = Type; pObj->nFans = nFans; + pObj->nWords = Dss_ObjWordNum( nFans ); + pObj->Type = Type; pObj->Id = Vec_PtrSize( p->vObjs ); pObj->iVar = 31; pObj->Mirror = ~0; Vec_PtrPush( p->vObjs, pObj ); + p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0); + assert( p->nMem < p->nMemAlloc ); return pObj; } Dss_Obj_t * Dss_ObjCreateNtk( Dss_Ntk_t * p, int Type, Vec_Int_t * vFaninLits ) { Dss_Obj_t * pObj; int i, Entry; - pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), 0 ); + pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 ); Vec_IntForEachEntry( vFaninLits, Entry, i ) { pObj->pFans[i] = Entry; @@ -226,7 +230,7 @@ Dss_Ntk_t * Dss_NtkAlloc( int nVars ) p = ABC_CALLOC( Dss_Ntk_t, 1 ); p->nVars = nVars; p->nMemAlloc = DAU_MAX_STR; - p->pMem = ABC_ALLOC( Dss_Obj_t, p->nMemAlloc ); + p->pMem = ABC_ALLOC( word, p->nMemAlloc ); p->vObjs = Vec_PtrAlloc( 100 ); Dss_ObjAllocNtk( p, DAU_DSD_CONST0, 0, 0 ); for ( i = 0; i < nVars; i++ ) @@ -252,6 +256,8 @@ void Dss_NtkPrint_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj ) assert( !Dss_IsComplement(pObj) ); if ( pObj->Type == DAU_DSD_VAR ) { printf( "%c", 'a' + pObj->iVar ); return; } + if ( pObj->Type == DAU_DSD_PRIME ) + Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans ); printf( "%c", OpenType[pObj->Type] ); Dss_ObjForEachFaninNtk( p, pObj, pFanin, i ) { @@ -311,12 +317,14 @@ int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk } while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) (*p)++; +/* if ( **p == '<' ) { char * q = pStr + pMatches[ *p - pStr ]; if ( *(q+1) == '{' ) *p = q+1; } +*/ if ( **p >= 'a' && **p <= 'z' ) // var return Abc_Var2Lit( Dss_ObjId(Dss_NtkVar(pNtk, **p - 'a')), fCompl ); if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor @@ -345,7 +353,7 @@ int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk assert( 0 ); return -1; } -Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars ) +Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth ) { int fCompl = 0; Dss_Ntk_t * pNtk = Dss_NtkAlloc( nVars ); @@ -361,6 +369,21 @@ Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars ) Dau_DsdMergeMatches( pDsd, pMatches ); iLit = Dss_NtkCreate_rec( pDsd, &pDsd, pMatches, pNtk ); pNtk->pRoot = Dss_Lit2ObjNtk( pNtk, iLit ); + // assign the truth table + if ( pTruth ) + { + Dss_Obj_t * pObj; + int k, Counter = 0; + Dss_NtkForEachNode( pNtk, pObj, k ) + if ( pObj->Type == DAU_DSD_PRIME ) + { +// Kit_DsdPrintFromTruth( (unsigned *)pTruth, nVars ); printf( "\n" ); + + Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(pObj->nFans), 0 ); + Counter++; + } + assert( Counter < 2 ); + } } if ( fCompl ) pNtk->pRoot = Dss_Not(pNtk->pRoot); @@ -477,6 +500,8 @@ void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd ) return; Dss_NtkForEachNode( p, pObj, i ) { + if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME ) + continue; Dss_ObjForEachChildNtk( p, pObj, pChild, k ) pChildren[k] = pChild; Dss_ObjSortNtk( p, pChildren, Dss_ObjFaninNum(pObj) ); @@ -512,8 +537,8 @@ int Dss_ObjCompare( Dss_Man_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i ) return 1; if ( Dss_ObjType(p0) < DAU_DSD_AND ) { - assert( !Dss_IsComplement(p0i) ); - assert( !Dss_IsComplement(p1i) ); +// assert( !Dss_IsComplement(p0i) ); +// assert( !Dss_IsComplement(p1i) ); return 0; } if ( Dss_ObjFaninNum(p0) < Dss_ObjFaninNum(p1) ) @@ -565,19 +590,19 @@ void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm ) ***********************************************************************/ Dss_Obj_t * Dss_ObjAlloc( Dss_Man_t * p, int Type, int nFans, int nTruthVars ) { - int nInts = sizeof(Dss_Obj_t) / sizeof(int) + nFans; - int nWords = (nInts >> 1) + (nInts & 1) + (nTruthVars ? Abc_Truth6WordNum(nTruthVars) : 0); + int nWords = Dss_ObjWordNum(nFans) + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0); Dss_Obj_t * pObj = (Dss_Obj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords ); Dss_ObjClean( pObj ); pObj->Type = Type; pObj->nFans = nFans; + pObj->nWords = Dss_ObjWordNum(nFans); pObj->Id = Vec_PtrSize( p->vObjs ); pObj->iVar = 31; pObj->Mirror = ~0; Vec_PtrPush( p->vObjs, pObj ); return pObj; } -Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) +Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth ) { Dss_Obj_t * pObj, * pFanin, * pPrev = NULL; int i, Entry; @@ -595,13 +620,21 @@ Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) pPrev = pFanin; } // create new node - pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), 0 ); + pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 ); + if ( Type == DAU_DSD_PRIME ) + Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(Vec_IntSize(vFaninLits)), 0 ); assert( pObj->nSupp == 0 ); Vec_IntForEachEntry( vFaninLits, Entry, i ) { pObj->pFans[i] = Entry; pObj->nSupp += Dss_ObjFanin(p, pObj, i)->nSupp; } +/* + { + extern void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits ); + Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL ); + } +*/ return pObj; } @@ -616,34 +649,60 @@ Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) SeeAlso [] ***********************************************************************/ -static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) +void Dss_ManHashProfile( Dss_Man_t * p ) +{ + Dss_Obj_t * pObj; + unsigned * pSpot; + int i, Counter; + for ( i = 0; i < p->nBins; i++ ) + { + Counter = 0; + for ( pSpot = p->pBins + i; *pSpot; pSpot = &pObj->Next, Counter++ ) + pObj = Dss_ManObj( p, *pSpot ); + if ( Counter ) + printf( "%d ", Counter ); + } + printf( "\n" ); +} +static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth ) { static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 }; int i, Entry; unsigned uHash = Type * 7873 + Vec_IntSize(vFaninLits) * 8147; Vec_IntForEachEntry( vFaninLits, Entry, i ) uHash += Entry * s_Primes[i & 0x7]; + assert( (Type == DAU_DSD_PRIME) == (pTruth != NULL) ); + if ( pTruth ) + { + unsigned char * pTruthC = (unsigned char *)pTruth; + int nBytes = Abc_TtByteNum(Vec_IntSize(vFaninLits)); + for ( i = 0; i < nBytes; i++ ) + uHash += pTruthC[i] * s_Primes[i & 0x7]; + } return uHash % p->nBins; } -unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) +unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth ) { Dss_Obj_t * pObj; - unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits); + unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth); for ( ; *pSpot; pSpot = &pObj->Next ) { pObj = Dss_ManObj( p, *pSpot ); - if ( (int)pObj->Type == Type && (int)pObj->nFans == Vec_IntSize(vFaninLits) && !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) ) // equal + if ( (int)pObj->Type == Type && + (int)pObj->nFans == Vec_IntSize(vFaninLits) && + !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) && + (pTruth == NULL || !memcmp(Dss_ObjTruth(pObj), pTruth, Abc_TtByteNum(pObj->nFans))) ) // equal return pSpot; } return pSpot; } -Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) +Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth ) { Dss_Obj_t * pObj; - unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits ); + unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth ); if ( *pSpot ) return Dss_ManObj( p, *pSpot ); - pObj = Dss_ObjCreate( p, Type, vFaninLits ); + pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth ); *pSpot = pObj->Id; return pObj; } @@ -659,17 +718,18 @@ Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) SeeAlso [] ***********************************************************************/ -Dss_Man_t * Dss_ManAlloc( int nVars ) +Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit ) { Dss_Man_t * p; Dss_Obj_t * pObj; int i; p = ABC_CALLOC( Dss_Man_t, 1 ); p->nVars = nVars; - p->nBins = Abc_PrimeCudd( 1000 ); + p->nNonDecLimit = nNonDecLimit; + p->nBins = Abc_PrimeCudd( 100000 ); p->pBins = ABC_CALLOC( unsigned, p->nBins ); p->pMem = Mem_FlexStart(); - p->vObjs = Vec_PtrAlloc( 1000 ); + p->vObjs = Vec_PtrAlloc( 10000 ); Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 ); for ( i = 0; i < nVars; i++ ) { @@ -708,6 +768,8 @@ void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits ) printf( "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) ); return; } + if ( pObj->Type == DAU_DSD_PRIME ) + Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans ); printf( "%c", OpenType[pObj->Type] ); Dss_ObjForEachFanin( p, pObj, pFanin, i ) { @@ -724,54 +786,95 @@ void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits ) Dss_ManPrint_rec( p, Dss_ManObj(p, Abc_Lit2Var(iDsdLit)), pPermLits ); printf( "\n" ); } -void Dss_ManPrintAll( Dss_Man_t * p ) +int Dss_ManPrintIndex_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) { + Dss_Obj_t * pFanin; + int i, nVarsMax = 0; + assert( !Dss_IsComplement(pObj) ); + if ( pObj->Type == DAU_DSD_CONST0 ) + return 0; + if ( pObj->Type == DAU_DSD_VAR ) + return pObj->iVar + 1; + Dss_ObjForEachFanin( p, pObj, pFanin, i ) + nVarsMax = Abc_MaxInt( nVarsMax, Dss_ManPrintIndex_rec(p, pFanin) ); + return nVarsMax; +} +int Dss_ManCheckNonDec_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) +{ + Dss_Obj_t * pFanin; + int i; + assert( !Dss_IsComplement(pObj) ); + if ( pObj->Type == DAU_DSD_CONST0 ) + return 0; + if ( pObj->Type == DAU_DSD_VAR ) + return 0; + if ( pObj->Type == DAU_DSD_PRIME ) + return 1; + Dss_ObjForEachFanin( p, pObj, pFanin, i ) + if ( Dss_ManCheckNonDec_rec( p, pFanin ) ) + return 1; + return 0; +} +void Dss_ManDump( Dss_Man_t * p ) +{ + char * pFileName = "dss_tts.txt"; + FILE * pFile; + word Temp[DAU_MAX_WORD]; Dss_Obj_t * pObj; - int i, nSuppMax = 0; - printf( "DSD manager contains %d objects:\n", Vec_PtrSize(p->vObjs) ); + int i; + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", pFileName ); + return; + } Dss_ManForEachObj( p, pObj, i ) { - if ( (int)pObj->nSupp < nSuppMax ) + if ( pObj->Type != DAU_DSD_PRIME ) continue; - Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL ); - nSuppMax = Abc_MaxInt( nSuppMax, pObj->nSupp ); + Abc_TtCopy( Temp, Dss_ObjTruth(pObj), Abc_TtWordNum(pObj->nFans), 0 ); + Abc_TtStretch6( Temp, pObj->nFans, p->nVars ); + fprintf( pFile, "0x" ); + Abc_TtPrintHexRev( pFile, Temp, p->nVars ); + fprintf( pFile, "\n" ); + +// printf( "%6d : ", i ); +// Abc_TtPrintHexRev( stdout, Temp, p->nVars ); +// printf( " " ); +// Dau_DsdPrintFromTruth( stdout, Temp, p->nVars ); } - printf( "\n" ); + fclose( pFile ); } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk ) +void Dss_ManPrint( Dss_Man_t * p ) { - 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 ) + Dss_Obj_t * pObj; + int i, c, CountStr = 0, CountNonDsd = 0, CountNonDsdStr = 0; + int clk = clock(); + Dss_ManForEachObj( p, 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) ); + CountStr += ((int)pObj->nSupp == Dss_ManPrintIndex_rec(p, pObj)); + CountNonDsd += (pObj->Type == DAU_DSD_PRIME); + CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj ); } - return Abc_Lit2Lit( Vec_IntArray(p->vCopies), Dss_Obj2Lit(pNtk->pRoot) ); + printf( "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) ); + printf( "Total number of structures = %8d\n", CountStr ); + printf( "Non-DSD objects (max =%2d) = %8d\n", p->nNonDecLimit, CountNonDsd ); + printf( "Non-DSD structures = %8d\n", CountNonDsdStr ); + printf( "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); + printf( "Memory used for array = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); + printf( "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) ); + Abc_PrintTime( 1, "Time", clock() - clk ); +// Dss_ManHashProfile( p ); +// Dss_ManDump( p ); +// return; + c = 0; + Dss_ManForEachObj( p, pObj, i ) + if ( (int)pObj->nSupp == Dss_ManPrintIndex_rec(p, pObj) ) + { + printf( "%6d : ", c++ ); + Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL ); + } + printf( "\n" ); } /**Function************************************************************* @@ -828,26 +931,33 @@ void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * } if ( pObj->Type == DAU_DSD_PRIME ) // function { + word pFanins[DAU_MAX_VAR][DAU_MAX_WORD]; + Dss_ObjForEachChild( p, pObj, pChild, i ) + Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits ); + Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords ); + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; } assert( 0 ); } word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits ) { - int nWords = Abc_TtWordNum( nVars ); + Dss_Obj_t * pObj = Dss_Lit2Obj(p, iDsd); word * pRes = p->pTtElems[DAU_MAX_VAR]; + int nWords = Abc_TtWordNum( nVars ); 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 ) + else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR ) { - int iPermLit = pPermLits[Abc_Lit2Var(iDsd)]; + int iPermLit = pPermLits[Dss_Regular(pObj)->iVar]; 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 ); + Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits ); return pRes; } @@ -888,7 +998,7 @@ Dss_Obj_t * Dss_ManShiftTree_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) nSupp += pFanin->nSupp; } // create new graph - pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, vFaninLits ); + pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, vFaninLits, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL ); pObjNew->Mirror = pObj->Id; Vec_IntFree( vFaninLits ); return pObjNew; @@ -910,6 +1020,90 @@ void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec /**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) ); +} +*/ + +// returns literal of non-shifted tree in p, corresponding to pObj in pNtk, which may be compl +int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj ) +{ + Dss_Obj_t * pChildren[DAU_MAX_VAR]; + Dss_Obj_t * pChild, * pObjNew; + int k, fCompl = Dss_IsComplement(pObj); + pObj = Dss_Regular(pObj); + if ( pObj->Type == DAU_DSD_VAR ) + return Abc_Var2Lit( 1, fCompl ); + Dss_ObjForEachChildNtk( pNtk, pObj, pChild, k ) + { + pChildren[k] = Dss_Lit2Obj( p, Dss_NtkRebuild_rec( p, pNtk, pChild ) ); + if ( pObj->Type == DAU_DSD_XOR && Dss_IsComplement(pChildren[k]) ) + pChildren[k] = Dss_Not(pChildren[k]), fCompl ^= 1; + } + // normalize MUX + if ( pObj->Type == DAU_DSD_MUX ) + { + if ( Dss_IsComplement(pChildren[0]) ) + { + pChildren[0] = Dss_Not(pChildren[0]); + ABC_SWAP( Dss_Obj_t *, pChildren[1], pChildren[2] ); + } + if ( Dss_IsComplement(pChildren[1]) ) + { + pChildren[1] = Dss_Not(pChildren[1]); + pChildren[2] = Dss_Not(pChildren[2]); + fCompl ^= 1; + } + } + // shift subgraphs + Dss_ManShiftTree( p, pChildren, k, p->vLeaves ); + // create new graph + pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL ); + pObjNew->Mirror = pObjNew->Id; + return Abc_Var2Lit( pObjNew->Id, fCompl ); +} +int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk ) +{ + 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 + 1, Dss_IsComplement(pNtk->pRoot) ); + return Dss_NtkRebuild_rec( p, pNtk, pNtk->pRoot ); +} + +/**Function************************************************************* + Synopsis [Performs DSD operation on the two literals.] Description [Returns the perm of the resulting literals. The perm size @@ -921,11 +1115,11 @@ void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec SeeAlso [] ***********************************************************************/ -int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm ) +int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth ) { Dss_Obj_t * pChildren[DAU_MAX_VAR]; Dss_Obj_t * pObj, * pChild; - int i, k, nChildren = 0, fCompl = 0; + int i, k, nChildren = 0, fCompl = 0, fComplFan; assert( Type == DAU_DSD_AND || pPerm == NULL ); if ( Type == DAU_DSD_AND && pPerm != NULL ) @@ -937,14 +1131,20 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned pObj = Dss_Lit2Obj(p, pLits[k]); if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND ) { - pBegEnd[nChildren] = (nSSize << 16) | (nSSize + Dss_Regular(pObj)->nSupp); + fComplFan = (Dss_Regular(pObj)->Type == DAU_DSD_VAR && Dss_IsComplement(pObj)); + if ( fComplFan ) + pObj = Dss_Regular(pObj); + pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (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); + fComplFan = (Dss_Regular(pChild)->Type == DAU_DSD_VAR && Dss_IsComplement(pChild)); + if ( fComplFan ) + pChild = Dss_Regular(pChild); + pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pChild)->nSupp); nSSize += Dss_Regular(pChild)->nSupp; pChildren[nChildren++] = pChild; } @@ -953,7 +1153,7 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned // 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 ); + pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 ); assert( j == nSSize ); } else if ( Type == DAU_DSD_AND ) @@ -988,31 +1188,31 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned } else if ( Type == DAU_DSD_MUX ) { - fCompl = Abc_LitIsCompl(pLits[1]) && Abc_LitIsCompl(pLits[2]); if ( Abc_LitIsCompl(pLits[0]) ) { - pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[0], 1)); - pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[2], fCompl)); - pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[1], fCompl)); + pLits[0] = Abc_LitNot(pLits[0]); + ABC_SWAP( int, pLits[1], pLits[2] ); } - else + if ( Abc_LitIsCompl(pLits[1]) ) { - pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[0], 0)); - pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[1], fCompl)); - pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[2], fCompl)); + pLits[1] = Abc_LitNot(pLits[1]); + pLits[2] = Abc_LitNot(pLits[2]); + fCompl ^= 1; } + for ( k = 0; k < nLits; k++ ) + pChildren[nChildren++] = Dss_Lit2Obj(p, pLits[k]); } else if ( Type == DAU_DSD_PRIME ) { for ( k = 0; k < nLits; k++ ) - pChildren[nChildren++] = Dss_Lit2Obj(p, pLits[k]); + pChildren[nChildren++] = Dss_Lit2Obj(p, pLits[k]); } else assert( 0 ); // shift subgraphs Dss_ManShiftTree( p, pChildren, nChildren, p->vLeaves ); // create new graph - pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves ); + pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth ); pObj->Mirror = pObj->Id; return Abc_Var2Lit( pObj->Id, fCompl ); } @@ -1020,7 +1220,7 @@ 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->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans, NULL ); pFun->nFans = nFans[0] + nFans[1]; assert( (int)pFun->nFans == Dss_ManLitSuppSize(p, pFun->iDsd) ); return pFun; @@ -1039,7 +1239,7 @@ Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int * nFans ) SeeAlso [] ***********************************************************************/ -Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans ) +Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans, int Counter ) { static char Buffer[100]; Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer; @@ -1058,7 +1258,10 @@ Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans ) } pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits ); Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 ); +if ( Counter ) +{ //Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" ); +} // create second truth table for ( i = 0; i < nFans[1]; i++ ) pPermLits[i] = -1; @@ -1071,16 +1274,21 @@ Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans ) pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 ); } pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits ); +if ( Counter ) +{ //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 ); + nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, 0, pDsd ); + if ( p->nNonDecLimit && nNonDec > p->nNonDecLimit ) + return NULL; // derive network and convert it into the manager - pNtk = Dss_NtkCreate( pDsd, p->nVars ); -Dss_NtkPrint( pNtk ); + pNtk = Dss_NtkCreate( pDsd, p->nVars, nNonDec ? pTruth : NULL ); +//Dss_NtkPrint( pNtk ); Dss_NtkCheck( pNtk ); Dss_NtkTransform( pNtk, pPermDsd ); -Dss_NtkPrint( pNtk ); +//Dss_NtkPrint( pNtk ); pFun->iDsd = Dss_NtkRebuild( p, pNtk ); Dss_NtkFree( pNtk ); // pPermDsd maps vars of iDsdRes into literals of pTruth @@ -1131,12 +1339,32 @@ Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFa 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 ) +int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes, word * pTruth ) { + int fVerbose = 0; + static int Counter = 0; +// word pTtTemp[DAU_MAX_WORD]; + word * pTruthOne; + int pPermResInt[DAU_MAX_VAR]; Dss_Ent_t * pEnt; Dss_Fun_t * pFun; int i; + Counter++; + + if ( Counter == 122053 ) + { + int s = 0; +// fVerbose = 1; + } + assert( iDsd[0] <= iDsd[1] ); + +if ( fVerbose ) +{ +Dss_ManPrintOne( p, iDsd[0], pFans[0] ); +Dss_ManPrintOne( p, iDsd[1], pFans[1] ); +} + // constant argument if ( iDsd[0] == 0 ) return 0; if ( iDsd[0] == 1 ) return iDsd[1]; @@ -1152,24 +1380,68 @@ int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned if ( uSharedMask == 0 ) pFun = Dss_ManOperationFun( p, iDsd, nFans ); else - pFun = Dss_ManBooleanAnd( p, pEnt, nFans ); + pFun = Dss_ManBooleanAnd( p, pEnt, nFans, 0 ); + if ( pFun == NULL ) + return -1; 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" ); +*/ + + + // perform support minimization + if ( uSharedMask && pFun->nFans > 1 ) + { + int pVarPres[DAU_MAX_VAR]; + int nSupp = 0; + for ( i = 0; i < p->nVars; i++ ) + pVarPres[i] = -1; + for ( i = 0; i < (int)pFun->nFans; i++ ) + pVarPres[ Abc_Lit2Var(pPermRes[i]) ] = i; + for ( i = 0; i < p->nVars; i++ ) + if ( pVarPres[i] >= 0 ) + pPermRes[pVarPres[i]] = Abc_Var2Lit( nSupp++, Abc_LitIsCompl(pPermRes[pVarPres[i]]) ); + assert( nSupp == (int)pFun->nFans ); + } + + for ( i = 0; i < (int)pFun->nFans; i++ ) + pPermResInt[i] = pPermRes[i]; + +if ( fVerbose ) +{ +Dss_ManPrintOne( p, pFun->iDsd, pPermResInt ); +printf( "\n" ); +} + +if ( Counter == 134 ) +{ + int s = 0; +// Dss_ManPrint( p ); +} + pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt ); + if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) ) + { + int s; +// Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" ); +// Kit_DsdPrintFromTruth( pTruth, p->nVars ); printf( "\n" ); + printf( "Verification failed.\n" ); + s = 0; + } return pFun->iDsd; } @@ -1231,7 +1503,7 @@ void Dau_DsdTest() int nVars = 8; // char * pDsd = "[(ab)(cd)]"; char * pDsd = "(!(a!(bh))[cde]!(fg))"; - Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars ); + Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars, NULL ); // Dss_NtkPrint( pNtk ); // Dss_NtkCheck( pNtk ); // Dss_NtkTransform( pNtk ); @@ -1263,7 +1535,7 @@ void Dau_DsdTest_() assert( nVars < DAU_MAX_VAR ); - p = Dss_ManAlloc( nVars ); + p = Dss_ManAlloc( nVars, 0 ); // init Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_ManVar(p, 0)) ); @@ -1284,14 +1556,14 @@ void Dau_DsdTest_() int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[0])) ); int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[1])) ); - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); if ( fAddInv0 ) { pEntries[0] = Abc_LitNot( pEntries[0] ); - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL ); pEntries[0] = Abc_LitNot( pEntries[0] ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); @@ -1300,7 +1572,7 @@ void Dau_DsdTest_() if ( fAddInv1 ) { pEntries[1] = Abc_LitNot( pEntries[1] ); - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL ); pEntries[1] = Abc_LitNot( pEntries[1] ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); @@ -1310,14 +1582,14 @@ void Dau_DsdTest_() { pEntries[0] = Abc_LitNot( pEntries[0] ); pEntries[1] = Abc_LitNot( pEntries[1] ); - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL ); pEntries[0] = Abc_LitNot( pEntries[0] ); pEntries[1] = Abc_LitNot( pEntries[1] ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); } - iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL, NULL ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); } @@ -1342,14 +1614,14 @@ void Dau_DsdTest_() if ( !fAddInv0 && k > j ) continue; - iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); if ( fAddInv1 ) { pEntries[1] = Abc_LitNot( pEntries[1] ); - iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL ); pEntries[1] = Abc_LitNot( pEntries[1] ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); @@ -1358,7 +1630,7 @@ void Dau_DsdTest_() if ( fAddInv2 ) { pEntries[2] = Abc_LitNot( pEntries[2] ); - iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL ); + iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL ); pEntries[2] = Abc_LitNot( pEntries[2] ); assert( !Abc_LitIsCompl(iLit) ); Vec_IntPush( vRes, iLit ); @@ -1367,7 +1639,7 @@ void Dau_DsdTest_() } Vec_IntUniqify( vRes ); } - Dss_ManPrintAll( p ); + Dss_ManPrint( p ); Dss_ManFree( p ); Vec_VecFree( vFuncs ); @@ -1387,7 +1659,7 @@ void Dau_DsdTest_() ***********************************************************************/ void Dau_DsdTest444() { - Dss_Man_t * p = Dss_ManAlloc( 6 ); + Dss_Man_t * p = Dss_ManAlloc( 6, 0 ); int iLit1[3] = { 2, 4 }; int iLit2[3] = { 2, 4, 6 }; int iRes[5]; @@ -1400,10 +1672,10 @@ void Dau_DsdTest444() unsigned uMaskShared = 2; int i; - iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL ); + iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL, 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 ); + iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL, NULL ); + iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL, NULL ); Dss_ManPrintOne( p, iRes[0], NULL ); Dss_ManPrintOne( p, iRes[2], NULL ); @@ -1412,7 +1684,7 @@ void Dau_DsdTest444() Dss_ManPrintOne( p, iRes[2], pPermLits1 ); Dss_ManPrintOne( p, iRes[3], pPermLits2 ); - iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes ); + iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes, NULL ); for ( i = 0; i < 6; i++ ) pPermResInt[i] = pPermRes[i]; |