diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 24 | ||||
| -rw-r--r-- | src/map/if/if.h | 2 | ||||
| -rw-r--r-- | src/map/if/ifCut.c | 2 | ||||
| -rw-r--r-- | src/map/if/ifDec10.c | 496 | ||||
| -rw-r--r-- | src/map/if/ifMap.c | 2 | ||||
| -rw-r--r-- | src/map/if/module.make | 1 |
7 files changed, 527 insertions, 4 deletions
@@ -2031,6 +2031,10 @@ SOURCE=.\src\map\if\ifDec.c # End Source File # Begin Source File +SOURCE=.\src\map\if\ifDec10.c +# End Source File +# Begin Source File + SOURCE=.\src\map\if\ifLib.c # End Source File # Begin Source File diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ae849424..035f0d4c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -12878,7 +12878,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) fLutMux = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbugojvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbugojkvh" ) ) != EOF ) { switch ( c ) { @@ -12995,6 +12995,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'j': pPars->fEnableCheck ^= 1; break; + case 'k': + pPars->fEnableCheck2 ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -13074,6 +13077,11 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fCutMin = 1; } + if ( pPars->fEnableCheck && pPars->fEnableCheck2 ) + { + Abc_Print( -1, "These two checks cannot be enabled at the same time.\n" ); + return 1; + } if ( pPars->fEnableCheck ) { if ( pPars->nLutSize < 6 || pPars->nLutSize > 7 ) @@ -13085,6 +13093,17 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fCutMin = 1; } + if ( pPars->fEnableCheck2 ) + { + if ( pPars->nLutSize < 6 || pPars->nLutSize > 10 ) + { + Abc_Print( -1, "This feature only works for {6,7,8,9,10}-LUTs.\n" ); + return 1; + } + pPars->pFuncCell = If_CutPerformCheck10; + pPars->fCutMin = 1; + } + // enable truth table computation if cut minimization is selected if ( pPars->fCutMin ) { @@ -13162,7 +13181,7 @@ usage: sprintf( LutSize, "library" ); else sprintf( LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: if [-KCFA num] [-DE float] [-qarlepmsdbugojvh]\n" ); + Abc_Print( -2, "usage: if [-KCFA num] [-DE float] [-qarlepmsdbugojkvh]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -13185,6 +13204,7 @@ usage: Abc_Print( -2, "\t-g : toggles global delay optimization [default = %s]\n", pPars->fDelayOpt? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" ); Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck? "yes": "no" ); + Abc_Print( -2, "\t-k : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck2? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : prints the command usage\n"); return 1; diff --git a/src/map/if/if.h b/src/map/if/if.h index a8f7cfdc..2584f281 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -97,6 +97,7 @@ struct If_Par_t_ int fUseBat; // use one specialized feature int fUseBuffs; // use buffers to decouple outputs int fEnableCheck; // enable additional checking + int fEnableCheck2; // enable additional checking int fVerbose; // the verbosity flag // internal parameters int fDelayOpt; // special delay optimization @@ -406,6 +407,7 @@ extern float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj extern float If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot ); /*=== ifDec.c =============================================================*/ extern int If_CutPerformCheck( unsigned * pTruth, int nVars, int nLeaves ); +extern int If_CutPerformCheck10( unsigned * pTruth, int nVars, int nLeaves ); /*=== ifLib.c =============================================================*/ extern If_Lib_t * If_LutLibRead( char * FileName ); extern If_Lib_t * If_LutLibDup( If_Lib_t * p ); diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index c37f9c04..b85a59a1 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -685,7 +685,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut ) return; } - if ( (p->pPars->fUseBat || p->pPars->fEnableCheck) && !pCut->fUseless ) + if ( (p->pPars->fUseBat || p->pPars->fEnableCheck || p->pPars->fEnableCheck2) && !pCut->fUseless ) { If_Cut_t * pFirst = pCutSet->ppCuts[0]; if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 ) diff --git a/src/map/if/ifDec10.c b/src/map/if/ifDec10.c new file mode 100644 index 00000000..f1906d81 --- /dev/null +++ b/src/map/if/ifDec10.c @@ -0,0 +1,496 @@ +/**CFile**************************************************************** + + FileName [ifDec10.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Performs additional check.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifDec10.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the bit count for the first 256 integer numbers +static int BitCount8[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; +// variable swapping code +static word PMasks[5][3] = { + { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, + { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, + { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, + { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, + { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } +}; +// elementary truth tables +static word Truth6[6] = { + 0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000 +}; +static word Truth10[10][16] = { + 0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000, + 0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF, + 0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF, + 0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF, + 0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF +}; + +extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); +extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int If_Dec10WordNum( int nVars ) +{ + return nVars <= 6 ? 1 : 1 << (nVars-6); +} +static void If_Dec10PrintConfigOne( unsigned z ) +{ + unsigned t; + t = (z & 0xffff) | ((z & 0xffff) << 16); + Extra_PrintBinary( stdout, &t, 16 ); + printf( " " ); + Kit_DsdPrintFromTruth( &t, 4 ); + printf( " " ); + printf( " %d", (z >> 16) & 7 ); + printf( " %d", (z >> 20) & 7 ); + printf( " %d", (z >> 24) & 7 ); + printf( " %d", (z >> 28) & 7 ); + printf( "\n" ); +} +void If_Dec10PrintConfig( unsigned * pZ ) +{ + while ( *pZ ) + If_Dec10PrintConfigOne( *pZ++ ); +} +static inline void If_Dec10ComposeLut4( int t, word ** pF, word * pR, int nVars ) +{ + word pC[16]; + int m, w, v, nWords; + assert( nVars <= 10 ); + nWords = If_Dec10WordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pR[w] = 0; + for ( m = 0; m < 16; m++ ) + { + if ( !((t >> m) & 1) ) + continue; + for ( w = 0; w < nWords; w++ ) + pC[w] = ~0; + for ( v = 0; v < 4; v++ ) + for ( w = 0; w < nWords; w++ ) + pC[w] &= ((m >> v) & 1) ? pF[v][w] : ~pF[v][w]; + for ( w = 0; w < nWords; w++ ) + pR[w] |= pC[w]; + } +} +void If_Dec10Verify( word * pF, int nVars, unsigned * pZ ) +{ + word pN[16][16], * pG[4]; + int i, w, v, k, nWords; + unsigned z; + nWords = If_Dec10WordNum( nVars ); + for ( k = 0; k < nVars; k++ ) + for ( w = 0; w < nWords; w++ ) + pN[k][w] = Truth10[k][w]; + for ( i = 0; (z = pZ[i]); i++, k++ ) + { + for ( v = 0; v < 4; v++ ) + pG[v] = pN[ (z >> (16+(v<<2))) & 7 ]; + If_Dec10ComposeLut4( (int)(z & 0xffff), pG, pN[k], nVars ); + } + k--; + for ( w = 0; w < nWords; w++ ) + if ( pN[k][w] != pF[w] ) + { + If_Dec10PrintConfig( pZ ); + Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)pN[k], nVars ); printf( "\n" ); + printf( "Verification failed!\n" ); + break; + } +} + + +// count the number of unique cofactors +static inline int If_Dec10CofCount2( word * pF, int nVars ) +{ + int nShift = (1 << (nVars - 4)); + word Mask = (((word)1) << nShift) - 1; + word iCof0 = pF[0] & Mask; + word iCof1 = iCof0, iCof; + int i; + assert( nVars > 6 && nVars <= 10 ); + if ( nVars == 10 ) + Mask = ~0; + for ( i = 1; i < 16; i++ ) + { + iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask; + if ( iCof == iCof0 ) + continue; + if ( iCof1 == iCof0 ) + iCof1 = iCof; + else if ( iCof != iCof1 ) + return 3; + } + return 2; +} +static inline int If_Dec10CofCount( word * pF, int nVars ) +{ + int nShift = (1 << (nVars - 4)); + word Mask = (((word)1) << nShift) - 1; + word iCofs[16], iCof; + int i, k, c, nCofs = 1; + if ( nVars == 10 ) + Mask = ~0; + iCofs[0] = pF[0] & Mask; + for ( i = k = 1; i < 16; i++ ) + { + iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask; + for ( c = 0; c < nCofs; c++ ) + if ( iCof == iCofs[c] ) + break; + if ( c == nCofs ) + iCofs[k++] = iCof; + } + return k; +} + + +// variable permutation for large functions +static inline void If_Dec10Copy( word * pOut, word * pIn, int nVars ) +{ + int w, nWords = If_Dec10WordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn[w]; +} +static inline void If_Dec10SwapAdjacent( word * pOut, word * pIn, int iVar, int nVars ) +{ + int i, k, nWords = If_Dec10WordNum( nVars ); + assert( iVar < nVars - 1 ); + if ( iVar < 5 ) + { + int Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift); + } + else if ( iVar > 5 ) + { + int Step = (1 << (iVar - 6)); + for ( k = 0; k < nWords; k += 4*Step ) + { + for ( i = 0; i < Step; i++ ) + pOut[i] = pIn[i]; + for ( i = 0; i < Step; i++ ) + pOut[Step+i] = pIn[2*Step+i]; + for ( i = 0; i < Step; i++ ) + pOut[2*Step+i] = pIn[Step+i]; + for ( i = 0; i < Step; i++ ) + pOut[3*Step+i] = pIn[3*Step+i]; + pIn += 4*Step; + pOut += 4*Step; + } + } + else // if ( iVar == 5 ) + { + for ( i = 0; i < nWords; i += 2 ) + { + pOut[i] = (pIn[i] & 0x00000000FFFFFFFF) | ((pIn[i+1] & 0x00000000FFFFFFFF) << 32); + pOut[i+1] = (pIn[i+1] & 0xFFFFFFFF00000000) | ((pIn[i] & 0xFFFFFFFF00000000) >> 32); + } + } +} +static inline void If_Dec10MoveTo( word * pF, int nVars, int v, int p, int Pla2Var[], int Var2Pla[] ) +{ + word pG[16], * pIn = pF, * pOut = pG, * pTemp; + int iPlace0, iPlace1, Count = 0; + assert( Var2Pla[v] >= p ); + while ( Var2Pla[v] != p ) + { + iPlace0 = Var2Pla[v]-1; + iPlace1 = Var2Pla[v]; + If_Dec10SwapAdjacent( 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_Dec10Copy( pF, pIn, nVars ); + assert( Pla2Var[p] == v ); +} + +// derive binary function +static inline int If_Dec10DeriveCount2( word * pF, word * pRes, int nVars ) +{ + int nShift = (1 << (nVars - 4)); + word Mask = (((word)1) << nShift) - 1; + int i, MaskDec = 0; + word iCof0 = pF[0] & Mask; + word iCof1 = pF[0] & Mask; + word iCof, * pCof0, * pCof1; + if ( nVars == 10 ) + Mask = ~0; + for ( i = 1; i < 16; i++ ) + { + iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask; + if ( *pCof0 != iCof ) + { + *pCof1 = iCof; + MaskDec |= (1 << i); + } + } + *pRes = ((iCof1 << nShift) | iCof0); + return MaskDec; +} + +static inline word If_DecTruthStretch( word t, int nVars ) +{ + assert( nVars > 1 ); + if ( nVars == 1 ) + nVars++, t = (t & 0x3) | ((t & 0x3) << 2); + if ( nVars == 2 ) + nVars++, t = (t & 0xF) | ((t & 0xF) << 4); + if ( nVars == 3 ) + nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8); + if ( nVars == 4 ) + nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16); + if ( nVars == 5 ) + nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32); + assert( nVars >= 6 ); +} + +// support minimization +static inline int If_DecSuppIsMinBase( int Supp ) +{ + return (Supp & (Supp+1)) == 0; +} +static inline int If_Dec10HasVar( word * t, int nVars, int iVar ) +{ + int nWords = If_Dec10WordNum( nVars ); + assert( iVar < nVars ); + if ( iVar < 6 ) + { + int i, Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) ) + return 1; + return 0; + } + else + { + int i, k, Step = (1 << (iVar - 6)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + if ( t[i] != t[Step+i] ) + return 1; + t += 2*Step; + } + return 0; + } +} +static inline int If_Dec10Support( word * t, int nVars ) +{ + int v, Supp = 0; + for ( v = 0; v < nVars; v++ ) + if ( If_Dec10HasVar( t, nVars, v ) ) + Supp |= (1 << v); + return Supp; +} + +// checks +void If_Dec10Cofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 ) +{ + int nWords = If_Dec10WordNum( nVars ); + assert( iVar < nVars ); + if ( iVar < 6 ) + { + int i, Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + { + pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift); + pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift); + } + return; + } + else + { + int i, k, Step = (1 << (iVar - 6)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + { + pCof0[i] = pCof0[Step+i] = pF[i]; + pCof1[i] = pCof1[Step+i] = pF[Step+i]; + } + pF += 2*Step; + pCof0 += 2*Step; + pCof1 += 2*Step; + } + return; + } +} +static inline int If_Dec10Count16( int Num16 ) +{ + assert( Num16 < (1<<16)-1 ); + return BitCount8[Num16 & 255] + BitCount8[(Num16 >> 8) & 255]; +} +static inline void If_DecVerifyPerm( int Pla2Var[10], int Var2Pla[10], int nVars ) +{ + int i; + for ( i = 0; i < nVars; i++ ) + assert( Pla2Var[Var2Pla[i]] == i ); +} +int If_Dec10Perform( word * pF, int nVars, int fDerive ) +{ + word pCof0[16], pCof1[16]; + int Pla2Var[10], Var2Pla[10], Count[210], Masks[210]; + int i, i0,i1,i2,i3, v, x; + assert( nVars >= 6 && nVars <= 10 ); + // start arrays + for ( i = 0; i < nVars; i++ ) + { + assert( If_Dec10HasVar( pF, nVars, i ) ); + Pla2Var[i] = Var2Pla[i] = i; + } + x = If_Dec10CofCount( pF, nVars ); + // generate permutations + v = 0; + for ( i0 = 0; i0 < nVars; i0++ ) + for ( i1 = i0+1; i1 < nVars; i1++ ) + for ( i2 = i1+1; i2 < nVars; i2++ ) + for ( i3 = i2+1; i3 < nVars; i3++, v++ ) + { + If_Dec10MoveTo( pF, nVars, i0, 0, Pla2Var, Var2Pla ); + If_Dec10MoveTo( pF, nVars, i1, 1, Pla2Var, Var2Pla ); + If_Dec10MoveTo( pF, nVars, i2, 2, Pla2Var, Var2Pla ); + If_Dec10MoveTo( pF, nVars, i3, 3, Pla2Var, Var2Pla ); + If_DecVerifyPerm( Pla2Var, Var2Pla, nVars ); + Count[v] = If_Dec10CofCount( pF, nVars ); + Masks[v] = (1 << i0) | (1 << i1) | (1 << i2) | (1 << i3); +// if ( Count[v] <= 1 ) +// { +// Count[v] = If_Dec10CofCount( pF, nVars ); +// } + assert( Count[v] > 1 ); + if ( Count[v] == 2 || Count[v] > 5 ) + continue; + for ( x = 0; x < 4; x++ ) + { + If_Dec10Cofactors( pF, nVars, x, pCof0, pCof1 ); + if ( If_Dec10CofCount2(pCof0, nVars) <= 2 && If_Dec10CofCount2(pCof1, nVars) <= 2 ) + { + Count[v] = -Count[v]; + break; + } + } + } + assert( v <= 210 ); + // check if there are compatible bound sets + for ( i0 = 0; i0 < v; i0++ ) + for ( i1 = i0+1; i1 < v; i1++ ) + { + if ( If_Dec10Count16(Masks[i0] & Masks[i1]) > 10 - nVars ) + continue; + if ( nVars == 10 ) + { + if ( Count[i0] == 2 && Count[i1] == 2 ) + return 1; + } + else if ( nVars == 9 ) + { + if ( (Count[i0] == 2 && Count[i1] == 2) || + (Count[i0] == 2 && Count[i1] < 0) || + (Count[i0] < 0 && Count[i1] == 2) ) + return 1; + } + else + { + if ( (Count[i0] == 2 && Count[i1] == 2) || + (Count[i0] == 2 && Count[i1] < 0) || + (Count[i0] < 0 && Count[i1] == 2) || + (Count[i0] < 0 && Count[i1] < 0) ) + return 1; + } + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Performs additional check.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutPerformCheck10( unsigned * pTruth, int nVars, int nLeaves ) +{ + int nSupp, fDerive = 0; + word z[2] = {0}, pF[16]; + if ( nLeaves <= 6 ) + return 1; + If_Dec10Copy( pF, (word *)pTruth, nVars ); + nSupp = If_Dec10Support( pF, nLeaves ); + if ( !nSupp || !If_DecSuppIsMinBase(nSupp) ) + return 0; + if ( If_Dec10Perform( pF, nLeaves, fDerive ) ) + { +// printf( "1" ); + return 1; +// If_Dec10Verify( t, nLeaves, NULL ); + } +// printf( "0" ); + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 1a7b6ea7..b7b7c568 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -140,7 +140,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep pCut->fUseless = 0; if ( p->pPars->pFuncCell && RetValue < 2 ) { - assert( pCut->nLimit >= 4 && pCut->nLimit <= 7 ); + assert( pCut->nLimit >= 4 && pCut->nLimit <= 10 ); pCut->fUseless = !p->pPars->pFuncCell( If_CutTruth(pCut), pCut->nLimit, pCut->nLeaves ); p->nCutsUseless += pCut->fUseless; } diff --git a/src/map/if/module.make b/src/map/if/module.make index 76afe9a3..0482c831 100644 --- a/src/map/if/module.make +++ b/src/map/if/module.make @@ -1,6 +1,7 @@ SRC += src/map/if/ifCore.c \ src/map/if/ifCut.c \ src/map/if/ifDec.c \ + src/map/if/ifDec10.c \ src/map/if/ifLib.c \ src/map/if/ifMan.c \ src/map/if/ifMap.c \ |