From 6c2ac7661dc1ea3ddd83617dd247a467e00486de Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 27 Jun 2011 20:17:52 -0700 Subject: Added another specialized check to the mapper. --- abc.rc | 2 +- src/base/abci/abc.c | 37 ++- src/map/if/if.h | 8 +- src/map/if/ifCut.c | 2 +- src/map/if/ifDec.c | 713 ------------------------------------------------- src/map/if/ifDec07.c | 713 +++++++++++++++++++++++++++++++++++++++++++++++++ src/map/if/ifDec08.c | 505 ++++++++++++++++++++++++++++++++++ src/map/if/module.make | 3 +- 8 files changed, 1252 insertions(+), 731 deletions(-) delete mode 100644 src/map/if/ifDec.c create mode 100644 src/map/if/ifDec07.c create mode 100644 src/map/if/ifDec08.c diff --git a/abc.rc b/abc.rc index 194b9945..751f0ce3 100644 --- a/abc.rc +++ b/abc.rc @@ -21,7 +21,7 @@ set gnuplotwin wgnuplot.exe set gnuplotunix gnuplot # Niklas Een's commands -load_plugin C:\_projects\abc\_TEST\bip\bip_2011-04-26.exe "BIP" +load_plugin C:\_projects\abc\_TEST\bip\bip_2011-06-27.exe "BIP" # standard aliases alias b balance diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dca0fcb8..7486e384 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -12884,7 +12884,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) fLutMux = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbugojkvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbugojikvh" ) ) != EOF ) { switch ( c ) { @@ -12999,10 +12999,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fUseBuffs ^= 1; break; case 'j': - pPars->fEnableCheck ^= 1; + pPars->fEnableCheck07 ^= 1; + break; + case 'i': + pPars->fEnableCheck08 ^= 1; break; case 'k': - pPars->fEnableCheck2 ^= 1; + pPars->fEnableCheck10 ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -13083,23 +13086,32 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fCutMin = 1; } - if ( pPars->fEnableCheck && pPars->fEnableCheck2 ) + if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fEnableCheck10 > 1 ) { - Abc_Print( -1, "These two checks cannot be enabled at the same time.\n" ); + Abc_Print( -1, "Only one additional check can be performed at the same time.\n" ); return 1; } - if ( pPars->fEnableCheck ) + if ( pPars->fEnableCheck07 ) { if ( pPars->nLutSize < 6 || pPars->nLutSize > 7 ) { Abc_Print( -1, "This feature only works for {6,7}-LUTs.\n" ); return 1; } - pPars->pFuncCell = If_CutPerformCheck; + pPars->pFuncCell = If_CutPerformCheck07; pPars->fCutMin = 1; } - - if ( pPars->fEnableCheck2 ) + if ( pPars->fEnableCheck08 ) + { + if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 ) + { + Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" ); + return 1; + } + pPars->pFuncCell = If_CutPerformCheck08; + pPars->fCutMin = 1; + } + if ( pPars->fEnableCheck10 ) { if ( pPars->nLutSize < 6 || pPars->nLutSize > 10 ) { @@ -13187,7 +13199,7 @@ usage: sprintf( LutSize, "library" ); else sprintf( LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: if [-KCFA num] [-DE float] [-qarlepmsdbugojkvh]\n" ); + Abc_Print( -2, "usage: if [-KCFA num] [-DE float] [-qarlepmsdbugojikvh]\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 ); @@ -13209,8 +13221,9 @@ usage: Abc_Print( -2, "\t-u : toggles the use of MUXes along with LUTs [default = %s]\n", fLutMux? "yes": "no" ); 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-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); + Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" ); + Abc_Print( -2, "\t-k : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "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 2584f281..61944eaa 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -96,8 +96,9 @@ struct If_Par_t_ int fBidec; // use bi-decomposition int fUseBat; // use one specialized feature int fUseBuffs; // use buffers to decouple outputs - int fEnableCheck; // enable additional checking - int fEnableCheck2; // enable additional checking + int fEnableCheck07;// enable additional checking + int fEnableCheck08;// enable additional checking + int fEnableCheck10;// enable additional checking int fVerbose; // the verbosity flag // internal parameters int fDelayOpt; // special delay optimization @@ -406,7 +407,8 @@ extern float If_CutPowerRef( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * extern float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot ); 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_CutPerformCheck07( unsigned * pTruth, int nVars, int nLeaves ); +extern int If_CutPerformCheck08( 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 ); diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index b85a59a1..f51807ee 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 || p->pPars->fEnableCheck2) && !pCut->fUseless ) + if ( (p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10) && !pCut->fUseless ) { If_Cut_t * pFirst = pCutSet->ppCuts[0]; if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 ) diff --git a/src/map/if/ifDec.c b/src/map/if/ifDec.c deleted file mode 100644 index 38952217..00000000 --- a/src/map/if/ifDec.c +++ /dev/null @@ -1,713 +0,0 @@ -/**CFile**************************************************************** - - FileName [ifDec.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: ifDec.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 Truth7[7][2] = { - 0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA, - 0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC, - 0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0, - 0xFF00FF00FF00FF00,0xFF00FF00FF00FF00, - 0xFFFF0000FFFF0000,0xFFFF0000FFFF0000, - 0xFFFFFFFF00000000,0xFFFFFFFF00000000, - 0x0000000000000000,0xFFFFFFFFFFFFFFFF -}; - -extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); -extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -void If_DecPrintConfig( word z ) -{ - unsigned S[1]; - S[0] = (z & 0xffff) | ((z & 0xffff) << 16); - Extra_PrintBinary( stdout, S, 16 ); - printf( " " ); - Kit_DsdPrintFromTruth( S, 4 ); - printf( " " ); - printf( " %d", (z >> 16) & 7 ); - printf( " %d", (z >> 20) & 7 ); - printf( " %d", (z >> 24) & 7 ); - printf( " %d", (z >> 28) & 7 ); - printf( " " ); - S[0] = ((z >> 32) & 0xffff) | (((z >> 32) & 0xffff) << 16); - Extra_PrintBinary( stdout, S, 16 ); - printf( " " ); - Kit_DsdPrintFromTruth( S, 4 ); - printf( " " ); - printf( " %d", (z >> 48) & 7 ); - printf( " %d", (z >> 52) & 7 ); - printf( " %d", (z >> 56) & 7 ); - printf( " %d", (z >> 60) & 7 ); - printf( "\n" ); -} - -// verification for 6-input function -static word If_Dec6ComposeLut4( int t, word f[4] ) -{ - int m, v; - word c, r = 0; - for ( m = 0; m < 16; m++ ) - { - if ( !((t >> m) & 1) ) - continue; - c = ~0; - for ( v = 0; v < 4; v++ ) - c &= ((m >> v) & 1) ? f[v] : ~f[v]; - r |= c; - } - return r; -} -void If_Dec6Verify( word t, word z ) -{ - word r, q, f[4]; - int i, v; - assert( z ); - for ( i = 0; i < 4; i++ ) - { - v = (z >> (16+(i<<2))) & 7; - assert( v != 7 ); - f[i] = Truth6[v]; - } - q = If_Dec6ComposeLut4( (int)(z & 0xffff), f ); - for ( i = 0; i < 4; i++ ) - { - v = (z >> (48+(i<<2))) & 7; - f[i] = (v == 7) ? q : Truth6[v]; - } - r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f ); - if ( r != t ) - { - If_DecPrintConfig( z ); - Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" ); - Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" ); - Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" ); - printf( "Verification failed!\n" ); - } -} -// verification for 7-input function -static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] ) -{ - int m, v; - word c[2]; - r[0] = r[1] = 0; - for ( m = 0; m < 16; m++ ) - { - if ( !((t >> m) & 1) ) - continue; - c[0] = c[1] = ~0; - for ( v = 0; v < 4; v++ ) - { - c[0] &= ((m >> v) & 1) ? f[v][0] : ~f[v][0]; - c[1] &= ((m >> v) & 1) ? f[v][1] : ~f[v][1]; - } - r[0] |= c[0]; - r[1] |= c[1]; - } -} -void If_Dec7Verify( word t[2], word z ) -{ - word f[4][2], r[2]; - int i, v; - assert( z ); - for ( i = 0; i < 4; i++ ) - { - v = (z >> (16+(i<<2))) & 7; - f[i][0] = Truth7[v][0]; - f[i][1] = Truth7[v][1]; - } - If_Dec7ComposeLut4( (int)(z & 0xffff), f, r ); - f[3][0] = r[0]; - f[3][1] = r[1]; - for ( i = 0; i < 3; i++ ) - { - v = (z >> (48+(i<<2))) & 7; - f[i][0] = Truth7[v][0]; - f[i][1] = Truth7[v][1]; - } - If_Dec7ComposeLut4( (int)((z >> 32) & 0xffff), f, r ); - if ( r[0] != t[0] || r[1] != t[1] ) - { - If_DecPrintConfig( z ); - Kit_DsdPrintFromTruth( (unsigned*)t, 7 ); printf( "\n" ); - Kit_DsdPrintFromTruth( (unsigned*)r, 7 ); printf( "\n" ); - printf( "Verification failed!\n" ); - } -} - - -// count the number of unique cofactors -static inline int If_Dec6CofCount2( word t ) -{ - int i, Mask = 0; - for ( i = 0; i < 16; i++ ) - Mask |= (1 << ((t >> (i<<2)) & 15)); - return BitCount8[((unsigned char*)&Mask)[0]] + BitCount8[((unsigned char*)&Mask)[1]]; -} -// count the number of unique cofactors (up to 3) -static inline int If_Dec7CofCount3( word t[2] ) -{ - unsigned char * pTruth = (unsigned char *)t; - int i, iCof2 = 0; - for ( i = 1; i < 16; i++ ) - { - if ( pTruth[i] == pTruth[0] ) - continue; - if ( iCof2 == 0 ) - iCof2 = i; - else if ( pTruth[i] != pTruth[iCof2] ) - return 3; - } - assert( iCof2 ); - return 2; -} - -// permute 6-input function -static inline word If_Dec6SwapAdjacent( word t, int v ) -{ - assert( v < 5 ); - return (t & PMasks[v][0]) | ((t & PMasks[v][1]) << (1 << v)) | ((t & PMasks[v][2]) >> (1 << v)); -} -static inline word If_Dec6MoveTo( word t, int v, int p, int Pla2Var[6], int Var2Pla[6] ) -{ - int iPlace0, iPlace1; - assert( Var2Pla[v] >= p ); - while ( Var2Pla[v] != p ) - { - iPlace0 = Var2Pla[v]-1; - iPlace1 = Var2Pla[v]; - t = If_Dec6SwapAdjacent( t, iPlace0 ); - Var2Pla[Pla2Var[iPlace0]]++; - Var2Pla[Pla2Var[iPlace1]]--; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - } - assert( Pla2Var[p] == v ); - return t; -} - -// permute 7-input function -static inline void If_Dec7SwapAdjacent( word t[2], int v ) -{ - if ( v == 5 ) - { - unsigned Temp = (t[0] >> 32); - t[0] = (t[0] & 0xFFFFFFFF) | ((t[1] & 0xFFFFFFFF) << 32); - t[1] ^= (t[1] & 0xFFFFFFFF) ^ Temp; - return; - } - assert( v < 5 ); - t[0] = If_Dec6SwapAdjacent( t[0], v ); - t[1] = If_Dec6SwapAdjacent( t[1], v ); -} -static inline void If_Dec7MoveTo( word t[2], int v, int p, int Pla2Var[7], int Var2Pla[7] ) -{ - int iPlace0, iPlace1; - assert( Var2Pla[v] >= p ); - while ( Var2Pla[v] != p ) - { - iPlace0 = Var2Pla[v]-1; - iPlace1 = Var2Pla[v]; - If_Dec7SwapAdjacent( t, iPlace0 ); - Var2Pla[Pla2Var[iPlace0]]++; - Var2Pla[Pla2Var[iPlace1]]--; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - } - assert( Pla2Var[p] == v ); -} - -// derive binary function -static inline int If_Dec6DeriveCount2( word t, int * pCof0, int * pCof1 ) -{ - int i, Mask = 0; - *pCof0 = (t & 15); - *pCof1 = (t & 15); - for ( i = 1; i < 16; i++ ) - if ( *pCof0 != ((t >> (i<<2)) & 15) ) - { - *pCof1 = ((t >> (i<<2)) & 15); - Mask |= (1 << i); - } - return Mask; -} -static inline int If_Dec7DeriveCount3( word t[2], int * pCof0, int * pCof1 ) -{ - unsigned char * pTruth = (unsigned char *)t; - int i, Mask = 0; - *pCof0 = pTruth[0]; - *pCof1 = pTruth[0]; - for ( i = 1; i < 16; i++ ) - if ( *pCof0 != pTruth[i] ) - { - *pCof1 = pTruth[i]; - Mask |= (1 << i); - } - return Mask; -} - -// derives decomposition -static inline word If_Dec6Cofactor( word t, int iVar, int fCof1 ) -{ - assert( iVar >= 0 && iVar < 6 ); - if ( fCof1 ) - return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<= 2 && s <= 5 ); - for ( i = 0; i < 6; i++ ) - { - Pla2Var[i] = Pla2Var0[i]; - Var2Pla[i] = Var2Pla0[i]; - } - for ( i = s; i < 5; i++ ) - { - t = If_Dec6SwapAdjacent( t, i ); - Var2Pla[Pla2Var[i]]++; - Var2Pla[Pla2Var[i+1]]--; - Pla2Var[i] ^= Pla2Var[i+1]; - Pla2Var[i+1] ^= Pla2Var[i]; - Pla2Var[i] ^= Pla2Var[i+1]; - } - c0 = If_Dec6Cofactor( t, 5, 0 ); - c1 = If_Dec6Cofactor( t, 5, 1 ); - assert( 2 >= If_Dec6CofCount2(c0) ); - assert( 2 >= If_Dec6CofCount2(c1) ); - Truth0 = If_Dec6DeriveCount2( c0, &Cof0[0], &Cof0[1] ); - Truth1 = If_Dec6DeriveCount2( c1, &Cof1[0], &Cof1[1] ); - z = ((Truth1 & 0xFF) << 8) | (Truth0 & 0xFF); - 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; -} -static word If_Dec7DeriveDisjoint( word t[2], int Pla2Var[7], int Var2Pla[7] ) -{ - int i, Cof0, Cof1; - word z = If_Dec7DeriveCount3( t, &Cof0, &Cof1 ); - for ( i = 0; i < 4; i++ ) - z |= (((word)Pla2Var[i+3]) << (16 + 4*i)); - z |= ((word)((Cof1 << 8) | Cof0) << 32); - for ( i = 0; i < 3; i++ ) - z |= (((word)Pla2Var[i]) << (48 + 4*i)); - z |= (((word)7) << (48 + 4*i)); - return z; -} - -static inline int If_Dec6CountOnes( word t ) -{ - t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555); - t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333); - t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F); - t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF); - t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF); - return (t & 0x00000000FFFFFFFF) + (t>>32); -} -static inline int If_Dec6HasVar( word t, int v ) -{ - return ((t & Truth6[v]) >> (1<= 0 && v < 7 ); - if ( v == 6 ) - return t[0] != t[1]; - return ((t[0] & Truth6[v]) >> (1<> (1< 1 ); - if ( Count == 2 ) - return !fDerive ? 1 : If_Dec6DeriveDisjoint( t, Pla2Var, Var2Pla ); - // check non-disjoint decomposition - if ( !r && (Count == 3 || Count == 4) ) - { - for ( x = 0; x < 4; x++ ) - { - word c0 = If_Dec6Cofactor( t, x+2, 0 ); - word c1 = If_Dec6Cofactor( t, x+2, 1 ); - if ( If_Dec6CofCount2( c0 ) <= 2 && If_Dec6CofCount2( c1 ) <= 2 ) - { - r = !fDerive ? 1 : If_Dec6DeriveNonDisjoint( t, x+2, Pla2Var, Var2Pla ); - break; - } - } - } - } - assert( i == 15 ); - return r; -} -word If_Dec7Perform( word t0[2], int fDerive ) -{ - word t[2] = {t0[0], t0[1]}; - int i, v, u, y, Pla2Var[7], Var2Pla[7]; - // start arrays - for ( i = 0; i < 7; i++ ) - { - if ( i < 6 ) - assert( If_Dec6HasVar( t[0], i ) || If_Dec6HasVar( t[1], i ) ); - else - assert( t[0] != t[1] ); - Pla2Var[i] = Var2Pla[i] = i; - } - // generate permutations - for ( v = 0; v < 7; v++ ) - for ( u = v+1; u < 7; u++ ) - for ( y = u+1; y < 7; y++ ) - { - If_Dec7MoveTo( t, v, 0, Pla2Var, Var2Pla ); - If_Dec7MoveTo( t, u, 1, Pla2Var, Var2Pla ); - If_Dec7MoveTo( t, y, 2, Pla2Var, Var2Pla ); -// If_DecVerifyPerm( Pla2Var, Var2Pla ); - if ( If_Dec7CofCount3( t ) == 2 ) - { - return !fDerive ? 1 : If_Dec7DeriveDisjoint( t, Pla2Var, Var2Pla ); - } - } - return 0; -} - - -// support minimization -static inline int If_DecSuppIsMinBase( int Supp ) -{ - return (Supp & (Supp+1)) == 0; -} -static inline word If_Dec6TruthShrink( word uTruth, int nVars, int nVarsAll, unsigned Phase ) -{ - int i, k, Var = 0; - assert( nVarsAll <= 6 ); - for ( i = 0; i < nVarsAll; i++ ) - if ( Phase & (1 << i) ) - { - for ( k = i-1; k >= Var; k-- ) - uTruth = If_Dec6SwapAdjacent( uTruth, k ); - Var++; - } - assert( Var == nVars ); - return uTruth; -} -word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars ) -{ - int v, iVar = 0, uSupp = 0; - assert( nVarsAll <= 6 ); - for ( v = 0; v < nVarsAll; v++ ) - if ( If_Dec6HasVar( uTruth, v ) ) - { - uSupp |= (1 << v); - if ( pSupp ) - pSupp[iVar] = pSupp[v]; - iVar++; - } - if ( pnVars ) - *pnVars = iVar; - if ( If_DecSuppIsMinBase( uSupp ) ) - return uTruth; - return If_Dec6TruthShrink( uTruth, iVar, nVarsAll, uSupp ); -} - -static inline void If_Dec7TruthShrink( word uTruth[2], int nVars, int nVarsAll, unsigned Phase ) -{ - int i, k, Var = 0; - assert( nVarsAll <= 7 ); - for ( i = 0; i < nVarsAll; i++ ) - if ( Phase & (1 << i) ) - { - for ( k = i-1; k >= Var; k-- ) - If_Dec7SwapAdjacent( uTruth, k ); - Var++; - } - assert( Var == nVars ); -} -void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars ) -{ - int v, iVar = 0, uSupp = 0; - assert( nVarsAll <= 7 ); - for ( v = 0; v < nVarsAll; v++ ) - if ( If_Dec7HasVar( uTruth, v ) ) - { - uSupp |= (1 << v); - if ( pSupp ) - pSupp[iVar] = pSupp[v]; - iVar++; - } - if ( pnVars ) - *pnVars = iVar; - if ( If_DecSuppIsMinBase( uSupp ) ) - return; - If_Dec7TruthShrink( uTruth, iVar, nVarsAll, uSupp ); -} - - - -// check for MUX decomposition -static inline int If_Dec6SuppSize( word t ) -{ - int v, Count = 0; - for ( v = 0; v < 6; v++ ) - if ( If_Dec6Cofactor(t, v, 0) != If_Dec6Cofactor(t, v, 1) ) - Count++; - return Count; -} -static inline int If_Dec6CheckMux( word t ) -{ - int v; - for ( v = 0; v < 6; v++ ) - if ( If_Dec6SuppSize(If_Dec6Cofactor(t, v, 0)) < 5 && - If_Dec6SuppSize(If_Dec6Cofactor(t, v, 1)) < 5 ) - return v; - return -1; -} - -// check for MUX decomposition -static inline void If_Dec7Cofactor( word t[2], int iVar, int fCof1, word r[2] ) -{ - assert( iVar >= 0 && iVar < 7 ); - if ( iVar == 6 ) - { - if ( fCof1 ) - r[0] = r[1] = t[1]; - else - r[0] = r[1] = t[0]; - } - else - { - if ( fCof1 ) - { - r[0] = (t[0] & Truth6[iVar]) | ((t[0] & Truth6[iVar]) >> (1<> (1< Count0 + Count1 ) - { - CountBest = Count0 + Count1; - vBest = v; - Cofs[0] = If_Dec6Cofactor(t, v, 0); - Cofs[1] = If_Dec6Cofactor(t, v, 1); - } - } - return vBest; -} -int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] ) -{ - word c0[2], c1[2]; - int v, vBest = -1, Count0, Count1, CountBest = 1000; - for ( v = 0; v < 7; v++ ) - { - If_Dec7Cofactor( t, v, 0, c0 ); - If_Dec7Cofactor( t, v, 1, c1 ); - Count0 = If_Dec7SuppSize(c0); - Count1 = If_Dec7SuppSize(c1); - if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 ) - { - CountBest = Count0 + Count1; - vBest = v; - c0r[0] = c0[0]; c0r[1] = c0[1]; - c1r[0] = c1[0]; c1r[1] = c1[1]; - } - } - return vBest; -} - - -/**Function************************************************************* - - Synopsis [Performs additional check.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int If_CutPerformCheck( unsigned * pTruth, int nVars, int nLeaves ) -{ - int fDerive = 1; - if ( nLeaves < 6 ) - return 1; - if ( nLeaves == 6 ) - { - word z, t = ((word *)pTruth)[0]; - if ( If_Dec6CheckMux(t) >= 0 ) - return 1; - z = If_Dec6Perform( t, fDerive ); - if ( fDerive && z ) - If_Dec6Verify( t, z ); - return z != 0; - } - if ( nLeaves == 7 ) - { - word z, t[2]; - t[0] = ((word *)pTruth)[0]; - t[1] = ((word *)pTruth)[1]; - if ( If_Dec7CheckMux(t) >= 0 ) - return 1; - z = If_Dec7Perform( t, fDerive ); - if ( fDerive && z ) - If_Dec7Verify( t, z ); - - - return z != 0; - } - assert( 0 ); - return 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c new file mode 100644 index 00000000..8ba6a670 --- /dev/null +++ b/src/map/if/ifDec07.c @@ -0,0 +1,713 @@ +/**CFile**************************************************************** + + FileName [ifDec07.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: ifDec07.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 Truth7[7][2] = { + 0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00,0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000,0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000,0xFFFFFFFF00000000, + 0x0000000000000000,0xFFFFFFFFFFFFFFFF +}; + +extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); +extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +void If_DecPrintConfig( word z ) +{ + unsigned S[1]; + S[0] = (z & 0xffff) | ((z & 0xffff) << 16); + Extra_PrintBinary( stdout, S, 16 ); + printf( " " ); + Kit_DsdPrintFromTruth( S, 4 ); + printf( " " ); + printf( " %d", (z >> 16) & 7 ); + printf( " %d", (z >> 20) & 7 ); + printf( " %d", (z >> 24) & 7 ); + printf( " %d", (z >> 28) & 7 ); + printf( " " ); + S[0] = ((z >> 32) & 0xffff) | (((z >> 32) & 0xffff) << 16); + Extra_PrintBinary( stdout, S, 16 ); + printf( " " ); + Kit_DsdPrintFromTruth( S, 4 ); + printf( " " ); + printf( " %d", (z >> 48) & 7 ); + printf( " %d", (z >> 52) & 7 ); + printf( " %d", (z >> 56) & 7 ); + printf( " %d", (z >> 60) & 7 ); + printf( "\n" ); +} + +// verification for 6-input function +static word If_Dec6ComposeLut4( int t, word f[4] ) +{ + int m, v; + word c, r = 0; + for ( m = 0; m < 16; m++ ) + { + if ( !((t >> m) & 1) ) + continue; + c = ~0; + for ( v = 0; v < 4; v++ ) + c &= ((m >> v) & 1) ? f[v] : ~f[v]; + r |= c; + } + return r; +} +void If_Dec6Verify( word t, word z ) +{ + word r, q, f[4]; + int i, v; + assert( z ); + for ( i = 0; i < 4; i++ ) + { + v = (z >> (16+(i<<2))) & 7; + assert( v != 7 ); + f[i] = Truth6[v]; + } + q = If_Dec6ComposeLut4( (int)(z & 0xffff), f ); + for ( i = 0; i < 4; i++ ) + { + v = (z >> (48+(i<<2))) & 7; + f[i] = (v == 7) ? q : Truth6[v]; + } + r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f ); + if ( r != t ) + { + If_DecPrintConfig( z ); + Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" ); + printf( "Verification failed!\n" ); + } +} +// verification for 7-input function +static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] ) +{ + int m, v; + word c[2]; + r[0] = r[1] = 0; + for ( m = 0; m < 16; m++ ) + { + if ( !((t >> m) & 1) ) + continue; + c[0] = c[1] = ~0; + for ( v = 0; v < 4; v++ ) + { + c[0] &= ((m >> v) & 1) ? f[v][0] : ~f[v][0]; + c[1] &= ((m >> v) & 1) ? f[v][1] : ~f[v][1]; + } + r[0] |= c[0]; + r[1] |= c[1]; + } +} +void If_Dec7Verify( word t[2], word z ) +{ + word f[4][2], r[2]; + int i, v; + assert( z ); + for ( i = 0; i < 4; i++ ) + { + v = (z >> (16+(i<<2))) & 7; + f[i][0] = Truth7[v][0]; + f[i][1] = Truth7[v][1]; + } + If_Dec7ComposeLut4( (int)(z & 0xffff), f, r ); + f[3][0] = r[0]; + f[3][1] = r[1]; + for ( i = 0; i < 3; i++ ) + { + v = (z >> (48+(i<<2))) & 7; + f[i][0] = Truth7[v][0]; + f[i][1] = Truth7[v][1]; + } + If_Dec7ComposeLut4( (int)((z >> 32) & 0xffff), f, r ); + if ( r[0] != t[0] || r[1] != t[1] ) + { + If_DecPrintConfig( z ); + Kit_DsdPrintFromTruth( (unsigned*)t, 7 ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)r, 7 ); printf( "\n" ); + printf( "Verification failed!\n" ); + } +} + + +// count the number of unique cofactors +static inline int If_Dec6CofCount2( word t ) +{ + int i, Mask = 0; + for ( i = 0; i < 16; i++ ) + Mask |= (1 << ((t >> (i<<2)) & 15)); + return BitCount8[((unsigned char*)&Mask)[0]] + BitCount8[((unsigned char*)&Mask)[1]]; +} +// count the number of unique cofactors (up to 3) +static inline int If_Dec7CofCount3( word t[2] ) +{ + unsigned char * pTruth = (unsigned char *)t; + int i, iCof2 = 0; + for ( i = 1; i < 16; i++ ) + { + if ( pTruth[i] == pTruth[0] ) + continue; + if ( iCof2 == 0 ) + iCof2 = i; + else if ( pTruth[i] != pTruth[iCof2] ) + return 3; + } + assert( iCof2 ); + return 2; +} + +// permute 6-input function +static inline word If_Dec6SwapAdjacent( word t, int v ) +{ + assert( v < 5 ); + return (t & PMasks[v][0]) | ((t & PMasks[v][1]) << (1 << v)) | ((t & PMasks[v][2]) >> (1 << v)); +} +static inline word If_Dec6MoveTo( word t, int v, int p, int Pla2Var[6], int Var2Pla[6] ) +{ + int iPlace0, iPlace1; + assert( Var2Pla[v] >= p ); + while ( Var2Pla[v] != p ) + { + iPlace0 = Var2Pla[v]-1; + iPlace1 = Var2Pla[v]; + t = If_Dec6SwapAdjacent( t, iPlace0 ); + Var2Pla[Pla2Var[iPlace0]]++; + Var2Pla[Pla2Var[iPlace1]]--; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + } + assert( Pla2Var[p] == v ); + return t; +} + +// permute 7-input function +static inline void If_Dec7SwapAdjacent( word t[2], int v ) +{ + if ( v == 5 ) + { + unsigned Temp = (t[0] >> 32); + t[0] = (t[0] & 0xFFFFFFFF) | ((t[1] & 0xFFFFFFFF) << 32); + t[1] ^= (t[1] & 0xFFFFFFFF) ^ Temp; + return; + } + assert( v < 5 ); + t[0] = If_Dec6SwapAdjacent( t[0], v ); + t[1] = If_Dec6SwapAdjacent( t[1], v ); +} +static inline void If_Dec7MoveTo( word t[2], int v, int p, int Pla2Var[7], int Var2Pla[7] ) +{ + int iPlace0, iPlace1; + assert( Var2Pla[v] >= p ); + while ( Var2Pla[v] != p ) + { + iPlace0 = Var2Pla[v]-1; + iPlace1 = Var2Pla[v]; + If_Dec7SwapAdjacent( t, iPlace0 ); + Var2Pla[Pla2Var[iPlace0]]++; + Var2Pla[Pla2Var[iPlace1]]--; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; + Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + } + assert( Pla2Var[p] == v ); +} + +// derive binary function +static inline int If_Dec6DeriveCount2( word t, int * pCof0, int * pCof1 ) +{ + int i, Mask = 0; + *pCof0 = (t & 15); + *pCof1 = (t & 15); + for ( i = 1; i < 16; i++ ) + if ( *pCof0 != ((t >> (i<<2)) & 15) ) + { + *pCof1 = ((t >> (i<<2)) & 15); + Mask |= (1 << i); + } + return Mask; +} +static inline int If_Dec7DeriveCount3( word t[2], int * pCof0, int * pCof1 ) +{ + unsigned char * pTruth = (unsigned char *)t; + int i, Mask = 0; + *pCof0 = pTruth[0]; + *pCof1 = pTruth[0]; + for ( i = 1; i < 16; i++ ) + if ( *pCof0 != pTruth[i] ) + { + *pCof1 = pTruth[i]; + Mask |= (1 << i); + } + return Mask; +} + +// derives decomposition +static inline word If_Dec6Cofactor( word t, int iVar, int fCof1 ) +{ + assert( iVar >= 0 && iVar < 6 ); + if ( fCof1 ) + return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<= 2 && s <= 5 ); + for ( i = 0; i < 6; i++ ) + { + Pla2Var[i] = Pla2Var0[i]; + Var2Pla[i] = Var2Pla0[i]; + } + for ( i = s; i < 5; i++ ) + { + t = If_Dec6SwapAdjacent( t, i ); + Var2Pla[Pla2Var[i]]++; + Var2Pla[Pla2Var[i+1]]--; + Pla2Var[i] ^= Pla2Var[i+1]; + Pla2Var[i+1] ^= Pla2Var[i]; + Pla2Var[i] ^= Pla2Var[i+1]; + } + c0 = If_Dec6Cofactor( t, 5, 0 ); + c1 = If_Dec6Cofactor( t, 5, 1 ); + assert( 2 >= If_Dec6CofCount2(c0) ); + assert( 2 >= If_Dec6CofCount2(c1) ); + Truth0 = If_Dec6DeriveCount2( c0, &Cof0[0], &Cof0[1] ); + Truth1 = If_Dec6DeriveCount2( c1, &Cof1[0], &Cof1[1] ); + z = ((Truth1 & 0xFF) << 8) | (Truth0 & 0xFF); + 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; +} +static word If_Dec7DeriveDisjoint( word t[2], int Pla2Var[7], int Var2Pla[7] ) +{ + int i, Cof0, Cof1; + word z = If_Dec7DeriveCount3( t, &Cof0, &Cof1 ); + for ( i = 0; i < 4; i++ ) + z |= (((word)Pla2Var[i+3]) << (16 + 4*i)); + z |= ((word)((Cof1 << 8) | Cof0) << 32); + for ( i = 0; i < 3; i++ ) + z |= (((word)Pla2Var[i]) << (48 + 4*i)); + z |= (((word)7) << (48 + 4*i)); + return z; +} + +static inline int If_Dec6CountOnes( word t ) +{ + t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555); + t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333); + t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F); + t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF); + t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF); + return (t & 0x00000000FFFFFFFF) + (t>>32); +} +static inline int If_Dec6HasVar( word t, int v ) +{ + return ((t & Truth6[v]) >> (1<= 0 && v < 7 ); + if ( v == 6 ) + return t[0] != t[1]; + return ((t[0] & Truth6[v]) >> (1<> (1< 1 ); + if ( Count == 2 ) + return !fDerive ? 1 : If_Dec6DeriveDisjoint( t, Pla2Var, Var2Pla ); + // check non-disjoint decomposition + if ( !r && (Count == 3 || Count == 4) ) + { + for ( x = 0; x < 4; x++ ) + { + word c0 = If_Dec6Cofactor( t, x+2, 0 ); + word c1 = If_Dec6Cofactor( t, x+2, 1 ); + if ( If_Dec6CofCount2( c0 ) <= 2 && If_Dec6CofCount2( c1 ) <= 2 ) + { + r = !fDerive ? 1 : If_Dec6DeriveNonDisjoint( t, x+2, Pla2Var, Var2Pla ); + break; + } + } + } + } + assert( i == 15 ); + return r; +} +word If_Dec7Perform( word t0[2], int fDerive ) +{ + word t[2] = {t0[0], t0[1]}; + int i, v, u, y, Pla2Var[7], Var2Pla[7]; + // start arrays + for ( i = 0; i < 7; i++ ) + { + if ( i < 6 ) + assert( If_Dec6HasVar( t[0], i ) || If_Dec6HasVar( t[1], i ) ); + else + assert( t[0] != t[1] ); + Pla2Var[i] = Var2Pla[i] = i; + } + // generate permutations + for ( v = 0; v < 7; v++ ) + for ( u = v+1; u < 7; u++ ) + for ( y = u+1; y < 7; y++ ) + { + If_Dec7MoveTo( t, v, 0, Pla2Var, Var2Pla ); + If_Dec7MoveTo( t, u, 1, Pla2Var, Var2Pla ); + If_Dec7MoveTo( t, y, 2, Pla2Var, Var2Pla ); +// If_DecVerifyPerm( Pla2Var, Var2Pla ); + if ( If_Dec7CofCount3( t ) == 2 ) + { + return !fDerive ? 1 : If_Dec7DeriveDisjoint( t, Pla2Var, Var2Pla ); + } + } + return 0; +} + + +// support minimization +static inline int If_DecSuppIsMinBase( int Supp ) +{ + return (Supp & (Supp+1)) == 0; +} +static inline word If_Dec6TruthShrink( word uTruth, int nVars, int nVarsAll, unsigned Phase ) +{ + int i, k, Var = 0; + assert( nVarsAll <= 6 ); + for ( i = 0; i < nVarsAll; i++ ) + if ( Phase & (1 << i) ) + { + for ( k = i-1; k >= Var; k-- ) + uTruth = If_Dec6SwapAdjacent( uTruth, k ); + Var++; + } + assert( Var == nVars ); + return uTruth; +} +word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars ) +{ + int v, iVar = 0, uSupp = 0; + assert( nVarsAll <= 6 ); + for ( v = 0; v < nVarsAll; v++ ) + if ( If_Dec6HasVar( uTruth, v ) ) + { + uSupp |= (1 << v); + if ( pSupp ) + pSupp[iVar] = pSupp[v]; + iVar++; + } + if ( pnVars ) + *pnVars = iVar; + if ( If_DecSuppIsMinBase( uSupp ) ) + return uTruth; + return If_Dec6TruthShrink( uTruth, iVar, nVarsAll, uSupp ); +} + +static inline void If_Dec7TruthShrink( word uTruth[2], int nVars, int nVarsAll, unsigned Phase ) +{ + int i, k, Var = 0; + assert( nVarsAll <= 7 ); + for ( i = 0; i < nVarsAll; i++ ) + if ( Phase & (1 << i) ) + { + for ( k = i-1; k >= Var; k-- ) + If_Dec7SwapAdjacent( uTruth, k ); + Var++; + } + assert( Var == nVars ); +} +void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars ) +{ + int v, iVar = 0, uSupp = 0; + assert( nVarsAll <= 7 ); + for ( v = 0; v < nVarsAll; v++ ) + if ( If_Dec7HasVar( uTruth, v ) ) + { + uSupp |= (1 << v); + if ( pSupp ) + pSupp[iVar] = pSupp[v]; + iVar++; + } + if ( pnVars ) + *pnVars = iVar; + if ( If_DecSuppIsMinBase( uSupp ) ) + return; + If_Dec7TruthShrink( uTruth, iVar, nVarsAll, uSupp ); +} + + + +// check for MUX decomposition +static inline int If_Dec6SuppSize( word t ) +{ + int v, Count = 0; + for ( v = 0; v < 6; v++ ) + if ( If_Dec6Cofactor(t, v, 0) != If_Dec6Cofactor(t, v, 1) ) + Count++; + return Count; +} +static inline int If_Dec6CheckMux( word t ) +{ + int v; + for ( v = 0; v < 6; v++ ) + if ( If_Dec6SuppSize(If_Dec6Cofactor(t, v, 0)) < 5 && + If_Dec6SuppSize(If_Dec6Cofactor(t, v, 1)) < 5 ) + return v; + return -1; +} + +// check for MUX decomposition +static inline void If_Dec7Cofactor( word t[2], int iVar, int fCof1, word r[2] ) +{ + assert( iVar >= 0 && iVar < 7 ); + if ( iVar == 6 ) + { + if ( fCof1 ) + r[0] = r[1] = t[1]; + else + r[0] = r[1] = t[0]; + } + else + { + if ( fCof1 ) + { + r[0] = (t[0] & Truth6[iVar]) | ((t[0] & Truth6[iVar]) >> (1<> (1< Count0 + Count1 ) + { + CountBest = Count0 + Count1; + vBest = v; + Cofs[0] = If_Dec6Cofactor(t, v, 0); + Cofs[1] = If_Dec6Cofactor(t, v, 1); + } + } + return vBest; +} +int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] ) +{ + word c0[2], c1[2]; + int v, vBest = -1, Count0, Count1, CountBest = 1000; + for ( v = 0; v < 7; v++ ) + { + If_Dec7Cofactor( t, v, 0, c0 ); + If_Dec7Cofactor( t, v, 1, c1 ); + Count0 = If_Dec7SuppSize(c0); + Count1 = If_Dec7SuppSize(c1); + if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 ) + { + CountBest = Count0 + Count1; + vBest = v; + c0r[0] = c0[0]; c0r[1] = c0[1]; + c1r[0] = c1[0]; c1r[1] = c1[1]; + } + } + return vBest; +} + + +/**Function************************************************************* + + Synopsis [Performs additional check.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutPerformCheck07( unsigned * pTruth, int nVars, int nLeaves ) +{ + int fDerive = 1; + if ( nLeaves < 6 ) + return 1; + if ( nLeaves == 6 ) + { + word z, t = ((word *)pTruth)[0]; + if ( If_Dec6CheckMux(t) >= 0 ) + return 1; + z = If_Dec6Perform( t, fDerive ); + if ( fDerive && z ) + If_Dec6Verify( t, z ); + return z != 0; + } + if ( nLeaves == 7 ) + { + word z, t[2]; + t[0] = ((word *)pTruth)[0]; + t[1] = ((word *)pTruth)[1]; + if ( If_Dec7CheckMux(t) >= 0 ) + return 1; + z = If_Dec7Perform( t, fDerive ); + if ( fDerive && z ) + If_Dec7Verify( t, z ); + + + return z != 0; + } + assert( 0 ); + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/map/if/ifDec08.c b/src/map/if/ifDec08.c new file mode 100644 index 00000000..ec23f288 --- /dev/null +++ b/src/map/if/ifDec08.c @@ -0,0 +1,505 @@ +/**CFile**************************************************************** + + FileName [ifDec08.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: ifDec08.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_Dec08WordNum( int nVars ) +{ + return nVars <= 6 ? 1 : 1 << (nVars-6); +} +static void If_Dec08PrintConfigOne( 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_Dec08PrintConfig( unsigned * pZ ) +{ + while ( *pZ ) + If_Dec08PrintConfigOne( *pZ++ ); +} +static inline void If_Dec08ComposeLut4( int t, word ** pF, word * pR, int nVars ) +{ + word pC[16]; + int m, w, v, nWords; + assert( nVars <= 10 ); + nWords = If_Dec08WordNum( 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_Dec08Verify( word * pF, int nVars, unsigned * pZ ) +{ + word pN[16][16], * pG[4]; + int i, w, v, k, nWords; + unsigned z; + nWords = If_Dec08WordNum( 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_Dec08ComposeLut4( (int)(z & 0xffff), pG, pN[k], nVars ); + } + k--; + for ( w = 0; w < nWords; w++ ) + if ( pN[k][w] != pF[w] ) + { + If_Dec08PrintConfig( 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_Dec08CofCount2( word * pF, int nVars ) +{ + int nShift = (1 << (nVars - 3)); + word Mask = (((word)1) << nShift) - 1; + word iCof0 = pF[0] & Mask; + word iCof1 = iCof0, iCof; + int i; + assert( nVars >= 6 && nVars <= 8 ); +// if ( nVars == 10 ) +// Mask = ~0; + for ( i = 1; i < 8; 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_Dec08CofCount( word * pF, int nVars ) +{ + int nShift = (1 << (nVars - 3)); + word Mask = (((word)1) << nShift) - 1; + word iCofs[16], iCof; + int i, c, nCofs = 1; +// if ( nVars == 10 ) +// Mask = ~0; + iCofs[0] = pF[0] & Mask; + for ( i = 1; i < 8; 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[nCofs++] = iCof; + } + return nCofs; +} + + +// variable permutation for large functions +static inline void If_Dec08Copy( word * pOut, word * pIn, int nVars ) +{ + int w, nWords = If_Dec08WordNum( nVars ); + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn[w]; +} +static inline void If_Dec08SwapAdjacent( word * pOut, word * pIn, int iVar, int nVars ) +{ + int i, k, nWords = If_Dec08WordNum( 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_Dec08MoveTo( 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]; + iPlace1 = Var2Pla[v]+1; + If_Dec08SwapAdjacent( 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_Dec08Copy( pF, pIn, nVars ); + assert( Pla2Var[p] == v ); +} + +// derive binary function +static inline int If_Dec08DeriveCount2( 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_Dec08HasVar( word * t, int nVars, int iVar ) +{ + int nWords = If_Dec08WordNum( 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_Dec08Support( word * t, int nVars ) +{ + int v, Supp = 0; + for ( v = 0; v < nVars; v++ ) + if ( If_Dec08HasVar( t, nVars, v ) ) + Supp |= (1 << v); + return Supp; +} + +// checks +void If_Dec08Cofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 ) +{ + int nWords = If_Dec08WordNum( 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_Dec08Count16( 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_Dec08Perform( word * pF, int nVars, int fDerive ) +{ +// static int Cnt = 0; + word pCof0[16], pCof1[16]; + int Pla2Var[10], Var2Pla[10], Count[210], Masks[210]; + int i, i0,i1,i2, v, x; + assert( nVars >= 6 && nVars <= 8 ); + // start arrays + for ( i = 0; i < nVars; i++ ) + { + assert( If_Dec08HasVar( pF, nVars, i ) ); + Pla2Var[i] = Var2Pla[i] = i; + } +/* + Cnt++; +//if ( Cnt == 108 ) +{ +printf( "%d\n", Cnt ); +//Extra_PrintHex( stdout, (unsigned *)pF, nVars ); +//printf( "\n" ); +Kit_DsdPrintFromTruth( (unsigned *)pF, nVars ); +printf( "\n" ); +printf( "\n" ); +} +*/ + // generate permutations + v = 0; + for ( i0 = 0; i0 < nVars; i0++ ) + for ( i1 = i0+1; i1 < nVars; i1++ ) + for ( i2 = i1+1; i2 < nVars; i2++, v++ ) + { + If_Dec08MoveTo( pF, nVars, i0, nVars-1, Pla2Var, Var2Pla ); + If_Dec08MoveTo( pF, nVars, i1, nVars-2, Pla2Var, Var2Pla ); + If_Dec08MoveTo( pF, nVars, i2, nVars-3, Pla2Var, Var2Pla ); + If_DecVerifyPerm( Pla2Var, Var2Pla, nVars ); + Count[v] = If_Dec08CofCount( pF, nVars ); + Masks[v] = (1 << i0) | (1 << i1) | (1 << i2); + assert( Count[v] > 1 ); +//printf( "%d ", Count[v] ); + if ( Count[v] == 2 || Count[v] > 5 ) + continue; + for ( x = 0; x < 4; x++ ) + { + If_Dec08Cofactors( pF, nVars, nVars-1-x, pCof0, pCof1 ); + if ( If_Dec08CofCount2(pCof0, nVars) <= 2 && If_Dec08CofCount2(pCof1, nVars) <= 2 ) + { + Count[v] = -Count[v]; + break; + } + } + } +//printf( "\n" ); + 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_Dec08Count16(Masks[i0] & Masks[i1]) > 8 - nVars ) + continue; + if ( nVars == 8 ) + { + if ( Count[i0] == 2 && Count[i1] == 2 ) + return 1; + } + else if ( nVars == 7 ) + { + 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; + } + } +// printf( "not found\n" ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Performs additional check.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutPerformCheck08( unsigned * pTruth, int nVars, int nLeaves ) +{ + int nSupp, fDerive = 0; + word z[2] = {0}, pF[16]; + if ( nLeaves <= 5 ) + return 1; + If_Dec08Copy( pF, (word *)pTruth, nVars ); + nSupp = If_Dec08Support( pF, nLeaves ); + if ( !nSupp || !If_DecSuppIsMinBase(nSupp) ) + return 0; + if ( If_Dec08Perform( pF, nLeaves, fDerive ) ) + { +// printf( "1" ); + return 1; +// If_Dec08Verify( t, nLeaves, NULL ); + } +// printf( "0" ); + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/map/if/module.make b/src/map/if/module.make index 0482c831..b60e2691 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/ifDec07.c \ + src/map/if/ifDec08.c \ src/map/if/ifDec10.c \ src/map/if/ifLib.c \ src/map/if/ifMan.c \ -- cgit v1.2.3