Added another specialized check to the mapper.

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

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;

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 );

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 )

src/map/if/ifDec.c → src/map/if/ifDec07.c

 /**CFile****************************************************************
 
-  FileName    [ifDec.c]
+  FileName    [ifDec07.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - November 21, 2006.]
 
-  Revision    [$Id: ifDec.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+  Revision    [$Id: ifDec07.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -671,7 +671,7 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutPerformCheck( unsigned * pTruth, int nVars, int nLeaves )
+int If_CutPerformCheck07( unsigned * pTruth, int nVars, int nLeaves )
 {
     int fDerive = 1;
     if ( nLeaves < 6 )

src/map/if/ifDec08.c

+/**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
+

src/map/if/module.make

 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 \