From e6e6a3cf9ecfccf71cba45273ea866e7e2526f0a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Oct 2011 17:00:59 +0700 Subject: Changes to the matching procedure. --- src/map/if/ifDec16.c | 800 +++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 615 insertions(+), 185 deletions(-) (limited to 'src/map/if/ifDec16.c') diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c index 5e988ae5..3902f053 100644 --- a/src/map/if/ifDec16.c +++ b/src/map/if/ifDec16.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [ifDec10f.c] + FileName [ifDec16.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - November 21, 2006.] - Revision [$Id: ifDec10f.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + Revision [$Id: ifDec16.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -36,7 +36,7 @@ struct If_Grp_t_ { char nVars; char nMyu; - char pVars[6]; + char pVars[CLU_VAR_MAX]; }; // the bit count for the first 256 integer numbers @@ -67,36 +67,33 @@ static word Truth6[6] = { 0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 }; -static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX]; +static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX] = {{0}}; extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); -// group representation (MSB <-> LSB) -// nVars | nMyu | v5 | v4 | v3 | v2 | v1 | v0 -// if nCofs > 2, v0 is the shared variable //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -void If_CluInitTruthTables() -{ - int i, k; - assert( CLU_VAR_MAX <= 16 ); - for ( i = 0; i < 6; i++ ) - for ( k = 0; k < CLU_WRD_MAX; k++ ) - TruthAll[i][k] = Truth6[i]; - for ( i = 6; i < CLU_VAR_MAX; i++ ) - for ( k = 0; k < CLU_WRD_MAX; k++ ) - TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0; -} - // variable permutation for large functions static inline int If_CluWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); } +static inline void If_CluClear( word * pIn, int nVars ) +{ + int w, nWords = If_CluWordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pIn[w] = 0; +} +static inline void If_CluFill( word * pIn, int nVars ) +{ + int w, nWords = If_CluWordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pIn[w] = ~0; +} static inline void If_CluCopy( word * pOut, word * pIn, int nVars ) { int w, nWords = If_CluWordNum( nVars ); @@ -111,6 +108,42 @@ static inline int If_CluEqual( word * pOut, word * pIn, int nVars ) return 0; return 1; } +static inline void If_CluAnd( word * pRes, word * pIn1, word * pIn2, int nVars ) +{ + int w, nWords = If_CluWordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pRes[w] = pIn1[w] & pIn2[w]; +} +static inline void If_CluSharp( word * pRes, word * pIn1, word * pIn2, int nVars ) +{ + int w, nWords = If_CluWordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pRes[w] = pIn1[w] & ~pIn2[w]; +} +static inline void If_CluOr( word * pRes, word * pIn1, word * pIn2, int nVars ) +{ + int w, nWords = If_CluWordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pRes[w] = pIn1[w] | pIn2[w]; +} +static inline word If_CluAdjust( word t, int nVars ) +{ + assert( nVars >= 0 && nVars < 6 ); + t &= (1 << (1 << nVars)) - 1; + if ( nVars == 0 ) + t |= t << (1<nVars ); + printf( "Myu = %d ", g->nMyu ); + for ( i = 0; i < g->nVars; i++ ) + printf( "%d ", g->pVars[i] ); + printf( "\n" ); +} + +void If_CluPrintConfig( int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth ) +{ + assert( r->nVars == nVars - g->nVars + 1 + (g->nMyu > 2) ); + If_CluPrintGroup( g ); + if ( g->nVars < 6 ) + BStruth = If_CluAdjust( BStruth, g->nVars ); + Kit_DsdPrintFromTruth( (unsigned *)&BStruth, g->nVars ); + printf( "\n" ); + If_CluPrintGroup( r ); + if ( r->nVars < 6 ) + pFStruth[0] = If_CluAdjust( pFStruth[0], r->nVars ); + Kit_DsdPrintFromTruth( (unsigned *)pFStruth, r->nVars ); + printf( "\n" ); +} + + +void If_CluInitTruthTables() +{ + int i, k; + assert( CLU_VAR_MAX <= 16 ); + for ( i = 0; i < 6; i++ ) + for ( k = 0; k < CLU_WRD_MAX; k++ ) + TruthAll[i][k] = Truth6[i]; + for ( i = 6; i < CLU_VAR_MAX; i++ ) + for ( k = 0; k < CLU_WRD_MAX; k++ ) + TruthAll[i][k] = ((k >> (i-6)) & 1) ? ~0 : 0; + +// Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" ); +// Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" ); +} + + +// verification +static void If_CluComposeLut( int nVars, If_Grp_t * g, word * t, word f[6][CLU_WRD_MAX], word * r ) +{ + word c[CLU_WRD_MAX]; + int m, v; + If_CluClear( r, nVars ); + for ( m = 0; m < (1<nVars); m++ ) + { + if ( !((t[m >> 6] >> (m & 63)) & 1) ) + continue; + If_CluFill( c, nVars ); + for ( v = 0; v < g->nVars; v++ ) + if ( (m >> v) & 1 ) + If_CluAnd( c, c, f[v], nVars ); + else + If_CluSharp( c, c, f[v], nVars ); + If_CluOr( r, r, c, nVars ); + } +} +void If_CluVerify( word * pF, int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth ) +{ + word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX]; + int i; + assert( g->nVars <= 6 && r->nVars <= 6 ); + + if ( TruthAll[0][0] == 0 ) + If_CluInitTruthTables(); + + for ( i = 0; i < g->nVars; i++ ) + If_CluCopy( pTTFans[i], TruthAll[g->pVars[i]], nVars ); + If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire ); + + for ( i = 0; i < r->nVars; i++ ) + if ( r->pVars[i] == nVars ) + If_CluCopy( pTTFans[i], pTTWire, nVars ); + else + If_CluCopy( pTTFans[i], TruthAll[r->pVars[i]], nVars ); + If_CluComposeLut( nVars, r, pFStruth, pTTFans, pTTRes ); + + if ( !If_CluEqual(pTTRes, pF, nVars) ) + { + printf( "\n" ); + If_CluPrintConfig( nVars, g, r, BStruth, pFStruth ); + Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" ); + printf( "Verification FAILED!\n" ); + } +// else +// printf( "Verification succeed!\n" ); +} + + // moves one var (v) to the given position (p) void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p ) { word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp; int iPlace0, iPlace1, Count = 0; assert( v >= 0 && v < nVars ); - if ( Var2Pla[v] <= p ) + while ( Var2Pla[v] < p ) { - while ( Var2Pla[v] < p ) - { - iPlace0 = Var2Pla[v]; - iPlace1 = Var2Pla[v]+1; - If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars ); - pTemp = pIn; pIn = pOut, pOut = pTemp; - Var2Pla[Pla2Var[iPlace0]]++; - Var2Pla[Pla2Var[iPlace1]]--; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Count++; - } + iPlace0 = Var2Pla[v]; + iPlace1 = Var2Pla[v]+1; + If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars ); + pTemp = pIn; pIn = pOut, pOut = pTemp; + Var2Pla[Pla2Var[iPlace0]]++; + Var2Pla[Pla2Var[iPlace1]]--; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Count++; } - else + while ( Var2Pla[v] > p ) { - while ( Var2Pla[v] > p ) - { - iPlace0 = Var2Pla[v]-1; - iPlace1 = Var2Pla[v]; - If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars ); - pTemp = pIn; pIn = pOut, pOut = pTemp; - Var2Pla[Pla2Var[iPlace0]]++; - Var2Pla[Pla2Var[iPlace1]]--; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Count++; - } + iPlace0 = Var2Pla[v]-1; + iPlace1 = Var2Pla[v]; + If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars ); + pTemp = pIn; pIn = pOut, pOut = pTemp; + Var2Pla[Pla2Var[iPlace0]]++; + Var2Pla[Pla2Var[iPlace1]]--; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Count++; } if ( Count & 1 ) If_CluCopy( pF, pIn, nVars ); @@ -199,64 +321,86 @@ void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[g->nVars - 1 - v], nVars - 1 - v ); } -// return the number of cofactors w.r.t. the topmost vars (nBSsize) -int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift, word * pCofs[2] ) +// reverses the variable order +void If_CluReverseOrder( word * pF, int nVars, int * V2P, int * P2V ) { - word iCofs[64], iCof; - int i, c, w, nMints = (1 << nBSsize), nCofs; - - assert( nBSsize < nVars ); - assert( nBSsize >= 3 && nBSsize <= 6 ); + int v; + for ( v = 0; v < nVars; v++ ) + If_CluMoveVar( pF, nVars, V2P, P2V, P2V[0], nVars - 1 - v ); +} - if ( nVars - nBSsize >= 6 ) +// return the number of cofactors w.r.t. the topmost vars (nBSsize) +int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift, word pCofs[3][CLU_WRD_MAX/4] ) +{ + word iCofs[128], iCof, Result = 0; + word * pCofA, * pCofB; + int nMints = (1 << nBSsize); + int i, c, w, nCofs; + assert( nBSsize >= 2 && nBSsize <= 7 && nBSsize < nVars ); + if ( nVars - nBSsize < 6 ) { - word * pCofA, * pCofB; - int nWords = (1 << (nVars - nBSsize - 6)); - assert( nWords * nMints == If_CluWordNum(nVars) ); + int nShift = (1 << (nVars - nBSsize)); + word Mask = ((((word)1) << nShift) - 1); for ( nCofs = i = 0; i < nMints; i++ ) { + iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask; for ( c = 0; c < nCofs; c++ ) - { - pCofA = pF + i * nWords; - pCofB = pF + iCofs[c] * nWords; - for ( w = 0; w < nWords; w++ ) - if ( pCofA[w] != pCofB[w] ) - break; - if ( w == nWords ) + if ( iCof == iCofs[c] ) break; - } if ( c == nCofs ) - iCofs[nCofs++] = i; + iCofs[nCofs++] = iCof; + if ( pCofs && iCof != iCofs[0] ) + Result |= (((word)1) << i); if ( nCofs == 5 ) break; } - if ( nCofs == 2 && pCofs ) + if ( nCofs <= 2 && pCofs ) { - for ( c = 0; c < nCofs; c++ ) - { - word * pCofA = pF + iCofs[c] * nWords; - for ( w = 0; w < nWords; w++ ) - pCofs[c][w] = pCofA[w]; - } + assert( nBSsize <= 6 ); + pCofs[0][0] = iCofs[0]; + pCofs[1][0] = (nCofs == 2) ? iCofs[1] : iCofs[0]; + pCofs[2][0] = Result; } } else { - int nShift = (1 << (nVars - nBSsize)); - word Mask = ((((word)1) << nShift) - 1); + int nWords = If_CluWordNum( nVars - nBSsize ); + assert( nWords * nMints == If_CluWordNum(nVars) ); for ( nCofs = i = 0; i < nMints; i++ ) { - iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask; + pCofA = pF + i * nWords; for ( c = 0; c < nCofs; c++ ) - if ( iCof == iCofs[c] ) + { + pCofB = pF + iCofs[c] * nWords; + for ( w = 0; w < nWords; w++ ) + if ( pCofA[w] != pCofB[w] ) + break; + if ( w == nWords ) break; + } if ( c == nCofs ) - iCofs[nCofs++] = iCof; + iCofs[nCofs++] = i; + if ( pCofs ) + { + assert( nBSsize <= 6 ); + pCofB = pF + iCofs[0] * nWords; + for ( w = 0; w < nWords; w++ ) + if ( pCofA[w] != pCofB[w] ) + break; + if ( w != nWords ) + Result |= (((word)1) << i); + } if ( nCofs == 5 ) break; } + if ( nCofs <= 2 && pCofs ) + { + If_CluCopy( pCofs[0], pF + iCofs[0] * nWords, nVars - nBSsize ); + If_CluCopy( pCofs[1], pF + ((nCofs == 2) ? iCofs[1] : iCofs[0]) * nWords, nVars - nBSsize ); + pCofs[2][0] = Result; + } } - assert( nCofs >= 2 && nCofs <= 5 ); + assert( nCofs >= 1 && nCofs <= 5 ); return nCofs; } @@ -272,7 +416,6 @@ void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift); pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift); } - return; } else { @@ -288,70 +431,227 @@ void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 pCof0 += 2*Step; pCof1 += 2*Step; } - return; } } -// derives non-disjoint decomposition (assumes the shared var in pG->pVars[pG->nVars-1] -word If_CluDeriveNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * pG ) +// returns 1 if we have special case of cofactors; otherwise, returns 0 +int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar ) { - /* - word Truth, Truth0, Truth1; - word Cof[2][CLU_WRD_MAX], Cof0[2][CLU_WRD_MAX], Cof1[2][CLU_WRD_MAX]; - int i, nFSvars, nFSHalfBits, nBSHalfBits; - assert( pG->nVars >= 3 && pG->nVar <= 6 ); - assert( pG->nMyu == 3 || pG->nMyu == 4 ); - - If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, pG ); - - If_CluCofactors( pF, nVars, nVars - 1, Cof[0], Cof[1] ); - - assert( 2 >= If_Dec6CofCount2(c0) ); - assert( 2 >= If_Dec6CofCount2(c1) ); - - assert( 2 >= If_CluCountCofs( Cof[0], nVars - 1, pG->nVars - 1, 0 ) ); - assert( 2 >= If_CluCountCofs( Cof[1], nVars - 1, pG->nVars - 1, 0 ) ); + word Cof0, Cof1; + int State[6] = {0}; + int i, nWords = If_CluWordNum( nVars ); + assert( iVar < nVars ); + if ( iVar < 6 ) + { + int Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + { + Cof0 = (pF[i] & ~Truth6[iVar]); + Cof1 = ((pF[i] & Truth6[iVar]) >> Shift); + + if ( Cof0 == 0 ) + State[0]++; + else if ( Cof0 == ~Truth6[iVar] ) + State[1]++; + else if ( Cof1 == 0 ) + State[2]++; + else if ( Cof1 == ~Truth6[iVar] ) + State[3]++; + else if ( Cof0 == ~Cof1 ) + State[4]++; + else if ( Cof0 == Cof1 ) + State[5]++; + } + } + else + { + int k, Step = (1 << (iVar - 6)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + { + Cof0 = pF[i]; + Cof1 = pF[Step+i]; + + if ( Cof0 == 0 ) + State[0]++; + else if ( Cof0 == ~Truth6[iVar] ) + State[1]++; + else if ( Cof1 == 0 ) + State[2]++; + else if ( Cof1 == ~Truth6[iVar] ) + State[3]++; + else if ( Cof0 == ~Cof1 ) + State[4]++; + else if ( Cof0 == Cof1 ) + State[5]++; + } + pF += 2*Step; + } + nWords /= 2; + } + assert( State[5] != nWords ); + for ( i = 0; i < 5; i++ ) + { + assert( State[i] <= nWords ); + if ( State[i] == nWords ) + return i; + } + return -1; +} - Truth0 = If_CluExtract2Cofs( Cof[0], nVars - 1, pG->nVars - 1, &Cof0[0], &Cof0[1] ); - Truth1 = If_CluExtract2Cofs( Cof[1], nVars - 1, pG->nVars - 1, &Cof0[0], &Cof0[1] ); +// returns 1 if we have special case of cofactors; otherwise, returns 0 +If_Grp_t If_CluDecUsingCofs( word * pTruth, int nVars, int nLutLeaf ) +{ + If_Grp_t G = {0}; + word pF2[CLU_WRD_MAX], * pF = pF2; + int Var2Pla[CLU_VAR_MAX+2], Pla2Var[CLU_VAR_MAX+2]; + int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2]; + int nVarsNeeded = nVars - nLutLeaf; + int v, i, k, iVar, State; +//Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" ); + // create local copy + If_CluCopy( pF, pTruth, nVars ); + for ( k = 0; k < nVars; k++ ) + Var2Pla[k] = Pla2Var[k] = k; + // find decomposable vars + for ( i = 0; i < nVarsNeeded; i++ ) + { + for ( v = nVars - 1; v >= 0; v-- ) + { + State = If_CluDetectSpecialCaseCofs( pF, nVars, v ); + if ( State == -1 ) + continue; + // update the variable place + iVar = Pla2Var[v]; + while ( Var2Pla[iVar] < nVars - 1 ) + { + int iPlace0 = Var2Pla[iVar]; + int iPlace1 = Var2Pla[iVar]+1; + Var2Pla[Pla2Var[iPlace0]]++; + Var2Pla[Pla2Var[iPlace1]]--; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + } + // move this variable to the top + for ( k = 0; k < nVars; k++ ) + V2P[k] = P2V[k] = k; +//Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); + If_CluMoveVar( pF, nVars, V2P, P2V, v, nVars - 1 ); +//Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); + // choose cofactor to follow + iVar = nVars - 1; + if ( State == 0 || State == 1 ) // need cof1 + { + if ( iVar < 6 ) + pF[0] = (pF[0] & Truth6[iVar]) | ((pF[0] & Truth6[iVar]) >> (1 << iVar)); + else + pF += If_CluWordNum( nVars ) / 2; + } + else // need cof0 + { + if ( iVar < 6 ) + pF[0] = (pF[0] & ~Truth6[iVar]) | ((pF[0] & ~Truth6[iVar]) << (1 << iVar)); + } + // update the variable count + nVars--; + break; + } + if ( v == -1 ) + return G; + } + // create the resulting group + G.nVars = nLutLeaf; + G.nMyu = 2; + for ( v = 0; v < G.nVars; v++ ) + G.pVars[v] = Pla2Var[v]; + return G; +} - nFSHalfBits = (1 << (nVars - pG->nVars - 1)); - nBSHalfBits = (1 << (pG->nVars - 1)) - Truth = ((Truth0 && ((1 << nBSHalfBits) - 1)) << nBSHalfBits) | (Truth0 && ((1 << nBSHalfBits) - 1)) +// deriving decomposition +word If_CluDeriveDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r ) +{ + word pCofs[3][CLU_WRD_MAX/4]; + int i, RetValue, nFSset = nVars - g->nVars; + RetValue = If_CluCountCofs( pF, nVars, g->nVars, 0, pCofs ); +// assert( RetValue == 2 ); - for ( i = 0; i < 4; i++ ) - z |= (((word)Pla2Var[i+2]) << (16 + 4*i)); - z |= ((word)((Cof0[1] << 4) | Cof0[0]) << 32); - z |= ((word)((Cof1[1] << 4) | Cof1[0]) << 40); - for ( i = 0; i < 2; i++ ) - z |= (((word)Pla2Var[i]) << (48 + 4*i)); - z |= (((word)7) << (48 + 4*i++)); - z |= (((word)Pla2Var[5]) << (48 + 4*i++)); - assert( i == 4 ); - return z; - */ - return 0; + if ( nFSset < 6 ) + pF[0] = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0]; + else + { + If_CluCopy( pF, pCofs[0], nFSset ); + If_CluCopy( pF + If_CluWordNum(nFSset), pCofs[1], nFSset ); + } + // create the resulting group + if ( r ) + { + r->nVars = nFSset + 1; + r->nMyu = 0; + for ( i = 0; i < nFSset; i++ ) + r->pVars[i] = P2V[i]; + r->pVars[nFSset] = nVars; + } + return pCofs[2][0]; } +word If_CluDeriveNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r ) +{ + word pCofs[2][CLU_WRD_MAX]; + word Truth0, Truth1, Truth; + int i, nFSset = nVars - g->nVars, nFSset1 = nFSset + 1; + If_CluCofactors( pF, nVars, nVars - 1, pCofs[0], pCofs[1] ); + +// Extra_PrintHex( stdout, (unsigned *)pCofs[0], nVars ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)pCofs[1], nVars ); printf( "\n" ); + + g->nVars--; + Truth0 = If_CluDeriveDisjoint( pCofs[0], nVars - 1, V2P, P2V, g, NULL ); + Truth1 = If_CluDeriveDisjoint( pCofs[1], nVars - 1, V2P, P2V, g, NULL ); + Truth = (Truth1 << (1 << g->nVars)) | Truth0; + g->nVars++; + if ( nFSset1 < 6 ) + pF[0] = (pCofs[1][0] << (1 << nFSset1)) | pCofs[0][0]; + else + { + If_CluCopy( pF, pCofs[0], nFSset1 ); + If_CluCopy( pF + If_CluWordNum(nFSset1), pCofs[1], nFSset1 ); + } +// Extra_PrintHex( stdout, (unsigned *)&Truth0, 6 ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)&Truth1, 6 ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)&pCofs[0][0], 6 ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)&pCofs[1][0], 6 ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)&Truth, 6 ); printf( "\n" ); +// Extra_PrintHex( stdout, (unsigned *)&pF[0], 6 ); printf( "\n" ); + + // create the resulting group + r->nVars = nFSset + 2; + r->nMyu = 0; + for ( i = 0; i < nFSset; i++ ) + r->pVars[i] = P2V[i]; + r->pVars[nFSset] = nVars; + r->pVars[nFSset+1] = g->pVars[g->nVars - 1]; + return Truth; +} // check non-disjoint decomposition -int If_CluCheckNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g ) +int If_CluCheckNonDisjointGroup( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g ) { int v, i, nCofsBest2; if ( (g->nMyu == 3 || g->nMyu == 4) ) { - word pCof0[CLU_WRD_MAX]; - word pCof1[CLU_WRD_MAX]; + word pCofs[2][CLU_WRD_MAX]; // try cofactoring w.r.t. each variable for ( v = 0; v < g->nVars; v++ ) { - If_CluCofactors( pF, nVars, V2P[g->pVars[v]], pCof0, pCof1 ); - nCofsBest2 = If_CluCountCofs( pCof0, nVars, g->nVars, 0, NULL ); + If_CluCofactors( pF, nVars, V2P[g->pVars[v]], pCofs[0], pCofs[1] ); + nCofsBest2 = If_CluCountCofs( pCofs[0], nVars, g->nVars, 0, NULL ); if ( nCofsBest2 > 2 ) continue; - nCofsBest2 = If_CluCountCofs( pCof1, nVars, g->nVars, 0, NULL ); + nCofsBest2 = If_CluCountCofs( pCofs[1], nVars, g->nVars, 0, NULL ); if ( nCofsBest2 > 2 ) continue; // found good shared variable - move to the end @@ -364,25 +664,15 @@ int If_CluCheckNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t return 0; } -void If_CluPrintGroup( If_Grp_t * g ) -{ - int i; - for ( i = 0; i < g->nVars; i++ ) - printf( "%d ", g->pVars[i] ); - printf( "\n" ); - printf( "Cofs = %d", g->nMyu ); - printf( "\n" ); - printf( "Vars = %d", g->nVars ); - printf( "\n" ); -} - - + // finds a good var group (cof count < 6; vars are MSBs) If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V, int nBSsize, int fDisjoint ) { + int fVerbose = 0; + int nRounds = 2;//nBSsize; If_Grp_t G = {0}, * g = &G; int i, r, v, nCofs, VarBest, nCofsBest2; - assert( nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX ); + assert( nVars > nBSsize && nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX ); assert( nBSsize >= 3 && nBSsize <= 6 ); // start with the default group g->nVars = nBSsize; @@ -392,33 +682,39 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * // check if good enough if ( g->nMyu == 2 ) return G; - if ( If_CluCheckNonDisjoint( pF, nVars, V2P, P2V, g ) ) + if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) ) return G; - printf( "Iter %d ", -1 ); - If_CluPrintGroup( g ); + if ( fVerbose ) + { + printf( "Iter %2d ", -1 ); + If_CluPrintGroup( g ); + } // try to find better group - for ( r = 0; r < nBSsize; r++ ) + for ( r = 0; r < nRounds; r++ ) { - // find the best var to add - VarBest = P2V[nVars-1-nBSsize]; - nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); - for ( v = nVars-2-nBSsize; v >= iVarStart; v-- ) + if ( nBSsize < nVars-1 ) { - If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); - nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); - if ( nCofsBest2 >= nCofs ) + // find the best var to add + VarBest = P2V[nVars-1-nBSsize]; + nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); + for ( v = nVars-2-nBSsize; v >= iVarStart; v-- ) { - nCofsBest2 = nCofs; - VarBest = P2V[nVars-1-nBSsize]; + If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); + nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); + if ( nCofsBest2 >= nCofs ) + { + nCofsBest2 = nCofs; + VarBest = P2V[nVars-1-nBSsize]; + } } + // go back + If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); + // update best bound set + nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); + assert( nCofs == nCofsBest2 ); } - // go back - If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); - // update best bound set - nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); - assert( nCofs == nCofsBest2 ); // find the best var to remove VarBest = P2V[nVars-1-nBSsize]; @@ -447,16 +743,20 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * g->pVars[i] = P2V[nVars-nBSsize+i]; } - printf( "Iter %d ", r ); - If_CluPrintGroup( g ); + if ( fVerbose ) + { + printf( "Iter %2d ", r ); + If_CluPrintGroup( g ); + } // check if good enough if ( g->nMyu == 2 ) return G; - if ( If_CluCheckNonDisjoint( pF, nVars, V2P, P2V, g ) ) + if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) ) return G; } - assert( r == nBSsize ); + + assert( r == nRounds ); g->nVars = 0; return G; } @@ -467,7 +767,7 @@ void If_CluCheckGroup( word * pTruth, int nVars, If_Grp_t * g ) { word pF[CLU_WRD_MAX]; int v, nCofs, V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX]; - assert( g->nVars >= 3 && g->nVars <= 6 ); // vars + assert( g->nVars >= 2 && g->nVars <= 6 ); // vars assert( g->nMyu >= 2 && g->nMyu <= 4 ); // cofs // create permutation for ( v = 0; v < nVars; v++ ) @@ -500,10 +800,10 @@ void If_CluCheckPerm( word * pTruth, word * pF, int nVars, int * V2P, int * P2V for ( i = 0; i < nVars; i++ ) If_CluMoveVar( pF, nVars, V2P, P2V, i, i ); - if ( If_CluEqual( pTruth, pF, nVars ) ) - printf( "Permutation successful\n" ); - else + if ( !If_CluEqual( pTruth, pF, nVars ) ) printf( "Permutation FAILED.\n" ); +// else +// printf( "Permutation successful\n" ); } @@ -550,32 +850,92 @@ static inline int If_CluSupport( word * t, int nVars ) // returns the best group found If_Grp_t If_CluCheck( word * pTruth, int nVars, int nLutLeaf, int nLutRoot ) { - int V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX]; - word pF[CLU_WRD_MAX]; - If_Grp_t G1 = {0}; + If_Grp_t G1 = {0}, R = {0}; + word Truth, pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX]; + int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2]; int i, nSupp; assert( nVars <= CLU_VAR_MAX ); assert( nVars <= nLutLeaf + nLutRoot - 1 ); + /* + { + int pCanonPerm[32]; + short pStore[32]; + unsigned uCanonPhase; + If_CluCopy( pF, pTruth, nVars ); + uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm, pStore ); + G1.nVars = 1; + return G1; + } +*/ + // check minnimum base If_CluCopy( pF, pTruth, nVars ); + for ( i = 0; i < nVars; i++ ) + V2P[i] = P2V[i] = i; + // check support nSupp = If_CluSupport( pF, nVars ); +//Extra_PrintBinary( stdout, &nSupp, 16 ); printf( "\n" ); if ( !nSupp || !If_CluSuppIsMinBase(nSupp) ) return G1; - // perform testing - for ( i = 0; i < nVars; i++ ) - V2P[i] = P2V[i] = i; - G1 = If_CluFindGroup( pF, nVars, 0, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); - - // check permutation - If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V ); - + // detect easy cofs + G1 = If_CluDecUsingCofs( pTruth, nVars, nLutLeaf ); if ( G1.nVars == 0 ) - return G1; + { + // perform testing + G1 = If_CluFindGroup( pF, nVars, 0, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); +// If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V ); + if ( G1.nVars == 0 ) + { + // perform testing with a smaller set + if ( nVars < nLutLeaf + nLutRoot - 2 ) + { + nLutLeaf--; + G1 = If_CluFindGroup( pF, nVars, 0, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); + nLutLeaf++; + } + if ( G1.nVars == 0 ) + { + // perform testing with a different order + If_CluReverseOrder( pF, nVars, V2P, P2V ); + G1 = If_CluFindGroup( pF, nVars, 0, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); + + // check permutation +// If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V ); + if ( G1.nVars == 0 ) + { +/* + if ( nVars == 6 ) + { + Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( " " ); + Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); + if ( !If_CutPerformCheck07( (unsigned *)pF, 6, 6, NULL ) ) + printf( "no\n" ); + } +*/ + return G1; + } + } + } + } - // perform checking - If_CluCheckGroup( pTruth, nVars, &G1 ); + // derive + if ( 0 ) + { + If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, &G1 ); + if ( G1.nMyu == 2 ) + Truth = If_CluDeriveDisjoint( pF, nVars, V2P, P2V, &G1, &R ); + else + Truth = If_CluDeriveNonDisjoint( pF, nVars, V2P, P2V, &G1, &R ); + + // perform checking + if ( 0 ) + { + If_CluCheckGroup( pTruth, nVars, &G1 ); + If_CluVerify( pTruth, nVars, &G1, &R, Truth, pF ); + } + } return G1; } @@ -600,7 +960,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi int nLeaves = If_CutLeaveNum(pCut); int i, nLutLeaf, nLutRoot; // mark the cut as user cut - pCut->fUser = 1; +// pCut->fUser = 1; // quit if parameters are wrong if ( strlen(pStr) != 2 ) { @@ -616,7 +976,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi nLutRoot = pStr[1] - '0'; if ( nLutRoot < 3 || nLutRoot > 6 ) { - printf( "Leaf size (%d) should belong to {3,4,5,6}.\n", nLutRoot ); + printf( "Root size (%d) should belong to {3,4,5,6}.\n", nLutRoot ); return ABC_INFINITY; } if ( nLeaves > nLutLeaf + nLutRoot - 1 ) @@ -627,7 +987,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi // remember the delays If_CutForEachLeaf( p, pCut, pLeaf, i ) - Delays[nLeaves-1-i] = If_ObjCutBest(pLeaf)->Delay; + Delays[i] = If_ObjCutBest(pLeaf)->Delay; // consider easy case if ( nLeaves <= Abc_MaxInt( nLutLeaf, nLutRoot ) ) @@ -639,7 +999,6 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi G1.pVars[i] = i; } G1.nVars = nLeaves; - pCut->Cost = 1; return 1.0 + If_CluDelayMax( &G1, Delays ); } @@ -647,6 +1006,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi G1 = If_CluCheck( (word *)If_CutTruth(pCut), nLeaves, nLutLeaf, nLutRoot ); if ( G1.nVars == 0 ) return ABC_INFINITY; + // compute the delay Delays[nLeaves] = If_CluDelayMax( &G1, Delays ) + (WireDelay == 0.0)?1.0:WireDelay; if ( G2.nVars ) @@ -661,7 +1021,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi assert( G1.nMyu >= 2 && G1.nMyu <= 4 ); if ( G1.nMyu > 2 ) fUsed[G1.pVars[G1.nVars-1]] = 0; - assert( G2.nMyu >= 2 && G2.nMyu <= 4 ); + assert( !G2.nVars || (G2.nMyu >= 2 && G2.nMyu <= 4) ); if ( G2.nMyu > 2 ) fUsed[G2.pVars[G2.nVars-1]] = 0; @@ -681,17 +1041,87 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi return 1.0 + If_CluDelayMax( &G3, Delays ); } + +/**Function************************************************************* + + Synopsis [Performs additional check.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutPerformCheck16( unsigned * pTruth, int nVars, int nLeaves, char * pStr ) +{ + If_Grp_t G1 = {0}, G2 = {0}, G3 = {0}; + int nLutLeaf, nLutRoot; + // quit if parameters are wrong + if ( strlen(pStr) != 2 ) + { + printf( "Wrong LUT struct (%s)\n", pStr ); + return 0; + } + nLutLeaf = pStr[0] - '0'; + if ( nLutLeaf < 3 || nLutLeaf > 6 ) + { + printf( "Leaf size (%d) should belong to {3,4,5,6}.\n", nLutLeaf ); + return 0; + } + nLutRoot = pStr[1] - '0'; + if ( nLutRoot < 3 || nLutRoot > 6 ) + { + printf( "Root size (%d) should belong to {3,4,5,6}.\n", nLutRoot ); + return 0; + } + if ( nLeaves > nLutLeaf + nLutRoot - 1 ) + { + printf( "The cut size (%d) is too large for the LUT structure %d%d.\n", nLeaves, nLutLeaf, nLutRoot ); + return 0; + } + + // consider easy case + if ( nLeaves <= Abc_MaxInt( nLutLeaf, nLutRoot ) ) + return 1; + + // derive the first group + G1 = If_CluCheck( (word *)pTruth, nLeaves, nLutLeaf, nLutRoot ); + if ( G1.nVars == 0 ) + { +// printf( "-%d ", nLeaves ); + return 0; + } +// printf( "+%d ", nLeaves ); + return 1; +} + + // testing procedure void If_CluTest() { // word t = 0xff00f0f0ccccaaaa; - word t = 0xfedcba9876543210; - int nLeaves = 6; +// word t = 0xfedcba9876543210; +// word t = 0xec64000000000000; +// word t = 0x0100200000000001; +// word t2[4] = { 0x0000800080008000, 0x8000000000008000, 0x8000000080008000, 0x0000000080008000 }; +// word t = 0x07770FFF07770FFF; +// word t = 0x002000D000D00020; +// word t = 0x000F000E000F000F; + word t = 0xF7FFF7F7F7F7F7F7; + int nVars = 6; int nLutLeaf = 4; int nLutRoot = 4; If_Grp_t G; - G = If_CluCheck( &t, nLeaves, nLutLeaf, nLutRoot ); + return; + + If_CutPerformCheck07( (unsigned *)&t, 6, 6, NULL ); +// return; + + Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" ); + + G = If_CluCheck( &t, nVars, nLutLeaf, nLutRoot ); If_CluPrintGroup( &G ); } -- cgit v1.2.3