| /**CFile**************************************************************** |
| |
| FileName [rsbDec6.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Truth-table-based resubstitution.] |
| |
| Synopsis [Implementation of the algorithm.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: rsbDec6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "rsbInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned Rsb_DecTry0( word c ) |
| { |
| return (unsigned)(c != 0); |
| } |
| static inline unsigned Rsb_DecTry1( word c, word f1 ) |
| { |
| return (Rsb_DecTry0(c&f1) << 1) | Rsb_DecTry0(c&~f1); |
| } |
| static inline unsigned Rsb_DecTry2( word c, word f1, word f2 ) |
| { |
| return (Rsb_DecTry1(c&f2, f1) << 2) | Rsb_DecTry1(c&~f2, f1); |
| } |
| static inline unsigned Rsb_DecTry3( word c, word f1, word f2, word f3 ) |
| { |
| return (Rsb_DecTry2(c&f3, f1, f2) << 4) | Rsb_DecTry2(c&~f3, f1, f2); |
| } |
| static inline unsigned Rsb_DecTry4( word c, word f1, word f2, word f3, word f4 ) |
| { |
| return (Rsb_DecTry3(c&f4, f1, f2, f3) << 8) | Rsb_DecTry3(c&~f4, f1, f2, f3); |
| } |
| static inline unsigned Rsb_DecTry5( word c, word f1, word f2, word f3, word f4, word f5 ) |
| { |
| return (Rsb_DecTry4(c&f5, f1, f2, f3, f4) << 16) | Rsb_DecTry4(c&~f5, f1, f2, f3, f4); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Rsb_DecTryCex( word * g, int iCexA, int iCexB ) |
| { |
| return Abc_TtGetBit(g, iCexA) == Abc_TtGetBit(g, iCexB); |
| } |
| static inline void Rsb_DecVerifyCex( word * f, word ** g, int nGs, int iCexA, int iCexB ) |
| { |
| int i; |
| // f distinquished it |
| if ( Rsb_DecTryCex( f, iCexA, iCexB ) ) |
| printf( "Verification of CEX has failed: f(A) == f(B)!!!\n" ); |
| // g do not distinguish it |
| for ( i = 0; i < nGs; i++ ) |
| if ( !Rsb_DecTryCex( g[i], iCexA, iCexB ) ) |
| printf( "Verification of CEX has failed: g[%d](A) != g[%d](B)!!!\n", i, i ); |
| } |
| static inline void Rsb_DecRecordCex( word ** g, int nGs, int iCexA, int iCexB, word * pCexes, int nCexes ) |
| { |
| int i; |
| assert( nCexes < 64 ); |
| for ( i = 0; i < nGs; i++ ) |
| if ( Rsb_DecTryCex(g[i], iCexA, iCexB) ) |
| Abc_TtSetBit( pCexes + i, nCexes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks decomposability of f with divisors g.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline word Rsb_DecCofactor( word ** g, int nGs, int w, int iMint ) |
| { |
| int i; |
| word Cof = ~(word)0; |
| for ( i = 0; i < nGs; i++ ) |
| Cof &= ((iMint >> i) & 1) ? g[i][w] : ~g[i][w]; |
| return Cof; |
| } |
| unsigned Rsb_DecCheck( int nVars, word * f, word ** g, int nGs, unsigned * pPat, int * pCexA, int * pCexB ) |
| { |
| word CofA, CofB; |
| int nWords = Abc_TtWordNum( nVars ); |
| int w, k, iMint, iShift = ( 1 << nGs ); |
| unsigned uMask = (~(unsigned)0) >> (32-iShift); |
| unsigned uTotal = 0; |
| assert( nGs > 0 && nGs < 5 ); |
| for ( w = 0; w < nWords; w++ ) |
| { |
| // generate decomposition pattern |
| if ( nGs == 1 ) |
| pPat[w] = Rsb_DecTry2( ~(word)0, g[0][w], f[w] ); |
| else if ( nGs == 2 ) |
| pPat[w] = Rsb_DecTry3( ~(word)0, g[0][w], g[1][w], f[w] ); |
| else if ( nGs == 3 ) |
| pPat[w] = Rsb_DecTry4( ~(word)0, g[0][w], g[1][w], g[2][w], f[w] ); |
| else if ( nGs == 4 ) |
| pPat[w] = Rsb_DecTry5( ~(word)0, g[0][w], g[1][w], g[2][w], g[3][w], f[w] ); |
| // check if it is consistent |
| iMint = Abc_Tt6FirstBit( (pPat[w] >> iShift) & pPat[w] & uMask ); |
| if ( iMint >= 0 ) |
| { // generate a cex |
| CofA = Rsb_DecCofactor( g, nGs, w, iMint ); |
| assert( (~f[w] & CofA) && (f[w] & CofA) ); |
| *pCexA = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofA ); |
| *pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofA ); |
| return 0; |
| } |
| uTotal |= pPat[w]; |
| if ( w == 0 ) |
| continue; |
| // check if it is consistent with other patterns seen so far |
| iMint = Abc_Tt6FirstBit( (uTotal >> iShift) & uTotal & uMask ); |
| if ( iMint == -1 ) |
| continue; |
| // find an overlap and generate a cex |
| for ( k = 0; k < w; k++ ) |
| { |
| iMint = Abc_Tt6FirstBit( ((pPat[k] | pPat[w]) >> iShift) & (pPat[k] | pPat[w]) & uMask ); |
| if ( iMint == -1 ) |
| continue; |
| CofA = Rsb_DecCofactor( g, nGs, k, iMint ); |
| CofB = Rsb_DecCofactor( g, nGs, w, iMint ); |
| if ( (~f[k] & CofA) && (f[w] & CofB) ) |
| { |
| *pCexA = k * 64 + Abc_Tt6FirstBit( ~f[k] & CofA ); |
| *pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofB ); |
| } |
| else |
| { |
| assert( (f[k] & CofA) && (~f[w] & CofB) ); |
| *pCexA = k * 64 + Abc_Tt6FirstBit( f[k] & CofA ); |
| *pCexB = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofB ); |
| } |
| return 0; |
| } |
| } |
| return uTotal; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Rsb_DecPrintTable( word * pCexes, int nGs, int nGsAll, Vec_Int_t * vTries ) |
| { |
| int pCands[16], nCands; |
| int i, c, Cand, iStart = 0; |
| if ( Vec_IntSize(vTries) == 0 ) |
| return; |
| |
| // printf( "\n" ); |
| for ( i = 0; i < 4; i++ ) |
| printf( " " ); |
| printf( " " ); |
| for ( i = 0; i < nGs; i++ ) |
| printf( "%d", (i % 100) / 10 ); |
| printf( "|" ); |
| for ( ; i < nGsAll; i++ ) |
| printf( "%d", (i % 100) / 10 ); |
| printf( "\n" ); |
| |
| for ( i = 0; i < 4; i++ ) |
| printf( " " ); |
| printf( " " ); |
| for ( i = 0; i < nGs; i++ ) |
| printf( "%d", i % 10 ); |
| printf( "|" ); |
| for ( ; i < nGsAll; i++ ) |
| printf( "%d", i % 10 ); |
| printf( "\n" ); |
| printf( "\n" ); |
| |
| for ( c = 0; iStart < Vec_IntSize(vTries); c++ ) |
| { |
| // collect candidates |
| for ( i = 0; i < 4; i++ ) |
| pCands[i] = -1; |
| nCands = 0; |
| Vec_IntForEachEntryStart( vTries, Cand, i, iStart ) |
| if ( Cand == -1 ) |
| { |
| iStart = i + 1; |
| break; |
| } |
| else |
| pCands[nCands++] = Cand; |
| assert( nCands <= 4 ); |
| // print them |
| for ( i = 0; i < 4; i++ ) |
| if ( pCands[i] >= 0 ) |
| printf( "%4d", pCands[i] ); |
| else |
| printf( " " ); |
| // print the bit-string |
| printf( " " ); |
| for ( i = 0; i < nGs; i++ ) |
| printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' ); |
| printf( "|" ); |
| for ( ; i < nGsAll; i++ ) |
| printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' ); |
| printf( " %3d\n", c ); |
| } |
| printf( "\n" ); |
| |
| // write the number of ones |
| for ( i = 0; i < 4; i++ ) |
| printf( " " ); |
| printf( " " ); |
| for ( i = 0; i < nGs; i++ ) |
| printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 ); |
| printf( "|" ); |
| for ( ; i < nGsAll; i++ ) |
| printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 ); |
| printf( "\n" ); |
| |
| for ( i = 0; i < 4; i++ ) |
| printf( " " ); |
| printf( " " ); |
| for ( i = 0; i < nGs; i++ ) |
| printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 ); |
| printf( "|" ); |
| for ( ; i < nGsAll; i++ ) |
| printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 ); |
| printf( "\n" ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Init ] |
| |
| Description [Returns the numbers of the decomposition functions and |
| the truth table of a function up to 4 variables.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word * pCexes, Vec_Int_t * vTries ) |
| { |
| int nWords = Abc_TtWordNum( nVars ); |
| int ValueB = Abc_TtGetBit( f, 0 ); |
| int ValueE = Abc_TtGetBit( f, 64*nWords-1 ); |
| int iCexT0, iCexT1, iCexF0, iCexF1; |
| |
| iCexT0 = ValueB ? 0 : Abc_TtFindFirstBit( f, nVars ); |
| iCexT1 = ValueE ? 64*nWords-1 : Abc_TtFindLastBit( f, nVars ); |
| |
| iCexF0 = !ValueB ? 0 : Abc_TtFindFirstZero( f, nVars ); |
| iCexF1 = !ValueE ? 64*nWords-1 : Abc_TtFindLastZero( f, nVars ); |
| |
| assert( !Rsb_DecTryCex( f, iCexT0, iCexF0 ) ); |
| assert( !Rsb_DecTryCex( f, iCexT0, iCexF1 ) ); |
| assert( !Rsb_DecTryCex( f, iCexT1, iCexF0 ) ); |
| assert( !Rsb_DecTryCex( f, iCexT1, iCexF1 ) ); |
| |
| Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF0, pCexes, 0 ); |
| Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF1, pCexes, 1 ); |
| Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF0, pCexes, 2 ); |
| Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF1, pCexes, 3 ); |
| |
| if ( vTries ) |
| { |
| Vec_IntPush( vTries, -1 ); |
| Vec_IntPush( vTries, -1 ); |
| Vec_IntPush( vTries, -1 ); |
| Vec_IntPush( vTries, -1 ); |
| } |
| return 4; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds a setset of gs to decompose f.] |
| |
| Description [Returns the numbers of the decomposition functions and |
| the truth table of a function up to 4 variables.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fFindAll ) |
| { |
| word * pCexes = Vec_WrdArray(p->vCexes); |
| unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats); |
| /* |
| The following filtering hueristic can be used: |
| after the first round (if there is more than 5 cexes, |
| remove all the divisors, except fanins of the node |
| This should lead to a speadup without sacrifying quality. |
| |
| Another idea is to precompute several counter-examples |
| like the first and last 0 and 1 mints of the function |
| which yields 4 cexes. |
| */ |
| |
| word * pDivs[16]; |
| unsigned uTruth = 0; |
| int i, k, j, n, iCexA, iCexB, nCexes = 0; |
| memset( pCexes, 0, sizeof(word) * nGsAll ); |
| Vec_IntClear( p->vTries ); |
| // populate the counter-examples with the three most obvious |
| // nCexes = Rsb_DecInitCexes( nVars, f, g, nGs, nGsAll, pCexes, vTries ); |
| // start by checking each function |
| p->vFanins->nSize = 1; |
| for ( i = 0; i < nGs; i++ ) |
| { |
| if ( pCexes[i] ) |
| continue; |
| pDivs[0] = g[i]; p->vFanins->pArray[0] = i; |
| uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); |
| if ( uTruth ) |
| { |
| if ( fFindAll ) |
| { |
| uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 1 ); |
| Kit_DsdPrintFromTruth( &uTruth, 1 ); printf( " " ); |
| Vec_IntPrint(p->vFanins); |
| continue; |
| } |
| else |
| return uTruth; |
| } |
| if ( nCexes == 64 ) |
| return 0; |
| Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); |
| Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ ); |
| if ( !p->fVerbose ) |
| continue; |
| Vec_IntPush( p->vTries, i ); |
| Vec_IntPush( p->vTries, -1 ); |
| } |
| if ( p->nDecMax == 1 ) |
| return 0; |
| // continue by checking pairs |
| p->vFanins->nSize = 2; |
| for ( i = 1; i < nGs; i++ ) |
| for ( k = 0; k < i; k++ ) |
| { |
| if ( pCexes[i] & pCexes[k] ) |
| continue; |
| pDivs[0] = g[i]; p->vFanins->pArray[0] = i; |
| pDivs[1] = g[k]; p->vFanins->pArray[1] = k; |
| uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); |
| if ( uTruth ) |
| { |
| if ( fFindAll ) |
| { |
| uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 2 ); |
| Kit_DsdPrintFromTruth( &uTruth, 2 ); printf( " " ); |
| Vec_IntPrint(p->vFanins); |
| continue; |
| } |
| else |
| return uTruth; |
| } |
| if ( nCexes == 64 ) |
| return 0; |
| Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); |
| Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ ); |
| if ( !p->fVerbose ) |
| continue; |
| Vec_IntPush( p->vTries, i ); |
| Vec_IntPush( p->vTries, k ); |
| Vec_IntPush( p->vTries, -1 ); |
| } |
| if ( p->nDecMax == 2 ) |
| return 0; |
| // continue by checking triples |
| p->vFanins->nSize = 3; |
| for ( i = 2; i < nGs; i++ ) |
| for ( k = 1; k < i; k++ ) |
| for ( j = 0; j < k; j++ ) |
| { |
| if ( pCexes[i] & pCexes[k] & pCexes[j] ) |
| continue; |
| pDivs[0] = g[i]; p->vFanins->pArray[0] = i; |
| pDivs[1] = g[k]; p->vFanins->pArray[1] = k; |
| pDivs[2] = g[j]; p->vFanins->pArray[2] = j; |
| uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); |
| if ( uTruth ) |
| { |
| if ( fFindAll ) |
| { |
| uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 3 ); |
| Kit_DsdPrintFromTruth( &uTruth, 3 ); printf( " " ); |
| Vec_IntPrint(p->vFanins); |
| continue; |
| } |
| else |
| return uTruth; |
| } |
| if ( nCexes == 64 ) |
| return 0; |
| Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); |
| Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ ); |
| if ( !p->fVerbose ) |
| continue; |
| Vec_IntPush( p->vTries, i ); |
| Vec_IntPush( p->vTries, k ); |
| Vec_IntPush( p->vTries, j ); |
| Vec_IntPush( p->vTries, -1 ); |
| } |
| if ( p->nDecMax == 3 ) |
| return 0; |
| // continue by checking quadras |
| p->vFanins->nSize = 4; |
| for ( i = 3; i < nGs; i++ ) |
| for ( k = 2; k < i; k++ ) |
| for ( j = 1; j < k; j++ ) |
| for ( n = 0; n < j; n++ ) |
| { |
| if ( pCexes[i] & pCexes[k] & pCexes[j] & pCexes[n] ) |
| continue; |
| pDivs[0] = g[i]; p->vFanins->pArray[0] = i; |
| pDivs[1] = g[k]; p->vFanins->pArray[1] = k; |
| pDivs[2] = g[j]; p->vFanins->pArray[2] = j; |
| pDivs[3] = g[n]; p->vFanins->pArray[3] = n; |
| uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); |
| if ( uTruth ) |
| { |
| if ( fFindAll ) |
| { |
| uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 4 ); |
| Kit_DsdPrintFromTruth( &uTruth, 4 ); printf( " " ); |
| Vec_IntPrint(p->vFanins); |
| continue; |
| } |
| else |
| return uTruth; |
| } |
| if ( nCexes == 64 ) |
| return 0; |
| Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); |
| Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ ); |
| if ( !p->fVerbose ) |
| continue; |
| Vec_IntPush( p->vTries, i ); |
| Vec_IntPush( p->vTries, k ); |
| Vec_IntPush( p->vTries, j ); |
| Vec_IntPush( p->vTries, n ); |
| Vec_IntPush( p->vTries, -1 ); |
| } |
| // printf( "%d ", nCexes ); |
| if ( p->nDecMax == 4 ) |
| return 0; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Verifies 4-input decomposition.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Rsb_DecPrintFunc( Rsb_Man_t * p, unsigned Truth4, word * f, word ** ppGs, int nGs, int nVarsAll ) |
| { |
| int nVars = Vec_IntSize(p->vFanins); |
| word Copy = Truth4; |
| word wOn = Abc_Tt6Stretch( Copy >> (1 << nVars), nVars ); |
| word wOnDc = ~Abc_Tt6Stretch( Copy, nVars ); |
| word wIsop = Abc_Tt6Isop( wOn, wOnDc, nVars, NULL ); |
| int i; |
| |
| printf( "Offset : " ); |
| Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" ); |
| Copy >>= ((word)1 << nVars); |
| printf( "Onset : " ); |
| Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" ); |
| printf( "Result : " ); |
| Abc_TtPrintBinary( &wIsop, nVars ); //printf( "\n" ); |
| Kit_DsdPrintFromTruth( (unsigned *)&wIsop, nVars ); printf( "\n" ); |
| |
| // print functions |
| printf( "Func : " ); |
| Abc_TtPrintBinary( f, nVarsAll ); //printf( "\n" ); |
| Kit_DsdPrintFromTruth( (unsigned *)f, nVarsAll ); printf( "\n" ); |
| for ( i = 0; i < nGs; i++ ) |
| { |
| printf( "Div%3d : ", i ); |
| Kit_DsdPrintFromTruth( (unsigned *)ppGs[i], nVarsAll ); printf( "\n" ); |
| } |
| printf( "Solution : " ); |
| for ( i = 0; i < Vec_IntSize(p->vFanins); i++ ) |
| printf( "%d ", Vec_IntEntry(p->vFanins, i) ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Verifies 4-input decomposition.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Rsb_DecVerify( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, unsigned Truth4, word * pTemp1, word * pTemp2 ) |
| { |
| word * pFanins[16]; |
| int b, m, Num, nSuppSize; |
| int nWords = Abc_TtWordNum(nVars); |
| Truth4 >>= (1 << Vec_IntSize(p->vFanins)); |
| Truth4 = (unsigned)Abc_Tt6Stretch( (word)Truth4, Vec_IntSize(p->vFanins) ); |
| //Kit_DsdPrintFromTruth( (unsigned *)&Truth4, Vec_IntSize(p->vFanins) ); |
| //printf( "\n" ); |
| // nSuppSize = Rsb_Word6SupportSize( Truth4 ); |
| // assert( nSuppSize == Vec_IntSize(p->vFanins) ); |
| nSuppSize = Vec_IntSize(p->vFanins); |
| // collect the fanins |
| Vec_IntForEachEntry( p->vFanins, Num, b ) |
| { |
| assert( Num < nGs ); |
| pFanins[b] = g[Num]; |
| } |
| // create the or of ands |
| Abc_TtClear( pTemp1, nWords ); |
| for ( m = 0; m < (1<<nSuppSize); m++ ) |
| { |
| if ( ((Truth4 >> m) & 1) == 0 ) |
| continue; |
| Abc_TtFill( pTemp2, nWords ); |
| for ( b = 0; b < nSuppSize; b++ ) |
| if ( (m >> b) & 1 ) |
| Abc_TtAnd( pTemp2, pTemp2, pFanins[b], nWords, 0 ); |
| else |
| Abc_TtSharp( pTemp2, pTemp2, pFanins[b], nWords ); |
| Abc_TtOr( pTemp1, pTemp1, pTemp2, nWords ); |
| } |
| // check the function |
| if ( !Abc_TtEqual( pTemp1, f, nWords ) ) |
| printf( "Verification failed.\n" ); |
| // else |
| // printf( "Verification passed.\n" ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds a setset of gs to decompose f.] |
| |
| Description [Returns the numbers of the decomposition functions and |
| the truth table of a function up to 4 variables.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fVerbose0 ) |
| { |
| word * pCexes = Vec_WrdArray(p->vCexes); |
| unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats); |
| int fVerbose = 0;//(nGs > 40); |
| Vec_Int_t * vTries = NULL; |
| unsigned uTruth; |
| |
| // verify original decomposition |
| if ( Vec_IntSize(p->vFaninsOld) && Vec_IntSize(p->vFaninsOld) <= 4 ) |
| { |
| word * pDivs[8]; |
| int i, Entry, iCexA, iCexB; |
| Vec_IntForEachEntry( p->vFaninsOld, Entry, i ) |
| pDivs[i] = g[Entry]; |
| uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFaninsOld), pPat, &iCexA, &iCexB ); |
| // assert( uTruth != 0 ); |
| if ( fVerbose ) |
| { |
| printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) ); |
| Vec_IntForEachEntry( p->vFaninsOld, Entry, i ) |
| printf( " %d", Entry ); |
| printf( " }\n" ); |
| } |
| if ( uTruth ) |
| { |
| // if ( fVerbose ) |
| // Rsb_DecPrintFunc( p, uTruth ); |
| } |
| else |
| { |
| printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) ); |
| Vec_IntForEachEntry( p->vFaninsOld, Entry, i ) |
| printf( " %d", Entry ); |
| printf( " }\n" ); |
| printf( "Verification FAILED.\n" ); |
| } |
| } |
| // start tries |
| if ( fVerbose ) |
| vTries = Vec_IntAlloc( 100 ); |
| assert( nGs < nGsAll ); |
| uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll, 0 ); |
| |
| if ( uTruth ) |
| { |
| if ( fVerbose ) |
| { |
| int i, Entry; |
| printf( "Found decomp with %d vars {", Vec_IntSize(p->vFanins) ); |
| Vec_IntForEachEntry( p->vFanins, Entry, i ) |
| printf( " %d", Entry ); |
| printf( " }\n" ); |
| // Rsb_DecPrintFunc( p, uTruth ); |
| // Rsb_DecVerify( nVars, f, g, nGs, p->vFanins, uTruth, g[nGsAll], g[nGsAll+1] ); |
| } |
| } |
| else |
| { |
| Vec_IntShrink( p->vFanins, 0 ); |
| if ( fVerbose ) |
| printf( "Did not find decomposition with 4 variables.\n" ); |
| } |
| |
| if ( fVerbose ) |
| Rsb_DecPrintTable( pCexes, nGs, nGsAll, vTries ); |
| if ( fVerbose ) |
| Vec_IntFree( vTries ); |
| return uTruth; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose ) |
| { |
| word * pGs[200]; |
| unsigned uTruthRes; |
| int i, nVars, nGs = Vec_WrdSize(vDivTruths); |
| assert( nGs < 200 ); |
| for ( i = 0; i < nGs; i++ ) |
| pGs[i] = Vec_WrdEntryP(vDivTruths,i); |
| uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs, 0 ); |
| if ( uTruthRes == 0 ) |
| return 0; |
| |
| if ( fVerbose ) |
| Rsb_DecPrintFunc( p, uTruthRes, &uTruth, pGs, nGs, nVarsAll ); |
| if ( fVerbose ) |
| Rsb_DecPrintTable( Vec_WrdArray(p->vCexes), nGs, nGs, p->vTries ); |
| |
| nVars = Vec_IntSize(p->vFanins); |
| *puTruth0 = Abc_Tt6Stretch( uTruthRes, nVars ); |
| *puTruth1 = Abc_Tt6Stretch( uTruthRes >> (1 << nVars), nVars ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Rsb_ManPerformResub6Test() |
| { |
| Rsb_Man_t * p; |
| Vec_Wrd_t * vDivTruths; |
| int RetValue; |
| word a = s_Truths6[0]; |
| word b = s_Truths6[1]; |
| word c = s_Truths6[2]; |
| word d = s_Truths6[3]; |
| word e = s_Truths6[4]; |
| word f = s_Truths6[5]; |
| word ab = a & b; |
| word cd = c & d; |
| word ef = e & f; |
| word F = ab | cd | ef; |
| word uTruth0, uTruth1; |
| |
| vDivTruths = Vec_WrdAlloc( 100 ); |
| Vec_WrdPush( vDivTruths, a ); |
| Vec_WrdPush( vDivTruths, b ); |
| Vec_WrdPush( vDivTruths, c ); |
| Vec_WrdPush( vDivTruths, d ); |
| Vec_WrdPush( vDivTruths, e ); |
| Vec_WrdPush( vDivTruths, f ); |
| Vec_WrdPush( vDivTruths, ab ); |
| Vec_WrdPush( vDivTruths, cd ); |
| Vec_WrdPush( vDivTruths, ef ); |
| |
| p = Rsb_ManAlloc( 6, 64, 4, 1 ); |
| |
| RetValue = Rsb_ManPerformResub6( p, 6, F, vDivTruths, &uTruth0, &uTruth1, 1 ); |
| |
| Rsb_ManFree( p ); |
| Vec_WrdFree( vDivTruths ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
