Special BLIF writing.

7 files changed, 540 insertions, 9 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 74c4b01a..d9b1b253 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -837,6 +837,7 @@ extern ABC_DLL char *             Abc_SopEncoderLog( Mem_Flex_t * pMan, int iBit
 extern ABC_DLL char *             Abc_SopDecoderPos( Mem_Flex_t * pMan, int nValues );
 extern ABC_DLL char *             Abc_SopDecoderLog( Mem_Flex_t * pMan, int nValues );
 extern ABC_DLL word               Abc_SopToTruth( char * pSop, int nInputs );
+extern ABC_DLL void               Abc_SopToTruth7( char * pSop, int nInputs, word r[2] );
 /*=== abcStrash.c ==========================================================*/
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 424f6bd1..39097cb4 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -1201,6 +1201,66 @@ word Abc_SopToTruth( char * pSop, int nInputs )
     return Result;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the node.]
+ 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SopToTruth7( char * pSop, int nInputs, word r[2] )
+{
+    static word Truth[7][2] = {
+        {0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA},
+        {0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC},
+        {0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0},
+        {0xFF00FF00FF00FF00,0xFF00FF00FF00FF00},
+        {0xFFFF0000FFFF0000,0xFFFF0000FFFF0000},
+        {0xFFFFFFFF00000000,0xFFFFFFFF00000000},
+        {0x0000000000000000,0xFFFFFFFFFFFFFFFF},
+    };
+    word Cube[2];
+    int v, lit = 0;
+    int nVars = Abc_SopGetVarNum(pSop);
+    assert( nVars >= 0 && nVars <= 7 );
+    assert( nVars == nInputs );
+    r[0] = r[1] = 0;
+    do {
+        Cube[0] = Cube[1] = ~0;
+        for ( v = 0; v < nVars; v++, lit++ )
+        {
+            if ( pSop[lit] == '1' )
+            {
+                Cube[0] &=  Truth[v][0];
+                Cube[1] &=  Truth[v][1];
+            }
+            else if ( pSop[lit] == '0' )
+            {
+                Cube[0] &= ~Truth[v][0];
+                Cube[1] &= ~Truth[v][1];
+            }
+            else if ( pSop[lit] != '-' )
+                assert( 0 );
+        }
+        r[0] |= Cube[0];
+        r[1] |= Cube[1];
+        assert( pSop[lit] == ' ' );
+        lit++;
+        lit++;
+        assert( pSop[lit] == '\n' );
+        lit++;
+    } while ( pSop[lit] );
+    if ( Abc_SopIsComplement(pSop) )
+    {
+        r[0] = ~r[0];
+        r[1] = ~r[1];
+    }
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d2ebf6a2..13411203 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8554,6 +8554,29 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ManStop( pGia );
 }
 */
+/*
+{
+    extern void Abc_BddTest( Aig_Man_t * pAig, int fNew );
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
+    Abc_BddTest( pAig, fVeryVerbose );
+    Aig_ManStop( pAig );
+}
+*/
+/*
+{
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    extern Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex );
+    if ( pAbc->pCex && pNtk )
+    {
+        Abc_Cex_t * pNew;
+        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        pNew = Saig_PhaseTranslateCex( pAig, pAbc->pCex );
+        Aig_ManStop( pAig );
+        Abc_FrameReplaceCex( pAbc, &pNew );
+    }
+}
+*/
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1230cd8e..c0f6b5a9 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1533,13 +1533,16 @@ usage:
 int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
-    int c;
+    int c, fSpecial = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "jh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'j':
+                fSpecial ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1556,12 +1559,16 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
+//    if ( fSpecial )
+//        Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName );
+//    else
+        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_blif [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_blif [-jh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the network into a BLIF file\n" );
+    fprintf( pAbc->Err, "\t-j     : enables special BLIF writing [default = %s]\n", fSpecial? "yes" : "no" );;
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .blif)\n" );
     return 1;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index d5415384..841fce40 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -105,6 +105,7 @@ extern void               Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName );
 extern void               Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
 extern void               Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches, int fBb2Wb, int fSeq );
 extern void               Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
+extern void               Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteBlifMv.c ==========================================================*/ 
 extern void               Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteBench.c =========================================================*/
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index cade2ea9..2a28f6ab 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -21,6 +21,7 @@
 #include "ioAbc.h"
 #include "main.h"
 #include "mio.h"
+#include "kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -624,6 +625,248 @@ void Abc_NtkConvertBb2Wb( char * pFileNameIn, char * pFileNameOut, int fSeq, int
     Abc_NtkDelete( pNetlist );
 }
 
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms truth table into an SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_NtkDeriveSop( Mem_Flex_t * pMem, unsigned uTruth, int nVars )
+{
+    char * pSop;
+    Vec_Int_t * vCover = Vec_IntAlloc( 100 );
+    int RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 1 );
+    assert( RetValue == 0 || RetValue == 1 );
+    // check the case of constant cover
+    assert( !(Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0)) );
+    // derive the AIG for that tree
+    pSop = Abc_SopCreateFromIsop( pMem, nVars, vCover );
+    if ( RetValue )
+        Abc_SopComplement( pSop );
+    Vec_IntFree( vCover );
+    return pSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write the node into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pNet;
+    int i, nVars = Abc_ObjFaninNum(pNode);
+    if ( nVars > 7 )
+    {
+        printf( "Node \"%s\" has more than 7 inputs. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        return;
+    }
+    if ( nVars <= 4 )
+    {
+        // write the .names line
+        fprintf( pFile, ".names" );
+        Abc_ObjForEachFanin( pNode, pNet, i )
+            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        // get the output name
+        fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        // write the cubes
+        fprintf( pFile, "%s", (char*)Abc_ObjData(pNode) );
+    }
+    else
+    {
+        extern int  If_Dec6PickBestMux( word t, word Cofs[2] );
+        extern int  If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] );
+        extern word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars );
+        extern void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars );
+        extern word If_Dec6Perform( word t, int fDerive );
+        extern word If_Dec7Perform( word t[2], int fDerive );
+
+        char * pSop;
+        word z, uTruth6, uTruth7[2], Cofs6[2], Cofs7[2][2];
+        int c, iVar, nVarsMin[2], pVars[2][10];
+
+        // collect variables
+        Abc_ObjForEachFanin( pNode, pNet, i )
+            pVars[0][i] = pVars[1][i] = i;
+
+        // derive truth table
+        if ( nVars == 7 )
+        {
+            Abc_SopToTruth7( (char*)Abc_ObjData(pNode), nVars, uTruth7 );
+            iVar = If_Dec7PickBestMux( uTruth7, Cofs7[0], Cofs7[1] );
+        }
+        else
+        {
+            uTruth6 = Abc_SopToTruth( (char*)Abc_ObjData(pNode), nVars );
+            iVar = If_Dec6PickBestMux( uTruth6, Cofs6 );
+        }
+        // perform MUX decomposition
+        if ( iVar >= 0 )
+        {
+            if ( nVars == 7 )
+            {
+                If_Dec7MinimumBase( Cofs7[0], pVars[0], nVars, &nVarsMin[0] );
+                If_Dec7MinimumBase( Cofs7[1], pVars[1], nVars, &nVarsMin[1] );
+            }
+            else
+            {
+                Cofs6[0] = If_Dec6MinimumBase( Cofs6[0], pVars[0], nVars, &nVarsMin[0] );
+                Cofs6[1] = If_Dec6MinimumBase( Cofs6[1], pVars[1], nVars, &nVarsMin[1] );
+            }
+            assert( nVarsMin[0] < 5 );
+            assert( nVarsMin[1] < 5 );
+            // write cofactors
+            for ( c = 0; c < 2; c++ )
+            {
+                pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, 
+                    (unsigned)(nVars == 7 ? Cofs7[c][0] : Cofs6[c]), nVarsMin[c] );
+                fprintf( pFile, ".names" );
+                for ( i = 0; i < nVarsMin[c]; i++ )
+                    fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
+                fprintf( pFile, " %s_cascade%d\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c );
+                fprintf( pFile, "%s", pSop );
+            }
+            // write MUX
+            fprintf( pFile, ".names" );
+            fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,iVar)) );
+            fprintf( pFile, " %s_cascade0", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            fprintf( pFile, " %s_cascade1", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            fprintf( pFile, "1-1 1\n01- 1\n" );
+            return;
+        }
+
+        // try cascade decomposition
+        if ( nVars == 7 )
+            z = If_Dec7Perform( uTruth7, 1 );
+        else
+            z = If_Dec6Perform( uTruth6, 1 );
+        if ( z == 0 )
+        {
+            printf( "Node \"%s\" is not decomposable. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            return;
+        }
+
+        // collect the nodes
+        for ( c = 0; c < 2; i++ )
+        {
+            uTruth7[c]  = ((c ? z >> 32 : z) & 0xffff);
+            uTruth7[c] |= (uTruth7[c] << 16);
+            uTruth7[c] |= (uTruth7[c] << 32);
+            for ( i = 0; i < 4; i++ )
+                pVars[c][i] = (z >> (c*32+16+4*i)) & 7;
+
+            // minimize truth table
+            Cofs6[i] = If_Dec6MinimumBase( uTruth7[i], pVars[i], 4, &nVarsMin[i] );
+            assert( c ? nVarsMin[0] == 4 : nVarsMin[1] <= 4 );
+
+            // write the nodes
+            pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, (unsigned)Cofs6[c], nVarsMin[c] );
+            fprintf( pFile, ".names" );
+            for ( i = 0; i < nVarsMin[c]; i++ )
+                if ( pVars[c][i] == 7 )
+                    fprintf( pFile, " %s_cascade", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+                else
+                    fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
+            fprintf( pFile, " %s%s\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c? "_cascade" : "" );
+            fprintf( pFile, "%s", pSop );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write the network into a BLIF file with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode, * pLatch;
+    int i;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // start writing the file
+    pFile = fopen( FileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteBlifInt(): Cannot open the output file.\n" );
+        return;
+    }
+    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    // write the model name
+    fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
+    // write the PIs
+    fprintf( pFile, ".inputs" );
+    Io_NtkWritePis( pFile, pNtk, 1 );
+    fprintf( pFile, "\n" );
+    // write the POs
+    fprintf( pFile, ".outputs" );
+    Io_NtkWritePos( pFile, pNtk, 1 );
+    fprintf( pFile, "\n" );
+    // write the latches
+    if ( Abc_NtkLatchNum(pNtk) )
+        fprintf( pFile, "\n" );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Io_NtkWriteLatch( pFile, pLatch );
+    if ( Abc_NtkLatchNum(pNtk) )
+        fprintf( pFile, "\n" );
+    // write each internal node
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Io_NtkWriteNodeInt( pFile, pNode );
+    // write the end
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write the network into a BLIF file with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName )
+{
+    Abc_Ntk_t * pNtkTemp;
+    assert( Abc_NtkIsLogic(pNtk) );
+    Abc_NtkToSop( pNtk, 0 );
+    // derive the netlist
+    pNtkTemp = Abc_NtkToNetlist(pNtk);
+    if ( pNtkTemp == NULL )
+    {
+        fprintf( stdout, "Writing BLIF has failed.\n" );
+        return;
+    }
+    Io_WriteBlifInt( pNtkTemp, FileName );
+    Abc_NtkDelete( pNtkTemp );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifDec.c b/src/map/if/ifDec.c
index 7409c05a..2dd91cd2 100644
--- a/src/map/if/ifDec.c
+++ b/src/map/if/ifDec.c
@@ -390,6 +390,14 @@ static inline int If_Dec6HasVar( word t, int v )
 {
     return ((t & Truth6[v]) >> (1<<v)) != (t & ~Truth6[v]);
 }
+static inline int If_Dec7HasVar( word t[2], int v )
+{
+    assert( v >= 0 && v < 7 );
+    if ( v == 6 )
+        return t[0] != t[1]; 
+    return ((t[0] & Truth6[v]) >> (1<<v)) != (t[0] & ~Truth6[v])
+        || ((t[1] & Truth6[v]) >> (1<<v)) != (t[1] & ~Truth6[v]);
+}
 
 static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
 {
@@ -397,7 +405,7 @@ static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
     for ( i = 0; i < 6; i++ )
         assert( Pla2Var[Var2Pla[i]] == i );
 } 
-static word If_Dec6Perform( word t, int fDerive )
+word If_Dec6Perform( word t, int fDerive )
 { 
     word r = 0;
     int i, v, u, x, Count, Pla2Var[6], Var2Pla[6];
@@ -437,7 +445,7 @@ static word If_Dec6Perform( word t, int fDerive )
     assert( i == 15 );
     return r;
 }
-static word If_Dec7Perform( word t0[2], int fDerive )
+word If_Dec7Perform( word t0[2], int fDerive )
 {
     word t[2] = {t0[0], t0[1]}; 
     int i, v, u, y, Pla2Var[7], Var2Pla[7];
@@ -468,6 +476,190 @@ static word If_Dec7Perform( word t0[2], int fDerive )
 }
 
 
+// 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<<iVar));
+            r[1] = (t[1] & Truth6[iVar]) | ((t[1] & Truth6[iVar]) >> (1<<iVar));
+        }
+        else
+        {
+            r[0] = (t[0] &~Truth6[iVar]) | ((t[0] &~Truth6[iVar]) << (1<<iVar));
+            r[1] = (t[1] &~Truth6[iVar]) | ((t[1] &~Truth6[iVar]) << (1<<iVar));
+        }
+    }
+}
+static inline int If_Dec7SuppSize( word t[2] )
+{
+    word c0[2], c1[2];
+    int v, Count = 0;
+    for ( v = 0; v < 7; v++ )
+    {
+        If_Dec7Cofactor( t, v, 0, c0 );
+        If_Dec7Cofactor( t, v, 1, c1 );
+        if ( c0[0] != c1[0] || c0[1] != c1[1] )
+            Count++;
+    }
+    return Count;
+}
+static inline int If_Dec7CheckMux( word t[2] )
+{
+    word c0[2], c1[2];
+    int v;
+    for ( v = 0; v < 7; v++ )
+    {
+        If_Dec7Cofactor( t, v, 0, c0 );
+        If_Dec7Cofactor( t, v, 1, c1 );
+        if ( If_Dec7SuppSize(c0) < 5 && If_Dec7SuppSize(c1) < 5 )
+            return v;
+    }
+    return -1;
+}
+
+// find the best MUX decomposition
+int If_Dec6PickBestMux( word t, word Cofs[2] )
+{
+    int v, vBest = -1, Count0, Count1, CountBest = 1000;
+    for ( v = 0; v < 6; v++ )
+    {
+        Count0 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 0) );
+        Count1 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 1) );
+        if ( Count0 < 5 && Count1 < 5 && CountBest > 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 < 6; 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.]
@@ -486,17 +678,21 @@ int If_CutPerformCheckInt( unsigned * pTruth, int nVars, int nLeaves )
         return 1;
     if ( nLeaves == 6 )
     {
-        word t = ((word *)pTruth)[0];
-        word z = If_Dec6Perform( t, fDerive );
+        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 t[2], z;
+        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 );