| /**CFile**************************************************************** |
| |
| FileName [dauNonDsd.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [DAG-aware unmapping.] |
| |
| Synopsis [] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: dauNonDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "dauInt.h" |
| #include "misc/util/utilTruth.h" |
| #include "misc/extra/extra.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks decomposability with given variable set.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dau_DecCheckSetTop5( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int * pSched, word * pDec, word * pComp ) |
| { |
| word Cof[2][64], Value; |
| word MaskFF = (((word)1) << (1 << nVarsF)) - 1; |
| int ShiftF = 6 - nVarsF, MaskF = (1 << ShiftF) - 1; |
| int pVarsS[16], pVarsB[16]; |
| int nMints = (1 << nVarsB); |
| int nMintsB = (1 <<(nVarsB-nVarsS)); |
| int nMintsS = (1 << nVarsS); |
| int s, b, v, m, Mint, MintB, MintS; |
| assert( nVars == nVarsB + nVarsF ); |
| assert( nVars <= 16 ); |
| assert( nVarsS <= 6 ); |
| assert( nVarsF >= 1 && nVarsF <= 5 ); |
| // collect bound/shared variables |
| for ( s = b = v = 0; v < nVarsB; v++ ) |
| if ( (uMaskS >> v) & 1 ) |
| pVarsB[v] = -1, pVarsS[v] = s++; |
| else |
| pVarsS[v] = -1, pVarsB[v] = b++; |
| assert( s == nVarsS ); |
| assert( b == nVarsB-nVarsS ); |
| // clean minterm storage |
| for ( s = 0; s < nMintsS; s++ ) |
| Cof[0][s] = Cof[1][s] = ~(word)0; |
| // iterate through bound set minters |
| for ( MintS = MintB = Mint = m = 0; m < nMints; m++ ) |
| { |
| // find minterm value |
| Value = (p[Mint>>ShiftF] >> ((Mint&MaskF)<<nVarsF)) & MaskFF; |
| // check if this cof already appeared |
| if ( !~Cof[0][MintS] || Cof[0][MintS] == Value ) |
| Cof[0][MintS] = Value; |
| else if ( !~Cof[1][MintS] || Cof[1][MintS] == Value ) |
| { |
| Cof[1][MintS] = Value; |
| if ( pDec ) |
| { |
| int iMintB = MintS * nMintsB + MintB; |
| pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63)); |
| } |
| } |
| else |
| return 0; |
| // find next minterm |
| v = pSched[m]; |
| Mint ^= (1 << v); |
| if ( (uMaskS >> v) & 1 ) // shared variable |
| MintS ^= (1 << pVarsS[v]); |
| else |
| MintB ^= (1 << pVarsB[v]); |
| } |
| // create composition function |
| if ( pComp ) |
| { |
| for ( s = 0; s < nMintsS; s++ ) |
| { |
| pComp[s>>ShiftF] |= (Cof[0][s] << ((s&MaskF) << nVarsF)); |
| if ( ~Cof[1][s] ) |
| pComp[(s+nMintsS)>>ShiftF] |= (Cof[1][s] << (((s+nMintsS)&MaskF) << nVarsF)); |
| else |
| pComp[(s+nMintsS)>>ShiftF] |= (Cof[0][s] << (((s+nMintsS)&MaskF) << nVarsF)); |
| } |
| if ( nVarsF + nVarsS + 1 < 6 ) |
| pComp[0] = Abc_Tt6Stretch( pComp[0], nVarsF + nVarsS + 1 ); |
| } |
| if ( pDec && nVarsB < 6 ) |
| pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB ); |
| return 1; |
| } |
| int Dau_DecCheckSetTop6( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int * pSched, word * pDec, word * pComp ) |
| { |
| word * Cof[2][64]; |
| int nWordsF = Abc_TtWordNum(nVarsF); |
| int pVarsS[16], pVarsB[16]; |
| int nMints = (1 << nVarsB); |
| int nMintsB = (1 <<(nVarsB-nVarsS)); |
| int nMintsS = (1 << nVarsS); |
| int s, b, v, m, Mint, MintB, MintS; |
| assert( nVars == nVarsB + nVarsF ); |
| assert( nVars <= 16 ); |
| assert( nVarsS <= 6 ); |
| assert( nVarsF >= 6 ); |
| // collect bound/shared variables |
| for ( s = b = v = 0; v < nVarsB; v++ ) |
| if ( (uMaskS >> v) & 1 ) |
| pVarsB[v] = -1, pVarsS[v] = s++; |
| else |
| pVarsS[v] = -1, pVarsB[v] = b++; |
| assert( s == nVarsS ); |
| assert( b == nVarsB-nVarsS ); |
| // clean minterm storage |
| for ( s = 0; s < nMintsS; s++ ) |
| Cof[0][s] = Cof[1][s] = NULL; |
| // iterate through bound set minters |
| for ( MintS = MintB = Mint = m = 0; m < nMints; m++ ) |
| { |
| // check if this cof already appeared |
| if ( !Cof[0][MintS] || !memcmp(Cof[0][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) ) |
| Cof[0][MintS] = p + Mint * nWordsF; |
| else if ( !Cof[1][MintS] || !memcmp(Cof[1][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) ) |
| { |
| Cof[1][MintS] = p + Mint * nWordsF; |
| if ( pDec ) |
| { |
| int iMintB = MintS * nMintsB + MintB; |
| pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63)); |
| } |
| } |
| else |
| return 0; |
| // find next minterm |
| v = pSched[m]; |
| Mint ^= (1 << v); |
| if ( (uMaskS >> v) & 1 ) // shared variable |
| MintS ^= (1 << pVarsS[v]); |
| else |
| MintB ^= (1 << pVarsB[v]); |
| } |
| // create composition function |
| if ( pComp ) |
| { |
| for ( s = 0; s < nMintsS; s++ ) |
| { |
| memcpy( pComp + s * nWordsF, Cof[0][s], sizeof(word) * nWordsF ); |
| if ( Cof[1][s] ) |
| memcpy( pComp + (s+nMintsS) * nWordsF, Cof[1][s], sizeof(word) * nWordsF ); |
| else |
| memcpy( pComp + (s+nMintsS) * nWordsF, Cof[0][s], sizeof(word) * nWordsF ); |
| } |
| } |
| if ( pDec && nVarsB < 6 ) |
| pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB ); |
| return 1; |
| } |
| static inline int Dau_DecCheckSetTop( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int * pSched, word * pDec, word * pComp ) |
| { |
| if ( nVarsF < 6 ) |
| return Dau_DecCheckSetTop5( p, nVars, nVarsF, nVarsB, nVarsS, uMaskS, pSched, pDec, pComp ); |
| else |
| return Dau_DecCheckSetTop6( p, nVars, nVarsF, nVarsB, nVarsS, uMaskS, pSched, pDec, pComp ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks decomposability with given BS variables.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Dau_DecGetMinterm( word * p, int g, int nVarsS, int uMaskAll ) |
| { |
| int m, c, v; |
| for ( m = c = v = 0; v < nVarsS; v++ ) |
| if ( !((uMaskAll >> v) & 1) ) // not shared bound set variable |
| { |
| if ( (g >> v) & 1 ) |
| m |= (1 << c); |
| c++; |
| } |
| assert( c >= 2 ); |
| p[m>>6] |= (((word)1)<<(m & 63)); |
| } |
| static inline int Dau_DecCheckSet5( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec ) |
| { |
| int fFound0 = 0, fFound1 = 0; |
| int g, gMax = (1 << (nVars - nVarsF)); |
| int Shift = 6 - nVarsF, Mask = (1 << Shift) - 1; |
| word Mask2 = (((word)1) << (1 << nVarsF)) - 1; |
| word Cof0 = 0, Cof1 = 0, Value; |
| assert( nVarsF >= 1 && nVarsF <= 5 ); |
| if ( pDec ) *pDec = 0; |
| for ( g = 0; g < gMax; g++ ) |
| if ( (g & uMaskAll) == uMaskValue ) // this minterm g matches shared variable minterm uMaskValue |
| { |
| Value = (p[g>>Shift] >> ((g&Mask)<<nVarsF)) & Mask2; |
| if ( !fFound0 ) |
| Cof0 = Value, fFound0 = 1; |
| else if ( Cof0 == Value ) |
| continue; |
| else if ( !fFound1 ) |
| { |
| Cof1 = Value, fFound1 = 1; |
| if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll ); |
| } |
| else if ( Cof1 == Value ) |
| { |
| if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll ); |
| continue; |
| } |
| else |
| return 0; |
| } |
| if ( pCof0 ) |
| { |
| assert( fFound0 ); |
| Cof1 = fFound1 ? Cof1 : Cof0; |
| *pCof0 = Abc_Tt6Stretch( Cof0, nVarsF ); |
| *pCof1 = Abc_Tt6Stretch( Cof1, nVarsF ); |
| } |
| return 1; |
| } |
| static inline int Dau_DecCheckSet6( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec ) |
| { |
| int fFound0 = 0, fFound1 = 0; |
| int g, gMax = (1 << (nVars - nVarsF)); |
| int nWords = Abc_TtWordNum(nVarsF); |
| word * Cof0 = NULL, * Cof1 = NULL; |
| assert( nVarsF >= 6 && nVarsF <= nVars - 2 ); |
| if ( pDec ) *pDec = 0; |
| for ( g = 0; g < gMax; g++ ) |
| if ( (g & uMaskAll) == uMaskValue ) |
| { |
| if ( !fFound0 ) |
| Cof0 = p + g * nWords, fFound0 = 1; |
| else if ( !memcmp(Cof0, p + g * nWords, sizeof(word) * nWords) ) |
| continue; |
| else if ( !fFound1 ) |
| { |
| Cof1 = p + g * nWords, fFound1 = 1; |
| if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll ); |
| } |
| else if ( !memcmp(Cof1, p + g * nWords, sizeof(word) * nWords) ) |
| { |
| if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll ); |
| continue; |
| } |
| else |
| return 0; |
| } |
| if ( pCof0 ) |
| { |
| assert( fFound0 ); |
| Cof1 = fFound1 ? Cof1 : Cof0; |
| memcpy( pCof0, Cof0, sizeof(word) * nWords ); |
| memcpy( pCof1, Cof1, sizeof(word) * nWords ); |
| } |
| return 1; |
| } |
| static inline int Dau_DecCheckSetAny( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec ) |
| { |
| assert( nVarsF >= 1 && nVarsF <= nVars - 2 ); |
| if ( nVarsF < 6 ) |
| return Dau_DecCheckSet5( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec ); |
| else |
| return Dau_DecCheckSet6( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec ); |
| } |
| int Dau_DecCheckSetTopOld( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word ** pCof0, word ** pCof1, word ** pDec ) |
| { |
| int i, pVarsS[16]; |
| int v, m, mMax = (1 << nVarsS), uMaskValue; |
| assert( nVars >= 3 && nVars <= 16 ); |
| assert( nVars == nVarsF + nVarsB ); |
| assert( nVarsF >= 1 && nVarsF <= nVars - 2 ); |
| assert( nVarsB >= 2 && nVarsB <= nVars - 1 ); |
| assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 ); |
| if ( nVarsS == 0 ) |
| return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 ); |
| // collect shared variables |
| assert( maskS > 0 && maskS < (1 << nVarsB) ); |
| for ( i = 0, v = 0; v < nVarsB; v++ ) |
| if ( (maskS >> v) & 1 ) |
| pVarsS[i++] = v; |
| assert( i == nVarsS ); |
| // go through shared set minterms |
| for ( m = 0; m < mMax; m++ ) |
| { |
| // generate share set mask |
| uMaskValue = 0; |
| for ( v = 0; v < nVarsS; v++ ) |
| if ( (m >> v) & 1 ) |
| uMaskValue |= (1 << pVarsS[v]); |
| assert( (maskS & uMaskValue) == uMaskValue ); |
| // check decomposition |
| if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) ) |
| return 0; |
| } |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Variable sets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned Dau_DecCreateSet( int * pVarsB, int sizeB, int maskS ) |
| { |
| unsigned uSet = 0; int v; |
| for ( v = 0; v < sizeB; v++ ) |
| { |
| uSet |= (1 << (pVarsB[v] << 1)); |
| if ( (maskS >> v) & 1 ) |
| uSet |= (1 << ((pVarsB[v] << 1)+1)); |
| } |
| return uSet; |
| } |
| static inline int Dau_DecSetHas01( unsigned Mask ) |
| { |
| return (Mask & ((~Mask) >> 1) & 0x55555555); |
| } |
| static inline int Dau_DecSetIsContained( Vec_Int_t * vSets, unsigned New ) |
| // Old=abcD contains New=abcDE |
| // Old=abcD contains New=abCD |
| { |
| unsigned Old; |
| int i, Entry; |
| Vec_IntForEachEntry( vSets, Entry, i ) |
| { |
| Old = (unsigned)Entry; |
| if ( (Old & ~New) == 0 && !Dau_DecSetHas01(~Old & New)) |
| return 1; |
| } |
| return 0; |
| } |
| void Dau_DecSortSet( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree ) |
| { |
| int v; |
| int nUnique = 0, nShared = 0, nFree = 0; |
| for ( v = 0; v < nVars; v++ ) |
| { |
| int Value = ((set >> (v << 1)) & 3); |
| if ( Value == 1 ) |
| nUnique++; |
| else if ( Value == 3 ) |
| nShared++; |
| else if ( Value == 0 ) |
| nFree++; |
| else assert( 0 ); |
| } |
| *pnUnique = nUnique; |
| *pnShared = nShared; |
| *pnFree = nFree; |
| } |
| void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine ) |
| { |
| int v, Counter = 0; |
| int nUnique = 0, nShared = 0, nFree = 0; |
| Dau_DecSortSet( set, nVars, &nUnique, &nShared, &nFree ); |
| printf( "S =%2d D =%2d C =%2d ", nShared, nUnique+nShared, nShared+nFree+1 ); |
| |
| printf( "x=" ); |
| for ( v = 0; v < nVars; v++ ) |
| { |
| int Value = ((set >> (v << 1)) & 3); |
| if ( Value == 1 ) |
| printf( "%c", 'a' + v ), Counter++; |
| else if ( Value == 3 ) |
| printf( "%c", 'A' + v ), Counter++; |
| else assert( Value == 0 ); |
| } |
| printf( " y=x" ); |
| for ( v = 0; v < nVars; v++ ) |
| { |
| int Value = ((set >> (v << 1)) & 3); |
| if ( Value == 0 ) |
| printf( "%c", 'a' + v ), Counter++; |
| else if ( Value == 3 ) |
| printf( "%c", 'A' + v ), Counter++; |
| } |
| for ( ; Counter < 15; Counter++ ) |
| printf( " " ); |
| if ( fNewLine ) |
| printf( "\n" ); |
| } |
| unsigned Dau_DecReadSet( char * pStr ) |
| { |
| unsigned uSet = 0; int v; |
| for ( v = 0; pStr[v]; v++ ) |
| { |
| if ( pStr[v] >= 'a' && pStr[v] <= 'z' ) |
| uSet |= (1 << ((pStr[v] - 'a') << 1)); |
| else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' ) |
| uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1)); |
| else break; |
| } |
| return uSet; |
| } |
| void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars ) |
| { |
| int i, Entry; |
| printf( "The %d-variable set family contains %d sets:\n", nVars, Vec_IntSize(vSets) ); |
| Vec_IntForEachEntry( vSets, Entry, i ) |
| Dau_DecPrintSet( (unsigned)Entry, nVars, 1 ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find decomposable bound-sets of the given function.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB, int sizeB ) |
| { |
| int v, c = 0; |
| for ( v = 0; v < nVars; v++ ) |
| if ( !((maskB >> v) & 1) ) |
| Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ ); |
| assert( c == nVars - sizeB ); |
| } |
| Vec_Int_t * Dau_DecFindSets_int( word * pInit, int nVars, int * pSched[16] ) |
| { |
| Vec_Int_t * vSets = Vec_IntAlloc( 32 ); |
| int V2P[16], P2V[16], pVarsB[16]; |
| int Limit = (1 << nVars); |
| int c, v, sizeB, sizeS, maskB, maskS; |
| unsigned setMixed; |
| word p[1<<10]; |
| memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) ); |
| for ( v = 0; v < nVars; v++ ) |
| assert( Abc_TtHasVar( p, nVars, v ) ); |
| // initialize permutation |
| for ( v = 0; v < nVars; v++ ) |
| V2P[v] = P2V[v] = v; |
| // iterate through bound sets of each size in increasing order |
| for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size |
| for ( maskB = 0; maskB < Limit; maskB++ ) // bound set |
| if ( Abc_TtBitCount16(maskB) == sizeB ) |
| { |
| // permute variables to have bound set on top |
| Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB ); |
| // collect bound set vars on levels nVars-sizeB to nVars-1 |
| for ( c = 0; c < sizeB; c++ ) |
| pVarsB[c] = P2V[nVars-sizeB+c]; |
| // check disjoint |
| // if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) ) |
| if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, pSched[sizeB], NULL, NULL) ) |
| { |
| Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) ); |
| continue; |
| } |
| if ( sizeB == 2 ) |
| continue; |
| // iterate through shared sets of each size in the increasing order |
| for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ ) // shared set size |
| if ( sizeS <= 3 ) |
| // sizeS = 1; |
| for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set |
| if ( Abc_TtBitCount16(maskS) == sizeS ) |
| { |
| setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS ); |
| // printf( "Considering %10d ", setMixed ); |
| // Dau_DecPrintSet( setMixed, nVars ); |
| // check if it exists |
| if ( Dau_DecSetIsContained(vSets, setMixed) ) |
| continue; |
| // check if it can be added |
| // if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) ) |
| if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, pSched[sizeB], NULL, NULL) ) |
| Vec_IntPush( vSets, setMixed ); |
| } |
| } |
| return vSets; |
| } |
| Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars ) |
| { |
| Vec_Int_t * vSets; |
| int v, * pSched[16] = {NULL}; |
| for ( v = 2; v < nVars; v++ ) |
| pSched[v] = Extra_GreyCodeSchedule( v ); |
| vSets = Dau_DecFindSets_int( pInit, nVars, pSched ); |
| for ( v = 2; v < nVars; v++ ) |
| ABC_FREE( pSched[v] ); |
| return vSets; |
| } |
| void Dau_DecFindSetsTest2() |
| { |
| Vec_Int_t * vSets; |
| word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]); |
| word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]); |
| word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1); |
| // word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2) |
| // word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct |
| // word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000 |
| // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) |
| // word t = ABC_CONST(0x7F00000000000000); // (!(abc)def) |
| int nVars = 5; |
| |
| vSets = Dau_DecFindSets( &t, nVars ); |
| Dau_DecPrintSets( vSets, nVars ); |
| Vec_IntFree( vSets ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Replaces variables in the string.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dau_DecVarReplace( char * pStr, int * pPerm, int nVars ) |
| { |
| int v; |
| for ( v = 0; pStr[v]; v++ ) |
| if ( pStr[v] >= 'a' && pStr[v] <= 'z' ) |
| { |
| assert( pStr[v] - 'a' < nVars ); |
| pStr[v] = 'a' + pPerm[pStr[v] - 'a']; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Decomposes with the given bound-set.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dau_DecDecomposeSet( word * pInit, int nVars, unsigned uSet, word * pComp, word * pDec, int * pPermC, int * pPermD, int * pnVarsC, int * pnVarsD, int * pnVarsS ) |
| { |
| word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64]; |
| word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD; |
| int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16]; |
| int nVarsU = 0, nVarsS = 0, nVarsF = 0; |
| int nWords = Abc_TtWordNum(nVars); |
| int v, d, c, Status, nDecs; |
| assert( nVars <= 16 ); |
| for ( v = 0; v < nVars; v++ ) |
| V2P[v] = P2V[v] = v; |
| memcpy( p, pInit, sizeof(word) * nWords ); |
| // sort variables |
| for ( v = 0; v < nVars; v++ ) |
| { |
| int Value = (uSet >> (v<<1)) & 3; |
| if ( Value == 0 ) |
| pVarsF[nVarsF++] = v; |
| else if ( Value == 1 ) |
| pVarsU[nVarsU++] = v; |
| else if ( Value == 3 ) |
| pVarsS[nVarsS++] = v; |
| else assert(0); |
| } |
| assert( nVarsS >= 0 && nVarsS <= 6 ); |
| assert( nVarsF + nVarsS + 1 <= 6 ); |
| assert( nVarsU + nVarsS <= 6 ); |
| // init space for decomposition functions |
| nDecs = (1 << nVarsS); |
| for ( d = 0; d < nDecs; d++ ) |
| { |
| pCof0[d] = Cof0 + d; |
| pCof1[d] = Cof1 + d; |
| pDecs[d] = Decs + d; |
| } |
| // permute variables |
| c = 0; |
| for ( v = 0; v < nVarsF; v++ ) |
| Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ ); |
| for ( v = 0; v < nVarsS; v++ ) |
| Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ ); |
| for ( v = 0; v < nVarsU; v++ ) |
| Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ ); |
| assert( c == nVars ); |
| // check decomposition |
| Status = Dau_DecCheckSetTopOld( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs ); |
| if ( !Status ) |
| return 0; |
| // compute cofactors |
| assert( nVarsF + nVarsS < 6 ); |
| for ( d = 0; d < nDecs; d++ ) |
| { |
| Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]); |
| pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU ); |
| } |
| // compute the resulting functions |
| pComp[0] = 0; |
| pDec[0] = 0; |
| for ( d = 0; d < nDecs; d++ ) |
| { |
| // compute minterms for composition/decomposition function |
| MintC = MintD = ~((word)0); |
| for ( v = 0; v < nVarsS; v++ ) |
| { |
| MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v]; |
| MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v]; |
| } |
| // derive functions |
| pComp[0] |= MintC & Cof[d]; |
| pDec[0] |= MintD & pDecs[d][0]; |
| } |
| // derive variable permutations |
| if ( pPermC ) |
| { |
| for ( v = 0; v < nVarsF; v++ ) |
| pPermC[v] = pVarsF[v]; |
| for ( v = 0; v < nVarsS; v++ ) |
| pPermC[nVarsF+v] = pVarsS[v]; |
| pPermC[nVarsF + nVarsS] = nVars; |
| } |
| if ( pPermD ) |
| { |
| for ( v = 0; v < nVarsU; v++ ) |
| pPermD[v] = pVarsU[v]; |
| for ( v = 0; v < nVarsS; v++ ) |
| pPermD[nVarsU+v] = pVarsS[v]; |
| } |
| if ( pnVarsC ) |
| *pnVarsC = nVarsF + nVarsS + 1; |
| if ( pnVarsD ) |
| *pnVarsD = nVarsU + nVarsS; |
| if ( pnVarsS ) |
| *pnVarsS = nVarsS; |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Testing procedures.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD ) |
| { |
| word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16 |
| int nWordsC = Abc_TtWordNum(nVars+1); |
| int nWordsD = Abc_TtWordNum(nVars); |
| assert( nVars < 16 ); |
| memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC ); |
| memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD ); |
| if ( nVars >= 6 ) |
| { |
| assert( nWordsD >= 1 ); |
| assert( nWordsC > 1 ); |
| Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD ); |
| } |
| else |
| { |
| word pC0 = Abc_Tt6Stretch( pC[0], nVars ); |
| word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars ); |
| Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD ); |
| } |
| if ( !Abc_TtEqual(pInit, pRes, nWordsD) ) |
| printf( " Verification failed" ); |
| // else |
| // printf( " Verification successful" ); |
| printf( "\n" ); |
| return 1; |
| } |
| int Dau_DecPerform6( word * p, int nVars, unsigned uSet ) |
| { |
| word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD; |
| char pDsdC[1000], pDsdD[1000]; |
| int pPermC[16], pPermD[16]; |
| int nVarsC, nVarsD, nVarsS, nVarsU, nVarsF, nPairs; |
| int i, m, v, status, ResC, ResD, Counter = 0; |
| status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec0, pPermC, pPermD, &nVarsC, &nVarsD, &nVarsS ); |
| if ( !status ) |
| { |
| printf( " Decomposition does not exist\n" ); |
| return 0; |
| } |
| nVarsU = nVarsD - nVarsS; |
| nVarsF = nVarsC - nVarsS - 1; |
| tComp0 = Abc_Tt6Cofactor0( tComp, nVarsF + nVarsS ); |
| tComp1 = Abc_Tt6Cofactor1( tComp, nVarsF + nVarsS ); |
| nPairs = 1 << (1 << nVarsS); |
| for ( i = 0; i < nPairs; i++ ) |
| { |
| if ( i & 1 ) |
| continue; |
| // create miterms with this polarity |
| FuncC = FuncD = 0; |
| for ( m = 0; m < (1 << nVarsS); m++ ) |
| { |
| word MintC, MintD; |
| if ( !((i >> m) & 1) ) |
| continue; |
| MintC = MintD = ~(word)0; |
| for ( v = 0; v < nVarsS; v++ ) |
| { |
| MintC &= ((m >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v]; |
| MintD &= ((m >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v]; |
| } |
| FuncC |= MintC; |
| FuncD |= MintD; |
| } |
| // uncomplement given variables |
| tComp = (~s_Truths6[nVarsF + nVarsS] & ((tComp0 & ~FuncC) | (tComp1 & FuncC))) | (s_Truths6[nVarsF + nVarsS] & ((tComp1 & ~FuncC) | (tComp0 & FuncC))); |
| tDec = tDec0 ^ FuncD; |
| // decompose |
| ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC ); |
| ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD ); |
| // replace variables |
| Dau_DecVarReplace( pDsdD, pPermD, nVarsD ); |
| Dau_DecVarReplace( pDsdC, pPermC, nVarsC ); |
| // report |
| // printf( " " ); |
| printf( "%3d : ", Counter++ ); |
| printf( "%24s ", pDsdD ); |
| printf( "%24s ", pDsdC ); |
| Dau_DecVerify( p, nVars, pDsdC, pDsdD ); |
| } |
| return 1; |
| } |
| |
| int Dau_DecPerform( word * pInit, int nVars, unsigned uSet ) |
| { |
| word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words |
| char pDsdC[5000], pDsdD[5000]; // at most 2^12 hex digits |
| int nVarsU, nVarsS, nVarsF, nVarsC = 0, nVarsD = 0; |
| int V2P[16], P2V[16], pPermC[16], pPermD[16], * pSched; |
| int v, i, status, ResC, ResD; |
| int nWords = Abc_TtWordNum(nVars); |
| assert( nVars <= 16 ); |
| // backup the function |
| memcpy( p, pInit, sizeof(word) * nWords ); |
| // get variable numbers |
| Dau_DecSortSet( uSet, nVars, &nVarsU, &nVarsS, &nVarsF ); |
| // permute function and order variables |
| for ( v = 0; v < nVars; v++ ) |
| V2P[v] = P2V[v] = v; |
| for ( i = v = 0; v < nVars; v++ ) |
| if ( ((uSet >> (v<<1)) & 3) == 0 ) // free first |
| Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v; |
| for ( v = 0; v < nVars; v++ ) |
| if ( ((uSet >> (v<<1)) & 3) == 3 ) // share second |
| Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v; |
| pPermC[nVarsC++] = nVars; |
| for ( v = 0; v < nVars; v++ ) |
| if ( ((uSet >> (v<<1)) & 3) == 1 ) // unique last |
| Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermD[nVarsD++] = v; |
| for ( v = 0; v < nVarsS; v++ ) |
| pPermD[nVarsD++] = pPermC[nVarsF+v]; |
| assert( nVarsD == nVarsU + nVarsS ); |
| assert( nVarsC == nVarsF + nVarsS + 1 ); |
| assert( i == nVars ); |
| // decompose |
| pSched = Extra_GreyCodeSchedule( nVarsU + nVarsS ); |
| memset( pDec, 0, sizeof(word) * Abc_TtWordNum(nVarsD) ); |
| memset( pComp, 0, sizeof(word) * Abc_TtWordNum(nVarsC) ); |
| status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsU + nVarsS, nVarsS, nVarsS ? Abc_InfoMask(nVarsS) : 0, pSched, pDec, pComp ); |
| ABC_FREE( pSched ); |
| if ( !status ) |
| { |
| printf( " Decomposition does not exist\n" ); |
| return 0; |
| } |
| // Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" ); |
| // Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" ); |
| // Kit_DsdPrintFromTruth( (unsigned *)pComp, 6 ); printf( "\n" ); |
| // Kit_DsdPrintFromTruth( (unsigned *)pDec, 6 ); printf( "\n" ); |
| // decompose |
| ResC = Dau_DsdDecompose( pComp, nVarsC, 0, 1, pDsdC ); |
| ResD = Dau_DsdDecompose( pDec, nVarsD, 0, 1, pDsdD ); |
| // replace variables |
| Dau_DecVarReplace( pDsdD, pPermD, nVarsD ); |
| Dau_DecVarReplace( pDsdC, pPermC, nVarsC ); |
| // report |
| printf( " " ); |
| printf( "%3d : ", 0 ); |
| printf( "%24s ", pDsdD ); |
| printf( "%24s ", pDsdC ); |
| Dau_DecVerify( pInit, nVars, pDsdC, pDsdD ); |
| return 1; |
| } |
| void Dau_DecTrySets( word * pInit, int nVars, int fVerbose ) |
| { |
| Vec_Int_t * vSets; |
| int i, Entry; |
| assert( nVars <= 16 ); |
| vSets = Dau_DecFindSets( pInit, nVars ); |
| if ( !fVerbose ) |
| { |
| Vec_IntFree( vSets ); |
| return; |
| } |
| Dau_DsdPrintFromTruth( pInit, nVars ); |
| printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) ); |
| Vec_IntForEachEntry( vSets, Entry, i ) |
| { |
| unsigned uSet = (unsigned)Entry; |
| printf( "Set %4d : ", i ); |
| if ( nVars > 6 ) |
| { |
| Dau_DecPrintSet( uSet, nVars, 0 ); |
| Dau_DecPerform( pInit, nVars, uSet ); |
| } |
| else |
| { |
| Dau_DecPrintSet( uSet, nVars, 1 ); |
| Dau_DecPerform6( pInit, nVars, uSet ); |
| } |
| } |
| Vec_IntFree( vSets ); |
| // printf( "\n" ); |
| } |
| |
| void Dau_DecFindSetsTest3() |
| { |
| word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]); |
| word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]); |
| word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1); |
| // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) |
| int nVars = 6; |
| char * pStr = "Bcd"; |
| // char * pStr = "Abcd"; |
| // char * pStr = "ab"; |
| unsigned uSet = Dau_DecReadSet( pStr ); |
| Dau_DecPerform6( &t, nVars, uSet ); |
| } |
| |
| void Dau_DecFindSetsTest() |
| { |
| int nVars = 6; |
| // word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]); |
| // word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]); |
| // word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1); |
| // word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2) |
| // word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct |
| // word t = ABC_CONST(0x00000000901FFFFF); // some funct |
| word t = ABC_CONST(0x000030F00D0D3FFF); // some funct |
| // word t = ABC_CONST(0x00000000690006FF); // some funct |
| // word t = ABC_CONST(0x7000F80007FF0FFF); // some funct |
| // word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var |
| // word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000 |
| // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) |
| // word t = ABC_CONST(0x7F00000000000000); // (!(abc)def) |
| Dau_DecTrySets( &t, nVars, 1 ); |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
