diff options
| -rw-r--r-- | src/misc/util/utilTruth.h | 52 | ||||
| -rw-r--r-- | src/opt/dau/dau.h | 3 | ||||
| -rw-r--r-- | src/opt/dau/dauDsd.c | 659 |
3 files changed, 356 insertions, 358 deletions
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index f7f250ce..9281d6f8 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -142,6 +142,22 @@ 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 void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) +{ + int w; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] ^ ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] ^ pIn2[w]; +} +static inline void Abc_TtMux( word * pOut, word * pCtrl, word * pIn1, word * pIn0, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pOut[w] = (pCtrl[w] & pIn1[w]) | (~pCtrl[w] & pIn0[w]); +} static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords ) { int w; @@ -182,6 +198,42 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords ) return 0; return 1; } +static inline void Abc_TtConst0( word * pIn1, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pIn1[w] = 0; +} +static inline void Abc_TtConst1( word * pIn1, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pIn1[w] = ~(word)0; +} + +/**Function************************************************************* + + Synopsis [Compute elementary truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtElemInit( word ** pTtElems, int nVars ) +{ + int i, k, nWords = Abc_TtWordNum( nVars ); + for ( i = 0; i < nVars; i++ ) + if ( i < 6 ) + for ( k = 0; k < nWords; k++ ) + pTtElems[i][k] = s_Truths6[i]; + else + for ( k = 0; k < nWords; k++ ) + pTtElems[i][k] = (k & (1 << (i-6))) ? ~(word)0 : 0; +} + /**Function************************************************************* diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index 1db02a0d..78b1535c 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -55,7 +55,10 @@ ABC_NAMESPACE_HEADER_START /*=== dauCanon.c ==========================================================*/ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ); +/*=== dauDsd.c ==========================================================*/ extern char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ); +extern word * Dau_DsdToTruth( char * p, int nVars ); + ABC_NAMESPACE_HEADER_END diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index 8895b97d..32c2dab1 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -18,6 +18,7 @@ ***********************************************************************/ +#include "dau.h" #include "dauInt.h" #include "misc/util/utilTruth.h" @@ -38,6 +39,7 @@ ABC_NAMESPACE_IMPL_START (ab) = a and b; [ab] = a xor b; <abc> = ITE( a, b, c ) + FUNCTION{abc} = FUNCTION( a, b, c ) */ @@ -47,7 +49,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [Computes truth table for the DSD formula.] + Synopsis [DSD formula manipulation.] Description [] @@ -68,6 +70,7 @@ int * Dau_DsdComputeMatches( char * p ) pNested[nNested++] = v; else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' ) pMatches[pNested[--nNested]] = v; + assert( nNested < DAU_MAX_VAR ); } assert( nNested == 0 ); /* @@ -96,7 +99,58 @@ char * Dau_DsdFindMatch( char * p ) } return NULL; } -word Dau_DsdTruthCompose_rec( word Func, word * pFanins, int nVars ) +static inline void Dau_DsdCleanBraces( char * p ) +{ + char * q, Last = -1; + int i; + for ( i = 0; p[i]; i++ ) + { + if ( p[i] == '(' || p[i] == '[' || p[i] == '<' ) + { + if ( p[i] != '<' && p[i] == Last && i > 0 && p[i-1] != '!' ) + { + q = Dau_DsdFindMatch( p + i ); + assert( (p[i] == '(') == (*q == ')') ); + assert( (p[i] == '[') == (*q == ']') ); + p[i] = *q = 'x'; + } + else + Last = p[i]; + } + else if ( p[i] == ')' || p[i] == ']' || p[i] == '>' ) + Last = -1; + } +/* + if ( p[0] == '(' ) + { + assert( p[i-1] == ')' ); + p[0] = p[i-1] = 'x'; + } + else if ( p[0] == '[' ) + { + assert( p[i-1] == ']' ); + p[0] = p[i-1] = 'x'; + } +*/ + for ( q = p; *p; p++ ) + if ( *p != 'x' ) + *q++ = *p; + *q = 0; +} + + +/**Function************************************************************* + + Synopsis [Computes truth table for the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +word Dau_Dsd6TruthCompose_rec( word Func, word * pFanins, int nVars ) { word t0, t1; if ( Func == 0 ) @@ -105,72 +159,77 @@ word Dau_DsdTruthCompose_rec( word Func, word * pFanins, int nVars ) return ~(word)0; assert( nVars > 0 ); if ( --nVars == 0 ) + { + assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] ); return (Func == s_Truths6[0]) ? pFanins[0] : ~pFanins[0]; + } if ( !Abc_Tt6HasVar(Func, nVars) ) - return Dau_DsdTruthCompose_rec( Func, pFanins, nVars ); - t0 = Dau_DsdTruthCompose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars ); - t1 = Dau_DsdTruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars ); + return Dau_Dsd6TruthCompose_rec( Func, pFanins, nVars ); + t0 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars ); + t1 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars ); return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1); } -word Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches ) +word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) { int fCompl = 0; if ( **p == '!' ) (*p)++, fCompl = 1; - if ( **p >= 'a' && **p <= 'f' ) + if ( **p >= 'a' && **p <= 'f' ) // var { assert( **p - 'a' >= 0 && **p - 'a' < 6 ); return fCompl ? ~s_Truths6[**p - 'a'] : s_Truths6[**p - 'a']; } - if ( **p == '(' || **p == '[' || **p == '<' ) + if ( **p == '(' ) // and/or { + char * q = pStr + pMatches[ *p - pStr ]; + word Res = ~(word)0; + assert( **p == '(' && *q == ')' ); + for ( (*p)++; *p < q; (*p)++ ) + Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + assert( *p == q ); + return fCompl ? ~Res : Res; + } + if ( **p == '[' ) // xor + { + char * q = pStr + pMatches[ *p - pStr ]; word Res = 0; -// char * q2 = Dau_DsdFindMatch( *p ); + assert( **p == '[' && *q == ']' ); + for ( (*p)++; *p < q; (*p)++ ) + Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + assert( *p == q ); + return fCompl ? ~Res : Res; + } + if ( **p == '<' ) // mux + { char * q = pStr + pMatches[ *p - pStr ]; - assert( (**p == '(') == (*q == ')') ); - assert( (**p == '[') == (*q == ']') ); - assert( (**p == '<') == (*q == '>') ); - if ( **p == '(' ) // and/or - { - Res = ~(word)0; - for ( (*p)++; *p < q; (*p)++ ) - Res &= Dau_DsdToTruth_rec( pStr, p, pMatches ); - } - else if ( **p == '[' ) // xor - { - Res = 0; - for ( (*p)++; *p < q; (*p)++ ) - Res ^= Dau_DsdToTruth_rec( pStr, p, pMatches ); - } - else if ( **p == '<' ) // mux - { - word Temp[3], * pTemp = Temp; - for ( (*p)++; *p < q; (*p)++ ) - *pTemp++ = Dau_DsdToTruth_rec( pStr, p, pMatches ); - assert( pTemp == Temp + 3 ); - Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]); - } - else assert( 0 ); + word Temp[3], * pTemp = Temp, Res; + assert( **p == '<' && *q == '>' ); + for ( (*p)++; *p < q; (*p)++ ) + *pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + assert( pTemp == Temp + 3 ); assert( *p == q ); + Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]); return fCompl ? ~Res : Res; } if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) { - word Func, Fanins[6]; + word Func, Fanins[6], Res; char * q; int i, nVars = Abc_TtReadHex( &Func, *p ); *p += Abc_TtHexDigitNum( nVars ); q = pStr + pMatches[ *p - pStr ]; assert( **p == '{' && *q == '}' ); for ( i = 0, (*p)++; *p < q; (*p)++, i++ ) - Fanins[i] = Dau_DsdToTruth_rec( pStr, p, pMatches ); + Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); assert( i == nVars ); - return Dau_DsdTruthCompose_rec( Func, Fanins, nVars ); + assert( *p == q ); + Res = Dau_Dsd6TruthCompose_rec( Func, Fanins, nVars ); + return fCompl ? ~Res : Res; } assert( 0 ); return 0; } -word Dau_DsdToTruth( char * p ) +word Dau_Dsd6ToTruth( char * p ) { word Res; if ( *p == '0' && *(p+1) == 0 ) @@ -178,13 +237,191 @@ word Dau_DsdToTruth( char * p ) else if ( *p == '1' && *(p+1) == 0 ) Res = ~(word)0; else - Res = Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p) ); + Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p) ); assert( *++p == 0 ); return Res; } /**Function************************************************************* + Synopsis [Computes truth table for the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_DsdTruth6Compose_rec( word Func, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars ) +{ + if ( Func == 0 ) + { + Abc_TtConst0( pRes, Abc_TtWordNum(nVars) ); + return; + } + if ( Func == ~(word)0 ) + { + Abc_TtConst1( pRes, Abc_TtWordNum(nVars) ); + return; + } + assert( nVars > 0 ); + if ( --nVars == 0 ) + { + assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] ); + Abc_TtCopy( pRes, pFanins[0], Abc_TtWordNum(nVars), Func == s_Truths6Neg[0] ); + return; + } + if ( !Abc_Tt6HasVar(Func, nVars) ) + { + Dau_DsdTruth6Compose_rec( Func, pFanins, pRes, nVars ); + return; + } + { + word pTtTemp[2][DAU_MAX_WORD]; + Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, pTtTemp[0], nVars ); + Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, pTtTemp[1], nVars ); + Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], Abc_TtWordNum(nVars) ); + return; + } +} +void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars ) +{ + int nWords; + if ( nVars <= 6 ) + { + Dau_DsdTruth6Compose_rec( pFunc[0], pFanins, pRes, nVars ); + return; + } + nWords = Abc_TtWordNum( nVars ); + if ( Abc_TtIsConst0(pFunc, nWords) ) + { + Abc_TtConst0( pRes, nWords ); + return; + } + if ( Abc_TtIsConst1(pFunc, nWords) ) + { + Abc_TtConst1( pRes, nWords ); + return; + } + if ( !Abc_TtHasVar( pFunc, nVars, nVars-1 ) ) + { + Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVars-1 ); + return; + } + { + word pCofTemp[2][DAU_MAX_WORD]; + word pTtTemp[2][DAU_MAX_WORD]; + nVars--; + Abc_TtCopy( pCofTemp[0], pFunc, nWords, 0 ); + Abc_TtCopy( pCofTemp[1], pFunc, nWords, 0 ); + Abc_TtCofactor0( pCofTemp[0], nWords, nVars ); + Abc_TtCofactor1( pCofTemp[1], nWords, nVars ); + Dau_DsdTruthCompose_rec( pCofTemp[0], pFanins, pTtTemp[0], nVars ); + Dau_DsdTruthCompose_rec( pCofTemp[1], pFanins, pTtTemp[1], nVars ); + Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWords ); + return; + } +} +void Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches, word ** pTtElems, word * pRes, int nVars ) +{ + int nWords = Abc_TtWordNum( nVars ); + int fCompl = 0; + if ( **p == '!' ) + (*p)++, fCompl = 1; + if ( **p >= 'a' && **p <= 'f' ) // var + { + assert( **p - 'a' >= 0 && **p - 'a' < 6 ); + Abc_TtCopy( pRes, pTtElems[**p - 'a'], nWords, fCompl ); + return; + } + if ( **p == '(' ) // and/or + { + char * q = pStr + pMatches[ *p - pStr ]; + word pTtTemp[DAU_MAX_WORD]; + assert( **p == '(' && *q == ')' ); + Abc_TtConst1( pRes, nWords ); + for ( (*p)++; *p < q; (*p)++ ) + { + Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp, nVars ); + Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 ); + } + assert( *p == q ); + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; + } + if ( **p == '[' ) // xor + { + char * q = pStr + pMatches[ *p - pStr ]; + word pTtTemp[DAU_MAX_WORD]; + assert( **p == '[' && *q == ']' ); + Abc_TtConst0( pRes, nWords ); + for ( (*p)++; *p < q; (*p)++ ) + { + Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp, nVars ); + Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 ); + } + assert( *p == q ); + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; + } + if ( **p == '<' ) // mux + { + char * q = pStr + pMatches[ *p - pStr ]; + word pTtTemp[3][DAU_MAX_WORD]; + int i; + assert( **p == '<' && *q == '>' ); + for ( i = 0, (*p)++; *p < q; (*p)++, i++ ) + Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp[i], nVars ); + assert( i == 3 ); + Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords ); + assert( *p == q ); + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; + } + if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + { + word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], pFunc[DAU_MAX_WORD]; + char * q; + int i, nVars = Abc_TtReadHex( pFunc, *p ); + *p += Abc_TtHexDigitNum( nVars ); + q = pStr + pMatches[ *p - pStr ]; + assert( **p == '{' && *q == '}' ); + for ( i = 0, (*p)++; *p < q; (*p)++, i++ ) + Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pFanins[i], nVars ); + assert( i == nVars ); + assert( *p == q ); + Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nWords ); + if ( fCompl ) Abc_TtNot( pRes, nWords ); + return; + } + assert( 0 ); +} +word * Dau_DsdToTruth( char * p, int nVars ) +{ + static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR] = {NULL}; + int v, nWords = Abc_TtWordNum( nVars ); + word * pRes; + if ( pTtElems[0] == NULL ) + { + for ( v = 0; v < DAU_MAX_VAR; v++ ) + pTtElems[v] = TtElems[v]; + Abc_TtElemInit( pTtElems, DAU_MAX_VAR ); + } + pRes = pTtElems[DAU_MAX_VAR]; + if ( p[0] == '0' && p[1] == 0 ) + Abc_TtConst0( pRes, nWords ); + else if ( p[0] == '1' && p[1] == 0 ) + Abc_TtConst1( pRes, nWords ); + else + Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p), pTtElems, pRes, nVars ); + assert( *++p == 0 ); + return pRes; +} + + +/**Function************************************************************* + Synopsis [] Description [] @@ -198,7 +435,7 @@ void Dau_DsdTest2() { // char * p = Abc_UtilStrsav( "!(ab!(de[cf]))" ); // char * p = Abc_UtilStrsav( "!(a![d<ecf>]b)" ); -// word t = Dau_DsdToTruth( p ); +// word t = Dau_Dsd6ToTruth( p ); } @@ -359,7 +596,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest ); return Pos; } - } + } // find best variable for MUX decomposition vBest = -1; CountBest = 10; @@ -385,46 +622,6 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars pBuffer[Pos++] = '>'; return Pos; } - -static inline void Dau_DsdCleanBraces( char * p ) -{ - char * q, Last = -1; - int i; - for ( i = 0; p[i]; i++ ) - { - if ( p[i] == '(' || p[i] == '[' || p[i] == '<' ) - { - if ( p[i] != '<' && p[i] == Last && i > 0 && p[i-1] != '!' ) - { - q = Dau_DsdFindMatch( p + i ); - assert( (p[i] == '(') == (*q == ')') ); - assert( (p[i] == '[') == (*q == ']') ); - p[i] = *q = 'x'; - } - else - Last = p[i]; - } - else if ( p[i] == ')' || p[i] == ']' || p[i] == '>' ) - Last = -1; - } -/* - if ( p[0] == '(' ) - { - assert( p[i-1] == ')' ); - p[0] = p[i-1] = 'x'; - } - else if ( p[0] == '[' ) - { - assert( p[i-1] == ']' ); - p[0] = p[i-1] = 'x'; - } -*/ - for ( q = p; *p; p++ ) - if ( *p != 'x' ) - *q++ = *p; - *q = 0; -} - char * Dau_DsdPerform( word t ) { static char pBuffer[DAU_MAX_STR+20]; @@ -470,16 +667,18 @@ void Dau_DsdTest3() // word t = 0x05050500f5f5f5f3; word t = 0x9ef7a8d9c7193a0f; char * p = Dau_DsdPerform( t ); - word t2 = Dau_DsdToTruth( p ); + word t2 = Dau_Dsd6ToTruth( p ); if ( t != t2 ) printf( "Verification failed.\n" ); } void Dau_DsdTestOne( word t, int i ) { + int nSizeNonDec; word t2; - char * p = Dau_DsdPerform( t ); +// char * p = Dau_DsdPerform( t ); + char * p = Dau_DsdDecompose( &t, 6, &nSizeNonDec ); return; - t2 = Dau_DsdToTruth( p ); + t2 = Dau_Dsd6ToTruth( p ); if ( t != t2 ) { printf( "Verification failed. " ); @@ -503,267 +702,6 @@ void Dau_DsdTestOne( word t, int i ) /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dau_DsdMinimize( word * p, int * pVars, int nVars ) -{ - int i, k; - assert( nVars > 6 ); - for ( i = k = nVars - 1; i >= 0; i-- ) - { - if ( Abc_TtHasVar( p, nVars, i ) ) - continue; - if ( i < k ) - { - pVars[i] = pVars[k]; - Abc_TtSwapVars( p, nVars, i, k ); - } - k--; - nVars--; - } - return nVars; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func ) -{ - return 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func ) -{ - 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_TtCof0IsConst1( p, nWords, v ) ) - { - pBuffer[Pos++] = '!'; - pBuffer[Pos++] = '('; - pBuffer[Pos++] = 'a' + pVars[v]; - Abc_TtSwapVars( p, nVars, v, nVars - 1 ); - pVars[v] = pVars[nVars-1]; - Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func ); - pBuffer[Pos++] = ')'; - return Pos; - } - } - else - { - // check for ax - for ( v = 0; v < nVars; v++ ) - if ( Abc_TtCof0IsConst0( p, nWords, v ) ) - { - pBuffer[Pos++] = '('; - pBuffer[Pos++] = 'a' + pVars[v]; - Abc_TtSwapVars( p, nVars, v, nVars - 1 ); - pVars[v] = pVars[nVars-1]; - Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func ); - pBuffer[Pos++] = ')'; - return Pos; - } - } - // consider positive cofactors - if ( (p[nWords-1] >> 63) & 1 ) - { - // check for !(!ax) - for ( v = 0; v < nVars; v++ ) - if ( Abc_TtCof0IsConst1( p, nWords, v ) ) - { - pBuffer[Pos++] = '!'; - pBuffer[Pos++] = '('; - pBuffer[Pos++] = '!'; - pBuffer[Pos++] = 'a' + pVars[v]; - Abc_TtSwapVars( p, nVars, v, nVars - 1 ); - pVars[v] = pVars[nVars-1]; - Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func ); - pBuffer[Pos++] = ')'; - return Pos; - } - } - else - { - // check for !ax - for ( v = 0; v < nVars; v++ ) - if ( Abc_TtCof1IsConst0( p, nWords, v ) ) - { - pBuffer[Pos++] = '('; - pBuffer[Pos++] = '!'; - pBuffer[Pos++] = 'a' + pVars[v]; - Abc_TtSwapVars( p, nVars, v, nVars - 1 ); - pVars[v] = pVars[nVars-1]; - Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func ); - pBuffer[Pos++] = ')'; - return Pos; - } - } - // check for a^x - for ( v = 0; v < nVars; v++ ) - if ( Abc_TtCofsOpposite( p, nWords, v ) ) - { - pBuffer[Pos++] = '['; - pBuffer[Pos++] = 'a' + pVars[v]; - Abc_TtSwapVars( p, nVars, v, nVars - 1 ); - pVars[v] = pVars[nVars-1]; - Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func ); - pBuffer[Pos++] = ']'; - return Pos; - } - - // 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; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Dau_DsdRun( word * p, int nVars ) -{ - static char pBuffer[DAU_MAX_STR+20]; - static char pStore[16][16]; - int nWords = Abc_TtWordNum( nVars ); - int i, Pos = 0, Func = 0, pVars[16]; - assert( nVars <= 16 ); - for ( i = 0; i < nVars; i++ ) - pVars[i] = i; - if ( Abc_TtTruthIsConst0( p, nWords ) ) - pBuffer[Pos++] = '0'; - else if ( Abc_TtTruthIsConst1( p, nWords ) ) - pBuffer[Pos++] = '1'; - else if ( nVars <= 6 ) - Pos = Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func ); - else - Pos = Dau_DsdRun_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func ); - pBuffer[Pos++] = 0; - Dau_DsdCleanBraces( pBuffer ); - return pBuffer; -} - - - - -/**Function************************************************************* - Synopsis [Data-structure to store DSD information.] Description [] @@ -1256,10 +1194,12 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) && Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor { - nVars = Dau_Dsd6DecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports ); - if ( nVars == 0 ) + int nVarsNew = Dau_Dsd6DecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports ); + if ( nVarsNew == nVars ) + continue; + if ( nVarsNew == 0 ) return 0; - nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars ); + nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVarsNew ); if ( nVars == 0 ) return 0; break; @@ -1373,7 +1313,7 @@ char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ) *pnSizeNonDec = p->nSizeNonDec; return p->pOutput; } -void Dau_DsdTest() +void Dau_DsdTest33() { // char * pStr = "(!(!a<bcd>)!(!fe))"; // char * pStr = "([acb]<!edf>)"; @@ -1382,13 +1322,13 @@ void Dau_DsdTest() // char * pStr = "<(a<bcd>)ef>"; char * pStr = "[d8001{a(!bc)ef}]"; char * pStr2; - word t = Dau_DsdToTruth( pStr ); -// return; + word t = Dau_Dsd6ToTruth( pStr ); + return; pStr2 = Dau_DsdDecompose( &t, 6, NULL ); - t = 0; + t = 0; } -void Dau_DsdTest22() +void Dau_DsdTest() { char * pFileName = "_npn/npn/dsd06.txt"; FILE * pFile = fopen( pFileName, "rb" ); @@ -1397,6 +1337,7 @@ void Dau_DsdTest22() char * pStr2; int nSizeNonDec; int i, Counter = 0; + clock_t clk = clock(); while ( fgets( pBuffer, 100, pFile ) != NULL ) { pStr2 = pBuffer + strlen(pBuffer)-1; @@ -1406,16 +1347,17 @@ void Dau_DsdTest22() *pStr2-- = 0; if ( pBuffer[0] == 'V' || pBuffer[0] == 0 ) continue; - Counter++; + Counter++; - for ( i = 0; i < 10; i++ ) + for ( i = 0; i < 1000; i++ ) { Dau_DsdPermute( pBuffer ); - - t = t1 = Dau_DsdToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer ); + + t = t1 = Dau_Dsd6ToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer ); pStr2 = Dau_DsdDecompose( &t, 6, &nSizeNonDec ); +// pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0; assert( nSizeNonDec == 0 ); - t2 = Dau_DsdToTruth( pStr2 ); + t2 = Dau_Dsd6ToTruth( pStr2 ); if ( t1 != t2 ) { // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); @@ -1426,7 +1368,8 @@ void Dau_DsdTest22() } } } - printf( "Finished trying %d decompositions.\n", Counter ); + printf( "Finished trying %d decompositions. ", Counter ); + Abc_PrintTime( 1, "Time", clock() - clk ); fclose( pFile ); } |