diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-12-11 20:45:41 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-12-11 20:45:41 -0800 |
commit | b379b3ee20266a4dcfc11f9113326f764846d79e (patch) | |
tree | bab68d4e2c10a6c576949f9fe878c3ed7e5ea213 /src/misc | |
parent | ac7633c5a4c874bd6f29827017ee23fc23613ad5 (diff) | |
download | abc-b379b3ee20266a4dcfc11f9113326f764846d79e.tar.gz abc-b379b3ee20266a4dcfc11f9113326f764846d79e.tar.bz2 abc-b379b3ee20266a4dcfc11f9113326f764846d79e.zip |
Adding new mapping feature.
Diffstat (limited to 'src/misc')
-rw-r--r-- | src/misc/util/utilTruth.h | 266 |
1 files changed, 266 insertions, 0 deletions
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 0b52b3f4..645b639c 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -2269,6 +2269,272 @@ static inline void Unm_ManCheckTest() } + +/**Function************************************************************* + + Synopsis [Checks existence of bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtComputeGraph( word * pTruth, int v, int nVars, int * pGraph ) +{ + word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 ) + word Cof00[64], Cof01[64], Cof10[64], Cof11[64]; + word CofXor, CofAndTest; + int i, w, nWords = Abc_TtWordNum(nVars); + pGraph[v] |= (1 << v); + if ( v == nVars - 1 ) + return; + assert( v < nVars - 1 ); + Abc_TtCofactor0p( Cof0, pTruth, nWords, v ); + Abc_TtCofactor1p( Cof1, pTruth, nWords, v ); + for ( i = v + 1; i < nVars; i++ ) + { + Abc_TtCofactor0p( Cof00, Cof0, nWords, i ); + Abc_TtCofactor1p( Cof01, Cof0, nWords, i ); + Abc_TtCofactor0p( Cof10, Cof1, nWords, i ); + Abc_TtCofactor1p( Cof11, Cof1, nWords, i ); + for ( w = 0; w < nWords; w++ ) + { + CofXor = Cof00[w] ^ Cof01[w] ^ Cof10[w] ^ Cof11[w]; + CofAndTest = (Cof00[w] & Cof01[w]) | (Cof10[w] & Cof11[w]); + if ( CofXor & CofAndTest ) + { + pGraph[v] |= (1 << i); + pGraph[i] |= (1 << v); + } + else if ( CofXor & ~CofAndTest ) + { + pGraph[v] |= (1 << (16+i)); + pGraph[i] |= (1 << (16+v)); + } + } + } +} +static inline void Abc_TtPrintVarSet( int Mask, int nVars ) +{ + int i; + for ( i = 0; i < nVars; i++ ) + if ( (Mask >> i) & 1 ) + printf( "1" ); + else + printf( "." ); +} +static inline void Abc_TtPrintBiDec( word * pTruth, int nVars ) +{ + int v, pGraph[12] = {0}; + assert( nVars <= 12 ); + for ( v = 0; v < nVars; v++ ) + { + Abc_TtComputeGraph( pTruth, v, nVars, pGraph ); + Abc_TtPrintVarSet( pGraph[v], nVars ); + printf( " " ); + Abc_TtPrintVarSet( pGraph[v] >> 16, nVars ); + printf( "\n" ); + } +} +static inline int Abc_TtVerifyBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word wThis, word wThat ) +{ + int pVarsThis[12], pVarsThat[12], pVarsAll[12]; + int nThis = Abc_TtBitCount16(This); + int nThat = Abc_TtBitCount16(That); + int i, k, nWords = Abc_TtWordNum(nVars); + word pThis[64] = {wThis}, pThat[64] = {wThat}; + assert( nVars <= 12 ); + for ( i = 0; i < nVars; i++ ) + pVarsAll[i] = i; + for ( i = k = 0; i < nVars; i++ ) + if ( (This >> i) & 1 ) + pVarsThis[k++] = i; + assert( k == nThis ); + for ( i = k = 0; i < nVars; i++ ) + if ( (That >> i) & 1 ) + pVarsThat[k++] = i; + assert( k == nThat ); + Abc_TtStretch6( pThis, nThis, nVars ); + Abc_TtStretch6( pThat, nThat, nVars ); + Abc_TtExpand( pThis, nVars, pVarsThis, nThis, pVarsAll, nVars ); + Abc_TtExpand( pThat, nVars, pVarsThat, nThat, pVarsAll, nVars ); + for ( k = 0; k < nWords; k++ ) + if ( pTruth[k] != (pThis[k] & pThat[k]) ) + return 0; + return 1; +} +static inline void Abc_TtExist( word * pTruth, int iVar, int nWords ) +{ + word Cof0[64], Cof1[64]; + Abc_TtCofactor0p( Cof0, pTruth, nWords, iVar ); + Abc_TtCofactor1p( Cof1, pTruth, nWords, iVar ); + Abc_TtOr( pTruth, Cof0, Cof1, nWords ); +} +static inline int Abc_TtCheckBiDec( word * pTruth, int nVars, int This, int That ) +{ + int VarMask[2] = {This & ~That, That & ~This}; + int v, c, nWords = Abc_TtWordNum(nVars); + word pTempR[2][64]; + for ( c = 0; c < 2; c++ ) + { + Abc_TtCopy( pTempR[c], pTruth, nWords, 0 ); + for ( v = 0; v < nVars; v++ ) + if ( ((VarMask[c] >> v) & 1) ) + Abc_TtExist( pTempR[c], v, nWords ); + } + for ( v = 0; v < nWords; v++ ) + if ( ~pTruth[v] & pTempR[0][v] & pTempR[1][v] ) + return 0; + return 1; +} +static inline word Abc_TtDeriveBiDecOne( word * pTruth, int nVars, int This ) +{ + word pTemp[64]; + int nThis = Abc_TtBitCount16(This); + int v, nWords = Abc_TtWordNum(nVars); + Abc_TtCopy( pTemp, pTruth, nWords, 0 ); + for ( v = 0; v < nVars; v++ ) + if ( !((This >> v) & 1) ) + Abc_TtExist( pTemp, v, nWords ); + Abc_TtShrink( pTemp, nThis, nVars, This ); + return Abc_Tt6Stretch( pTemp[0], nThis ); +} +static inline void Abc_TtDeriveBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word * pThis, word * pThat ) +{ + assert( Abc_TtBitCount16(This) <= nSuppLim ); + assert( Abc_TtBitCount16(That) <= nSuppLim ); + pThis[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, This ); + pThat[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, That ); + if ( !Abc_TtVerifyBiDec(pTruth, nVars, This, That, nSuppLim, pThis[0], pThat[0] ) ) + printf( "Bi-decomposition verification failed.\n" ); +} +// detect simple case of decomposition with topmost AND gate +static inline int Abc_TtCheckBiDecSimple( word * pTruth, int nVars, int nSuppLim ) +{ + word Cof0[64], Cof1[64]; + int v, Res = 0, nDecVars = 0, nWords = Abc_TtWordNum(nVars); + for ( v = 0; v < nVars; v++ ) + { + Abc_TtCofactor0p( Cof0, pTruth, nWords, v ); + Abc_TtCofactor1p( Cof1, pTruth, nWords, v ); + if ( !Abc_TtIsConst0(Cof0, nWords) && !Abc_TtIsConst0(Cof1, nWords) ) + continue; + nDecVars++; + Res |= 1 << v; + if ( nDecVars >= nVars - nSuppLim ) + return ((Res ^ (int)Abc_Tt6Mask(nVars)) << 16) | Res; + } + return 0; +} +static inline int Abc_TtProcessBiDec( word * pTruth, int nVars, int nSuppLim ) +{ + int i, v, Res, nSupp, CountShared = 0, pGraph[12] = {0}; + assert( nSuppLim < nVars && nVars <= 12 ); + assert( 2 <= nSuppLim && nSuppLim <= 6 ); + Res = Abc_TtCheckBiDecSimple( pTruth, nVars, nSuppLim ); + if ( Res ) + return Res; + for ( v = 0; v < nVars; v++ ) + { + Abc_TtComputeGraph( pTruth, v, nVars, pGraph ); + nSupp = Abc_TtBitCount16(pGraph[v] & 0xFFFF); + if ( nSupp > nSuppLim ) + { + // this variable is shared - check if the limit is exceeded + if ( ++CountShared > 2*nSuppLim - nVars ) + return 0; + } + else if ( nVars - nSupp <= nSuppLim ) + { + int This = pGraph[v] & 0xFFFF; + int That = This ^ (int)Abc_Tt6Mask(nVars); + // find the other component + int Graph = That; + for ( i = 0; i < nVars; i++ ) + if ( (That >> i) & 1 ) + Graph |= pGraph[i] & 0xFFFF; + // check if this can be done + if ( Abc_TtBitCount16(Graph) > nSuppLim ) + continue; + // try decomposition + if ( Abc_TtCheckBiDec(pTruth, nVars, This, Graph) ) + return (Graph << 16) | This; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Tests decomposition procedures.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLim ) +{ + word This, That, pTemp[64]; + int Res, resThis, resThat, nThis, nThat; + int nWords = Abc_TtWordNum(nVars); + Abc_TtCopy( pTemp, pTruth, nWords, 0 ); + Res = Abc_TtProcessBiDec( pTemp, nVars, nSuppLim ); + if ( Res == 0 ) + { + //Dau_DsdPrintFromTruth( pTemp, nVars ); + //printf( "Non_dec\n\n" ); + return; + } + + resThis = Res & 0xFFFF; + resThat = Res >> 16; + + Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That ); + return; + + //if ( !(resThis & resThat) ) + // return; + +// Dau_DsdPrintFromTruth( pTemp, nVars ); + + nThis = Abc_TtBitCount16(resThis); + nThat = Abc_TtBitCount16(resThat); + + printf( "Variable sets: " ); + Abc_TtPrintVarSet( resThis, nVars ); + printf( " " ); + Abc_TtPrintVarSet( resThat, nVars ); + printf( "\n" ); + Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That ); +// Dau_DsdPrintFromTruth( &This, nThis ); +// Dau_DsdPrintFromTruth( &That, nThat ); + printf( "\n" ); +} +static inline void Abc_TtProcessBiDecExperiment() +{ + int nVars = 3; + int nSuppLim = 2; + int Res, resThis, resThat; + word This, That; +// word t = ABC_CONST(0x8000000000000000); +// word t = (s_Truths6[0] | s_Truths6[1]) & (s_Truths6[2] | s_Truths6[3] | s_Truths6[4] | s_Truths6[5]); +// word t = ((s_Truths6[0] & s_Truths6[1]) | (~s_Truths6[1] & s_Truths6[2])); + word t = ((s_Truths6[0] | s_Truths6[1]) & (s_Truths6[1] | s_Truths6[2])); + Abc_TtPrintBiDec( &t, nVars ); + Res = Abc_TtProcessBiDec( &t, nVars, nSuppLim ); + resThis = Res & 0xFFFF; + resThat = Res >> 16; + Abc_TtDeriveBiDec( &t, nVars, resThis, resThat, nSuppLim, &This, &That ); +// Dau_DsdPrintFromTruth( &This, Abc_TtBitCount16(resThis) ); +// Dau_DsdPrintFromTruth( &That, Abc_TtBitCount16(resThat) ); + nVars = nSuppLim; +} + /*=== utilTruth.c ===========================================================*/ |