diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/base/abci/abcNpn.c | 2 | ||||
| -rw-r--r-- | src/misc/extra/extra.h | 1 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilFile.c | 18 | ||||
| -rw-r--r-- | src/misc/util/abc_global.h | 1 | ||||
| -rw-r--r-- | src/misc/util/utilTruth.h | 966 | ||||
| -rw-r--r-- | src/opt/dau/dauDsd.c | 247 |
7 files changed, 997 insertions, 242 deletions
@@ -1975,6 +1975,10 @@ SOURCE=.\src\opt\dau\dau.c # End Source File # Begin Source File +SOURCE=.\src\opt\dau\dauCanon.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\dau\dauCore.c # End Source File # Begin Source File diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c index 0e3f41f9..06732d2b 100644 --- a/src/base/abci/abcNpn.c +++ b/src/base/abci/abcNpn.c @@ -202,8 +202,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) { for ( i = 0; i < p->nFuncs; i++ ) { + extern void Abc_TtConfactorTest( word * pTruth, int nVars, int i ); if ( fVerbose ) printf( "%7d : ", i ); + Abc_TtConfactorTest( p->pFuncs[i], p->nVars, i ); if ( fVerbose ) Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" ); } diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index bb31dc1f..78a0fa99 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -119,6 +119,7 @@ extern int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int extern void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars ); extern void Extra_PrintHexadecimalString( char * pString, unsigned Sign[], int nVars ); extern void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars ); +extern void Extra_PrintHexReverse( FILE * pFile, unsigned * pTruth, int nVars ); extern void Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine ); /*=== extraUtilReader.c ========================================================*/ diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c index c0810e4b..721cbb12 100644 --- a/src/misc/extra/extraUtilFile.c +++ b/src/misc/extra/extraUtilFile.c @@ -561,6 +561,24 @@ void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars ) } // fprintf( pFile, "\n" ); } +void Extra_PrintHexReverse( FILE * pFile, unsigned * pTruth, int nVars ) +{ + int nMints, nDigits, Digit, k; + + // write the number into the file + fprintf( pFile, "0x" ); + nMints = (1 << nVars); + nDigits = nMints / 4; + for ( k = 0; k < nDigits; k++ ) + { + Digit = ((pTruth[k/8] >> (k * 4)) & 15); + if ( Digit < 10 ) + fprintf( pFile, "%d", Digit ); + else + fprintf( pFile, "%c", 'A' + Digit-10 ); + } +// fprintf( pFile, "\n" ); +} /**Function************************************************************* diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index fe3eda63..2b4e17a7 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -198,6 +198,7 @@ typedef unsigned __int64 ABC_UINT64_T; #endif /* defined(PLATFORM) */ typedef ABC_UINT64_T word; +typedef ABC_INT64_T iword; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 6bfb5699..30508498 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -44,6 +44,23 @@ static word s_Truths6[6] = { 0xFFFFFFFF00000000 }; +static word s_Truths6Neg[6] = { + 0x5555555555555555, + 0x3333333333333333, + 0x0F0F0F0F0F0F0F0F, + 0x00FF00FF00FF00FF, + 0x0000FFFF0000FFFF, + 0x00000000FFFFFFFF +}; + +static word s_CMasks6[5] = { + 0x1111111111111111, + 0x0303030303030303, + 0x000F000F000F000F, + 0x000000FF000000FF, + 0x000000000000FFFF +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -76,6 +93,12 @@ static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nV SeeAlso [] ***********************************************************************/ +static inline void Abc_TtNot( word * pOut, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~pOut[w]; +} static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl ) { int w; @@ -96,6 +119,368 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & pIn2[w]; } +static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( pIn1[w] != pIn2[w] ) + return 0; + return 1; +} +static inline int Abc_TtCompare( word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( pIn1[w] != pIn2[w] ) + return (pIn1[w] < pIn2[w]) ? -1 : 1; + return 0; +} +static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = nWords - 1; w >= 0; w-- ) + if ( pIn1[w] != pIn2[w] ) + return (pIn1[w] < pIn2[w]) ? -1 : 1; + return 0; +} + + +/**Function************************************************************* + + Synopsis [Compares Cof0 and Cof1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar ) +{ + if ( nWords == 1 ) + { + word Cof0 = pTruth[0] & s_Truths6Neg[iVar]; + word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + return 0; + } + if ( iVar <= 5 ) + { + word Cof0, Cof1; + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + { + Cof0 = pTruth[w] & s_Truths6Neg[iVar]; + Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + } + return 0; + } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + assert( nWords >= 2 ); + for ( ; pTruth < pLimit; pTruth += 2*iStep ) + for ( i = 0; i < iStep; i++ ) + if ( pTruth[i] != pTruth[i + iStep] ) + return pTruth[i] < pTruth[i + iStep] ? -1 : 1; + return 0; + } +} +static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar ) +{ + if ( nWords == 1 ) + { + word Cof0 = pTruth[0] & s_Truths6Neg[iVar]; + word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + return 0; + } + if ( iVar <= 5 ) + { + word Cof0, Cof1; + int w, shift = (1 << iVar); + for ( w = nWords - 1; w >= 0; w-- ) + { + Cof0 = pTruth[w] & s_Truths6Neg[iVar]; + Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + } + return 0; + } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + assert( nWords >= 2 ); + for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep ) + for ( i = iStep - 1; i >= 0; i-- ) + if ( pLimit[i] != pLimit[i + iStep] ) + return pLimit[i] < pLimit[i + iStep] ? -1 : 1; + return 0; + } +} + +/**Function************************************************************* + + Synopsis [Checks pairs of cofactors w.r.t. adjacent variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) +{ + assert( Num1 < Num2 && Num2 < 4 ); + if ( nWords == 1 ) + return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]); + if ( iVar <= 4 ) + { + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) ) + return 0; + return 1; + } + if ( iVar == 5 ) + { + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + assert( nWords >= 2 ); + for ( ; pTruthU < pLimitU; pTruthU += 4 ) + if ( pTruthU[Num2] != pTruthU[Num1] ) + return 0; + return 1; + } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + assert( nWords >= 4 ); + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) + if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] ) + return 0; + return 1; + } +} +static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) +{ + assert( Num1 < Num2 && Num2 < 4 ); + if ( nWords == 1 ) + { + word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]; + word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; + return 0; + } + if ( iVar <= 4 ) + { + word Cof1, Cof2; + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + { + Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; + Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; + } + return 0; + } + if ( iVar == 5 ) + { + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + assert( nWords >= 2 ); + for ( ; pTruthU < pLimitU; pTruthU += 4 ) + if ( pTruthU[Num1] != pTruthU[Num2] ) + return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1; + return 0; + } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + int Offset1 = Num1*iStep; + int Offset2 = Num2*iStep; + assert( nWords >= 4 ); + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) + if ( pTruth[i + Offset1] != pTruth[i + Offset2] ) + return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1; + return 0; + } +} +static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) +{ + assert( Num1 < Num2 && Num2 < 4 ); + if ( nWords == 1 ) + { + word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]; + word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; + return 0; + } + if ( iVar <= 4 ) + { + word Cof1, Cof2; + int w, shift = (1 << iVar); + for ( w = nWords - 1; w >= 0; w-- ) + { + Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; + Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; + } + return 0; + } + if ( iVar == 5 ) + { + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + assert( nWords >= 2 ); + for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 ) + if ( pLimitU[Num1] != pLimitU[Num2] ) + return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1; + return 0; + } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + int Offset1 = Num1*iStep; + int Offset2 = Num2*iStep; + assert( nWords >= 4 ); + for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep ) + for ( i = iStep - 1; i >= 0; i-- ) + if ( pLimit[i + Offset1] != pLimit[i + Offset2] ) + return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1; + return 0; + } +} + +/**Function************************************************************* + + Synopsis [Checks pairs of cofactors w.r.t. two variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int jVar, int Num1, int Num2 ) +{ + assert( Num1 < Num2 && Num2 < 4 ); + assert( iVar < jVar ); + if ( nWords == 1 ) + { + word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar]; + int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar); + int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar); + return ((pTruth[0] >> shift1) & Mask) == ((pTruth[0] >> shift2) & Mask); + } + if ( jVar <= 5 ) + { + word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar]; + int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar); + int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar); + int w; + for ( w = 0; w < nWords; w++ ) + if ( ((pTruth[w] >> shift1) & Mask) != ((pTruth[w] >> shift2) & Mask) ) + return 0; + return 1; + } + if ( iVar <= 5 && jVar > 5 ) + { + word * pLimit = pTruth + nWords; + int j, jStep = Abc_TtWordNum(jVar); + int shift1 = (Num1 & 1) * (1 << iVar); + int shift2 = (Num2 & 1) * (1 << iVar); + int Offset1 = (Num1 >> 1) * jStep; + int Offset2 = (Num2 >> 1) * jStep; + for ( ; pTruth < pLimit; pTruth += 2*jStep ) + for ( j = 0; j < jStep; j++ ) + if ( ((pTruth[j + Offset1] >> shift1) & s_Truths6Neg[iVar]) != ((pTruth[j + Offset2] >> shift2) & s_Truths6Neg[iVar]) ) + return 0; + return 1; + } + { + word * pLimit = pTruth + nWords; + int j, jStep = Abc_TtWordNum(jVar); + int i, iStep = Abc_TtWordNum(iVar); + int Offset1 = (Num1 >> 1) * jStep + (Num1 & 1) * iStep; + int Offset2 = (Num2 >> 1) * jStep + (Num2 & 1) * iStep; + for ( ; pTruth < pLimit; pTruth += 2*jStep ) + for ( i = 0; i < jStep; i += 2*iStep ) + for ( j = 0; j < iStep; j++ ) + if ( pTruth[Offset1 + i + j] != pTruth[Offset2 + i + j] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar ) +{ + if ( nWords == 1 ) + pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]); + else if ( iVar <= 5 ) + { + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]); + } + else // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + for ( ; pTruth < pLimit; pTruth += 2*iStep ) + for ( i = 0; i < iStep; i++ ) + pTruth[i + iStep] = pTruth[i]; + } +} +static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar ) +{ + if ( nWords == 1 ) + pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar)); + else if ( iVar <= 5 ) + { + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift); + } + else // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + for ( ; pTruth < pLimit; pTruth += 2*iStep ) + for ( i = 0; i < iStep; i++ ) + pTruth[i] = pTruth[i + iStep]; + } +} /**Function************************************************************* @@ -109,13 +494,238 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, SeeAlso [] ***********************************************************************/ +static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == 0; } +static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar]; } +static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0; } +static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar]; } +static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; } +static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; } + +static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( t[i] & s_Truths6Neg[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i] ) + return 0; + return 1; + } +} +static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( (t[i] & s_Truths6Neg[iVar]) != s_Truths6Neg[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( ~t[i] ) + return 0; + return 1; + } +} +static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( t[i] & s_Truths6[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i+Step] ) + return 0; + return 1; + } +} +static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( ~t[i+Step] ) + return 0; + return 1; + } +} +static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i, Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i] != ~t[i+Step] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtPrintDigit( int Digit ) +{ + assert( Digit >= 0 && Digit < 16 ); + if ( Digit < 10 ) + printf( "%d", Digit ); + else + printf( "%c", 'A' + Digit-10 ); +} +static inline void Abc_TtPrintHex( word * pTruth, int nVars ) +{ + word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars); + int k, nDigits = 1 << (nVars-2); + assert( nVars >= 2 ); + for ( pThis = pTruth; pThis < pLimit; pThis++ ) + for ( k = 0; k < 16; k++ ) + Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 ); + printf( "\n" ); +} +static inline void Abc_TtPrintHexRev( word * pTruth, int nVars ) +{ + word * pThis; + int k, nDigits = 1 << (nVars-2); + assert( nVars >= 2 ); + for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- ) + for ( k = 15; k >= 0; k-- ) + Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 ); + printf( "\n" ); +} +static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars ) +{ + word * pThis; + int k, nDigits = 1 << (nVars-2); + assert( nVars >= 2 ); + for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- ) + for ( k = 0; k < 16; k++ ) + Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 ); + printf( "\n" ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtPrintBinary( word * pTruth, int nVars ) +{ + word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars); + int k, nDigits = 1 << (nVars-2); + assert( nVars >= 2 ); + for ( pThis = pTruth; pThis < pLimit; pThis++ ) + for ( k = 0; k < 64; k++ ) + printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtSuppFindFirst( int Supp ) +{ + int i; + assert( Supp > 0 ); + for ( i = 0; i < 32; i++ ) + if ( Supp & (1 << i) ) + return i; + return -1; +} +static inline int Abc_TtSuppOnlyOne( int Supp ) +{ + assert( Supp > 0 ); + return (Supp & (Supp-1)) == 0; +} static inline int Abc_TtSuppIsMinBase( int Supp ) { + assert( Supp > 0 ); return (Supp & (Supp+1)) == 0; } static inline int Abc_Tt6HasVar( word t, int iVar ) { - return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]); + return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]); } static inline int Abc_TtHasVar( word * t, int nVars, int iVar ) { @@ -125,7 +735,7 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar ) { int i, Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) - if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) ) + if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) ) return 1; return 0; } @@ -188,6 +798,69 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize ) SeeAlso [] ***********************************************************************/ +static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar ) +{ + if ( nWords == 1 ) + pTruth[0] = ((pTruth[0] << (1 << iVar)) & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar)); + else if ( iVar <= 5 ) + { + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + pTruth[w] = ((pTruth[w] << shift) & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift); + } + else // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + for ( ; pTruth < pLimit; pTruth += 2*iStep ) + for ( i = 0; i < iStep; i++ ) + ABC_SWAP( word, pTruth[i], pTruth[i + iStep] ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar ) +{ + static word PMasks[5][3] = { + { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, + { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, + { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, + { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, + { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } + }; + if ( iVar < 5 ) + { + int i, Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + pTruth[i] = (pTruth[i] & PMasks[iVar][0]) | ((pTruth[i] & PMasks[iVar][1]) << Shift) | ((pTruth[i] & PMasks[iVar][2]) >> Shift); + } + else if ( iVar == 5 ) + { + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + for ( ; pTruthU < pLimitU; pTruthU += 4 ) + ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] ); + } + else // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) + ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] ); + } +} + static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ) { static word PPMasks[5][6][3] = { @@ -270,106 +943,239 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar } else { - word temp, * pLimit = pTruth + Abc_TtWordNum(nVars); + word * pLimit = pTruth + Abc_TtWordNum(nVars); int i, iStep = Abc_TtWordNum(iVar); int j, jStep = Abc_TtWordNum(jVar); for ( ; pTruth < pLimit; pTruth += 2*jStep ) for ( i = 0; i < jStep; i += 2*iStep ) for ( j = 0; j < iStep; j++ ) - { - temp = pTruth[iStep + i + j]; - pTruth[iStep + i + j] = pTruth[jStep + i + j]; - pTruth[jStep + i + j] = temp; - } + ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] ); } } } -static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar ) +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCountOnesSlow( word t ) { - static word PPMasks[6][6] = { - { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA }, - { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC }, - { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 }, - { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 }, - { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 }, - { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 } - }; + t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555); + t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333); + t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F); + t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF); + t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF); + return (t & 0x00000000FFFFFFFF) + (t>>32); +} +static inline int Abc_TtCountOnes( word x ) +{ + x = x - ((x >> 1) & 0x5555555555555555); + x = (x & 0x3333333333333333) + ((x >> 2) & 0x3333333333333333); + x = (x + (x >> 4)) & 0x0F0F0F0F0F0F0F0F; + x = x + (x >> 8); + x = x + (x >> 16); + x = x + (x >> 32); + return (int)(x & 0xFF); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars ) +{ + int nWords = Abc_TtWordNum( nVars ); + int k, Counter = 0; + for ( k = 0; k < nWords; k++ ) + Counter += Abc_TtCountOnes( pTruth[k] ); + return Counter; +} +static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore ) +{ + int i, k, Counter, nWords; + memset( pStore, 0, sizeof(int) * nVars ); if ( nVars <= 6 ) { - int shift; - word low2High, high2Low; - assert( iVar <= 5 && jVar <= 5 && iVar < jVar ); - shift = (1 << jVar) - (1 << iVar); - low2High = (pTruth[0] & PPMasks[iVar][jVar - 1] ) << shift; - pTruth[0] &= ~PPMasks[iVar][jVar - 1]; - high2Low = (pTruth[0] & (PPMasks[iVar][jVar - 1] << shift )) >> shift; - pTruth[0] &= ~(PPMasks[iVar][jVar - 1] << shift); - pTruth[0] |= low2High | high2Low; + for ( i = 0; i < nVars; i++ ) + pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] ); + return; } - else + assert( nVars > 6 ); + nWords = Abc_TtWordNum( nVars ); + for ( k = 0; k < nWords; k++ ) { - word low2High, high2Low, temp; - int nWords = Abc_TtWordNum(nVars); - int shift, step, iStep, jStep; - int w = 0, i = 0, j = 0; - if ( iVar == jVar ) - return; - if ( jVar < iVar ) - ABC_SWAP( int, iVar, jVar ); - if ( iVar <= 5 && jVar <= 5 ) - { - shift = (1 << jVar) - (1 << iVar); - for ( w = 0; w < nWords; w++ ) - { - low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift; - pTruth[w] &= ~PPMasks[iVar][jVar - 1]; - high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift; - pTruth[w] &= ~(PPMasks[iVar][jVar - 1] << shift); - pTruth[w] |= low2High | high2Low; - } - } - else if ( iVar <= 5 && jVar > 5 ) + // count 1's for the first six variables + for ( i = 0; i < 6; i++ ) + pStore[i] += Abc_TtCountOnes( (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i)) ); + // count 1's for all other variables + Counter = Abc_TtCountOnes( pTruth[k] ); + for ( i = 6; i < nVars; i++ ) + if ( (k & (1 << (i-6))) == 0 ) + pStore[i] += Counter; + // count 1's for all other variables + Counter = Abc_TtCountOnes( pTruth[++k] ); + for ( i = 6; i < nVars; i++ ) + if ( (k & (1 << (i-6))) == 0 ) + pStore[i] += Counter; + } +} +static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore ) +{ + static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 + }; + int i, k, nBytes; + unsigned char * pTruthC = (unsigned char *)pTruth; + nBytes = 8 * Abc_TtWordNum( nVars ); + memset( pStore, 0, sizeof(int) * nVars ); + for ( k = 0; k < nBytes; k++ ) + { + pStore[0] += bit_count[ pTruthC[k] & 0x55 ]; + pStore[1] += bit_count[ pTruthC[k] & 0x33 ]; + pStore[2] += bit_count[ pTruthC[k] & 0x0F ]; + for ( i = 3; i < nVars; i++ ) + if ( (k & (1 << (i-3))) == 0 ) + pStore[i] += bit_count[pTruthC[k]]; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm ) +{ + int pStore[16]; + int nWords = Abc_TtWordNum( nVars ); + int i, Temp, fChange, nOnes; + unsigned uCanonPhase = 0; + assert( nVars <= 16 ); + // normalize polarity + nOnes = Abc_TtCountOnesInTruth( pTruth, nVars ); + if ( nOnes > nWords * 32 ) + { + Abc_TtNot( pTruth, nWords ); + nOnes = nWords*64 - nOnes; + uCanonPhase |= (1 << nVars); + } + // normalize phase + Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); + for ( i = 0; i < nVars; i++ ) + { + if ( pStore[i] >= nOnes - pStore[i] ) + continue; + Abc_TtFlip( pTruth, nWords, i ); + uCanonPhase |= (1 << i); + pStore[i] = nOnes - pStore[i]; + } + + do { + fChange = 0; + for ( i = 0; i < nVars-1; i++ ) { - step = Abc_TtWordNum(jVar + 1)/2; - shift = 1 << iVar; - for ( w = 0; w < nWords; w += 2*step ) + if ( pStore[i] <= pStore[i+1] ) + continue; + + Temp = pCanonPerm[i]; + pCanonPerm[i] = pCanonPerm[i+1]; + pCanonPerm[i+1] = Temp; + + Temp = pStore[i]; + pStore[i] = pStore[i+1]; + pStore[i+1] = Temp; + + if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) ) { - for (j = 0; j < step; j++) - { - low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift; - pTruth[w + j] &= ~PPMasks[iVar][5]; - high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift; - pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift); - pTruth[w + j] |= high2Low; - pTruth[w + step + j] |= low2High; - } + uCanonPhase ^= (1 << i); + uCanonPhase ^= (1 << (i+1)); } + Abc_TtSwapAdjacent( pTruth, nWords, i ); + fChange = 1; } - else - { - iStep = Abc_TtWordNum(iVar + 1)/2; - jStep = Abc_TtWordNum(jVar + 1)/2; - for (w = 0; w < nWords; w += 2*jStep) - { - for (i = 0; i < jStep; i += 2*iStep) - { - for (j = 0; j < iStep; j++) - { - temp = pTruth[w + iStep + i + j]; - pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j]; - pTruth[w + jStep + i + j] = temp; - } - } - } - } - } + } while ( fChange ); + return uCanonPhase; } /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtReverseVars( word * pTruth, int nVars ) +{ + int k; + for ( k = 0; k < nVars/2 ; k++ ) + Abc_TtSwapVars( pTruth, nVars, k, nVars - 1 - k ); +} +static inline void Abc_TtReverseBits( word * pTruth, int nVars ) +{ + static unsigned char pMirror[256] = { + 0, 128, 64, 192, 32, 160, 96, 224, 16, 144, 80, 208, 48, 176, 112, 240, + 8, 136, 72, 200, 40, 168, 104, 232, 24, 152, 88, 216, 56, 184, 120, 248, + 4, 132, 68, 196, 36, 164, 100, 228, 20, 148, 84, 212, 52, 180, 116, 244, + 12, 140, 76, 204, 44, 172, 108, 236, 28, 156, 92, 220, 60, 188, 124, 252, + 2, 130, 66, 194, 34, 162, 98, 226, 18, 146, 82, 210, 50, 178, 114, 242, + 10, 138, 74, 202, 42, 170, 106, 234, 26, 154, 90, 218, 58, 186, 122, 250, + 6, 134, 70, 198, 38, 166, 102, 230, 22, 150, 86, 214, 54, 182, 118, 246, + 14, 142, 78, 206, 46, 174, 110, 238, 30, 158, 94, 222, 62, 190, 126, 254, + 1, 129, 65, 193, 33, 161, 97, 225, 17, 145, 81, 209, 49, 177, 113, 241, + 9, 137, 73, 201, 41, 169, 105, 233, 25, 153, 89, 217, 57, 185, 121, 249, + 5, 133, 69, 197, 37, 165, 101, 229, 21, 149, 85, 213, 53, 181, 117, 245, + 13, 141, 77, 205, 45, 173, 109, 237, 29, 157, 93, 221, 61, 189, 125, 253, + 3, 131, 67, 195, 35, 163, 99, 227, 19, 147, 83, 211, 51, 179, 115, 243, + 11, 139, 75, 203, 43, 171, 107, 235, 27, 155, 91, 219, 59, 187, 123, 251, + 7, 135, 71, 199, 39, 167, 103, 231, 23, 151, 87, 215, 55, 183, 119, 247, + 15, 143, 79, 207, 47, 175, 111, 239, 31, 159, 95, 223, 63, 191, 127, 255 + }; + unsigned char Temp, * pTruthC = (unsigned char *)pTruth; + int i, nBytes = (nVars > 6) ? (1 << (nVars - 3)) : 8; + for ( i = 0; i < nBytes/2; i++ ) + { + Temp = pMirror[pTruthC[i]]; + pTruthC[i] = pMirror[pTruthC[nBytes-1-i]]; + pTruthC[nBytes-1-i] = Temp; + } +} + + +/**Function************************************************************* + Synopsis [Stretch truthtable to have more input variables.] Description [] @@ -379,7 +1185,7 @@ static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar SeeAlso [] ***********************************************************************/ -static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB ) +static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB ) { int w, i, step, nWords; if ( nVarS == nVarB ) @@ -394,7 +1200,7 @@ static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB ) for ( i = 0; i < step; i++ ) pInOut[w + i] = pInOut[i]; } -static void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB ) +static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB ) { int w, i, step, nWords; if ( nVarS == nVarB ) diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index f6367304..d319e62d 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -478,163 +478,6 @@ void Dau_DsdTestOne( word t, int i ) SeeAlso [] ***********************************************************************/ -static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; } -static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; } - -static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar ) -{ - if ( iVar < 6 ) - { - int i; - for ( i = 0; i < nWords; i++ ) - if ( t[i] & ~s_Truths6[iVar] ) - return 0; - return 1; - } - else - { - int i, Step = (1 << (iVar - 6)); - word * tLimit = t + nWords; - for ( ; t < tLimit; t += 2*Step ) - for ( i = 0; i < Step; i++ ) - if ( t[i] ) - return 0; - return 1; - } -} -static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar ) -{ - if ( iVar < 6 ) - { - int i; - for ( i = 0; i < nWords; i++ ) - if ( (t[i] & ~s_Truths6[iVar]) != ~s_Truths6[iVar] ) - return 0; - return 1; - } - else - { - int i, Step = (1 << (iVar - 6)); - word * tLimit = t + nWords; - for ( ; t < tLimit; t += 2*Step ) - for ( i = 0; i < Step; i++ ) - if ( t[i] != ~(word)0 ) - return 0; - return 1; - } -} -static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar ) -{ - if ( iVar < 6 ) - { - int i; - for ( i = 0; i < nWords; i++ ) - if ( t[i] & s_Truths6[iVar] ) - return 0; - return 1; - } - else - { - int i, Step = (1 << (iVar - 6)); - word * tLimit = t + nWords; - for ( ; t < tLimit; t += 2*Step ) - for ( i = 0; i < Step; i++ ) - if ( t[i+Step] ) - return 0; - return 1; - } -} -static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar ) -{ - if ( iVar < 6 ) - { - int i; - for ( i = 0; i < nWords; i++ ) - if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] ) - return 0; - return 1; - } - else - { - int i, Step = (1 << (iVar - 6)); - word * tLimit = t + nWords; - for ( ; t < tLimit; t += 2*Step ) - for ( i = 0; i < Step; i++ ) - if ( t[i+Step] != ~(word)0 ) - return 0; - return 1; - } -} -static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) -{ - if ( iVar < 6 ) - { - int i, Shift = (1 << iVar); - for ( i = 0; i < nWords; i++ ) - if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) ) - return 0; - return 1; - } - else - { - int i, Step = (1 << (iVar - 6)); - word * tLimit = t + nWords; - for ( ; t < tLimit; t += 2*Step ) - for ( i = 0; i < Step; i++ ) - if ( t[i] != ~t[i+Step] ) - return 0; - return 1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Abc_TtCof0HasVar( word * t, int nWords, int iVarI, int iVarJ ) -{ - assert( iVarI > iVarJ ); - if ( iVarI < 6 ) - { - int i, Shift = (1 << iVarJ); - for ( i = 0; i < nWords; i++ ) - if ( (((t[i] & ~s_Truths6[iVarI]) << Shift) & s_Truths6[iVarJ]) != ((t[i] & ~s_Truths6[iVarI]) & s_Truths6[iVarJ]) ) - return 0; - return 1; - } - else if ( iVarI == 6 ) - { - } - else - { - int i, Step = (1 << (iVarJ - 6)); - word * tLimit = t + nWords; - for ( ; t < tLimit; t += 2*Step ) - for ( i = 0; i < Step; i++ ) - if ( t[i] != t[i+Step] ) - return 0; - return 1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Dau_DsdMinimize( word * p, int * pVars, int nVars ) { int i, k; @@ -683,16 +526,18 @@ int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, ***********************************************************************/ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func ) { - int v, nWords = Abc_TtWordNum( nVars ); + int v, u, nWords = Abc_TtWordNum( nVars ); nVars = Dau_DsdMinimize( p, pVars, nVars ); if ( nVars <= 6 ) return Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func ); + // consider negative cofactors if ( p[0] & 1 ) { // check for !(ax) for ( v = 0; v < nVars; v++ ) - if ( Abc_TtCof0IsConst0( p, nWords, v ) ) + if ( Abc_TtCof0IsConst1( p, nWords, v ) ) { + pBuffer[Pos++] = '!'; pBuffer[Pos++] = '('; pBuffer[Pos++] = 'a' + pVars[v]; Abc_TtSwapVars( p, nVars, v, nVars - 1 ); @@ -706,9 +551,8 @@ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, c { // check for ax for ( v = 0; v < nVars; v++ ) - if ( Abc_TtCof0IsConst1( p, nWords, v ) ) + if ( Abc_TtCof0IsConst0( p, nWords, v ) ) { - pBuffer[Pos++] = '!'; pBuffer[Pos++] = '('; pBuffer[Pos++] = 'a' + pVars[v]; Abc_TtSwapVars( p, nVars, v, nVars - 1 ); @@ -718,6 +562,7 @@ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, c return Pos; } } + // consider positive cofactors if ( (p[nWords-1] >> 63) & 1 ) { // check for !(!ax) @@ -764,7 +609,85 @@ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, c return Pos; } - return 0; + // consider two-variable cofactors + for ( v = nVars - 1; v > 0; v-- ) + { + unsigned uSupp0 = 0, uSupp1 = 0; + for ( u = v - 1; u >= 0; u-- ) + { + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 1 ) ) + { + uSupp0 |= (1 << u); + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 2, 3 ) ) + { + uSupp1 |= (1 << u); + // check XOR decomposition + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 3 ) && Abc_TtCheckEqualCofs( p, nWords, u, v, 1, 2 ) ) + { + // perform XOR (u, v) + return Pos; + } + } + else + { + // F(v=0) does not depend on u; F(v=1) depends on u + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 2 ) ) + { + // perform AND (u, v) + return Pos; + } + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 3 ) ) + { + // perform AND (u, v) + return Pos; + } + } + } + else if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 2, 3 ) ) + { + uSupp1 |= (1 << u); + // F(v=0) depends on u; F(v=1) does not depend on u + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 2 ) ) + { + // perform AND (u, v) + return Pos; + } + if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 1, 2 ) ) + { + // perform AND (u, v) + return Pos; + } + } + else assert( 0 ); + } + // check MUX decomposition w.r.t. u + if ( (uSupp0 & uSupp1) == 0 ) + { + // perform MUX( v, F(v=1), F(v=0) ) + } + // check MUX decomposition w.r.t. u + if ( Abc_TtSuppOnlyOne( uSupp0 & ~uSupp1 ) && Abc_TtSuppOnlyOne( ~uSupp0 & uSupp1 ) ) + { + // check MUX + int iVar0 = Abc_TtSuppFindFirst( uSupp0 ); + int iVar1 = Abc_TtSuppFindFirst( uSupp1 ); + int fEqual0, fEqual1; + + if ( iVar0 > iVar1 ) + ABC_SWAP( int, iVar0, iVar1 ); + + // check existence conditions + assert( iVar0 < iVar1 ); + fEqual0 = Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 1, 3 ); + fEqual1 = Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 1, 2 ); + if ( fEqual0 || fEqual1 ) + { + // perform MUX( v, F(v=1), F(v=0) ) + return Pos; + } + } + } + return Pos; } |