Modified write_blif to output LUT structures.

7 files changed, 317 insertions, 33 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index cf0526a9..de5bc663 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -849,6 +849,7 @@ extern ABC_DLL char *             Abc_SopDecoderPos( Mem_Flex_t * pMan, int nVal
 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] );
+extern ABC_DLL void               Abc_SopToTruthBig( char * pSop, int nInputs, word ** pVars, word * pCube, word * pRes );
 /*=== 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 39097cb4..2b66fc77 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -1261,6 +1261,58 @@ void Abc_SopToTruth7( char * pSop, int nInputs, word r[2] )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the node.]
+ 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SopToTruthBig( char * pSop, int nInputs, word ** pVars, word * pCube, word * pRes )
+{
+    int nVars = Abc_SopGetVarNum(pSop);
+    int nWords = nVars <= 6 ? 1 : 1 << (nVars-6);
+    int v, i, lit = 0;
+    assert( nVars >= 0 && nVars <= 16 );
+    assert( nVars == nInputs );
+    for ( i = 0; i < nWords; i++ )
+        pRes[i] = 0;
+    do {
+        for ( i = 0; i < nWords; i++ )
+            pCube[i] = ~0;
+        for ( v = 0; v < nVars; v++, lit++ )
+        {
+            if ( pSop[lit] == '1' )
+            {
+                for ( i = 0; i < nWords; i++ )
+                    pCube[i] &= pVars[v][i];
+            }
+            else if ( pSop[lit] == '0' )
+            {
+                for ( i = 0; i < nWords; i++ )
+                    pCube[i] &= ~pVars[v][i];
+            }
+            else if ( pSop[lit] != '-' )
+                assert( 0 );
+        }
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] |= pCube[i];
+        assert( pSop[lit] == ' ' );
+        lit++;
+        lit++;
+        assert( pSop[lit] == '\n' );
+        lit++;
+    } while ( pSop[lit] );
+    if ( Abc_SopIsComplement(pSop) )
+    {
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] = ~pRes[i];
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/io.c b/src/base/io/io.c
index d8277b08..3b85a020 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1581,13 +1581,28 @@ usage:
 int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
+    char * pLutStruct = NULL;
     int c, fSpecial = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "jh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Sjh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'S':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" );
+                    goto usage;
+                }
+                pLutStruct = argv[globalUtilOptind];
+                globalUtilOptind++;
+                if ( !strlen(pLutStruct) == 2 && !strlen(pLutStruct) == 3 ) 
+                {
+                    Abc_Print( -1, "Command line switch \"-S\" should be followed by a 2- or 3-char string (e.g. \"44\" or \"555\").\n" );
+                    goto usage;
+                }
+                break;
             case 'j':
                 fSpecial ^= 1;
                 break;
@@ -1607,15 +1622,16 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-    if ( fSpecial )
-        Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName );
+    if ( fSpecial || pLutStruct )
+        Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName, pLutStruct );
     else
         Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_blif [-jh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_blif [-S str] [-jh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the network into a BLIF file\n" );
+    fprintf( pAbc->Err, "\t-S str : string representing the LUT structure [default = %s]\n", pLutStruct ? pLutStruct : "not used" );  
     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" );
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index fa3f6240..f3db4c15 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -106,7 +106,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 );
+extern void               Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct );
 /*=== 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 dd33cfdd..e731631e 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -661,10 +661,10 @@ void Abc_NtkConvertBb2Wb( char * pFileNameIn, char * pFileNameOut, int fSeq, int
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_NtkDeriveSop( Mem_Flex_t * pMem, unsigned uTruth, int nVars, Vec_Int_t * vCover )
+char * Io_NtkDeriveSop( Mem_Flex_t * pMem, word uTruth, int nVars, Vec_Int_t * vCover )
 {
     char * pSop;
-    int RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 1 );
+    int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, nVars, vCover, 1 );
     assert( RetValue == 0 || RetValue == 1 );
     // check the case of constant cover
     if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
@@ -767,7 +767,7 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover )
             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], vCover );
+                    (word)(nVars == 7 ? Cofs7[c][0] : Cofs6[c]), nVarsMin[c], vCover );
                 fprintf( pFile, ".names" );
                 for ( i = 0; i < nVarsMin[c]; i++ )
                     fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
@@ -819,7 +819,7 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover )
 
             // write SOP
             pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, 
-                (unsigned)Cofs6[c], nVarsMin[c], vCover );
+                (word)Cofs6[c], nVarsMin[c], vCover );
             fprintf( pFile, "%s", pSop );
         }
     }
@@ -827,6 +827,149 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover )
 
 /**Function*************************************************************
 
+  Synopsis    [Write the node into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover, char * pStr )
+{
+    Abc_Obj_t * pNet;
+    int nLeaves = Abc_ObjFaninNum(pNode);
+    int i, nLutLeaf, nLutRoot;
+
+    // quit if parameters are wrong
+    if ( strlen(pStr) != 2 )
+    {
+        printf( "Wrong LUT struct (%s)\n", pStr );
+        return;
+    }
+    nLutLeaf = pStr[0] - '0';
+    if ( nLutLeaf < 3 || nLutLeaf > 6 )
+    {
+        printf( "Leaf size (%d) should belong to {3,4,5,6}.\n", nLutLeaf );
+        return;
+    }
+    nLutRoot = pStr[1] - '0';
+    if ( nLutRoot < 3 || nLutRoot > 6 )
+    {
+        printf( "Root size (%d) should belong to {3,4,5,6}.\n", nLutRoot );
+        return;
+    }
+    if ( nLeaves > nLutLeaf + nLutRoot - 1 )
+    {
+        printf( "Node \"%s\" has %d inputs (too many for the LUT structure \"%d%d\"). Writing BLIF has failed.\n", 
+            Abc_ObjName(Abc_ObjFanout0(pNode)), nLeaves, nLutLeaf, nLutRoot );
+        return;
+    }
+
+    // consider easy case
+    fprintf( pFile, "\n" );
+    if ( nLeaves <= Abc_MaxInt( nLutLeaf, nLutRoot ) )
+    {
+        // 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) );
+        return;
+    }
+    else
+    {
+        extern int If_CluMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars );
+        extern int If_CluCheckExt( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutRoot, char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 );
+
+        static word TruthStore[16][1<<10] = {{0}}, * pTruths[16];
+        word pCube[1<<10], pRes[1<<10], Func0, Func1;
+        char pLut0[32], pLut1[32], * pSop;
+//        int nVarsMin[3], pVars[3][20];
+
+        if ( TruthStore[0][0] == 0 )
+        {
+            static word Truth6[6] = {
+                0xAAAAAAAAAAAAAAAA,
+                0xCCCCCCCCCCCCCCCC,
+                0xF0F0F0F0F0F0F0F0,
+                0xFF00FF00FF00FF00,
+                0xFFFF0000FFFF0000,
+                0xFFFFFFFF00000000
+            };
+            int nVarsMax = 16;
+            int nWordsMax = (1 << nVarsMax);
+            int i, k;
+            assert( nVarsMax <= 16 );
+            for ( i = 0; i < nVarsMax; i++ )
+                pTruths[i] = TruthStore[i];
+            for ( i = 0; i < 6; i++ )
+                for ( k = 0; k < nWordsMax; k++ )
+                    pTruths[i][k] = Truth6[i];
+            for ( i = 6; i < nVarsMax; i++ )
+                for ( k = 0; k < nWordsMax; k++ )
+                    pTruths[i][k] = ((k >> (i-6)) & 1) ? ~0 : 0;
+        }
+
+        // collect variables
+//        Abc_ObjForEachFanin( pNode, pNet, i )
+//            pVars[0][i] = pVars[1][i] = pVars[2][i] = i;
+
+        // derive truth table
+        Abc_SopToTruthBig( (char*)Abc_ObjData(pNode), nLeaves, pTruths, pCube, pRes );
+
+//        Extra_PrintHex( stdout, (unsigned *)pRes, nLeaves );  printf( "    " );
+//        Kit_DsdPrintFromTruth( (unsigned*)pRes, nLeaves );  printf( "\n" );
+
+        // perform decomposition
+        if ( !If_CluCheckExt( NULL, pRes, nLeaves, nLutLeaf, nLutRoot, pLut0, pLut1, &Func0, &Func1 ) )
+        {
+            Extra_PrintHex( stdout, (unsigned *)pRes, nLeaves );  printf( "    " );
+            Kit_DsdPrintFromTruth( (unsigned*)pRes, nLeaves );  printf( "\n" );
+            printf( "Node \"%s\" is not decomposable. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            return;
+        }
+
+        // write leaf node
+        fprintf( pFile, ".names" );
+        for ( i = 0; i < pLut1[0]; i++ )
+            fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pLut1[2+i])) );
+        fprintf( pFile, " %s_lut1\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        // write SOP
+        pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, Func1, pLut1[0], vCover );
+        fprintf( pFile, "%s", pSop );
+/*
+        // write leaf node
+        fprintf( pFile, ".names" );
+        for ( i = 0; i < pLut2[0]; i++ )
+            fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pLut2[2+i])) );
+        fprintf( pFile, " %s_lut1\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        // write SOP
+        pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, Func2, pLut2[0], vCover );
+        fprintf( pFile, "%s", pSop );
+*/
+        // write root node
+        fprintf( pFile, ".names" );
+        for ( i = 0; i < pLut0[0]; i++ )
+            if ( pLut0[2+i] == nLeaves )
+                fprintf( pFile, " %s_lut1", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            else if ( pLut0[2+i] == nLeaves+1 )
+                fprintf( pFile, " %s_lut2", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            else
+                fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pLut0[2+i])) );
+        fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        // write SOP
+        pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, Func0, pLut0[0], vCover );
+        fprintf( pFile, "%s", pSop );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Write the network into a BLIF file with the given name.]
 
   Description []
@@ -836,7 +979,7 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
+void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
 {
     FILE * pFile;
     Vec_Int_t * vCover;
@@ -871,7 +1014,12 @@ void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
     // write each internal node
     vCover = Vec_IntAlloc( (1<<16) );
     Abc_NtkForEachNode( pNtk, pNode, i )
-        Io_NtkWriteNodeInt( pFile, pNode, vCover );
+    {
+        if ( pLutStruct )
+            Io_NtkWriteNodeIntStruct( pFile, pNode, vCover, pLutStruct );
+        else
+            Io_NtkWriteNodeInt( pFile, pNode, vCover );
+    }
     Vec_IntFree( vCover );
     // write the end
     fprintf( pFile, ".end\n\n" );
@@ -889,7 +1037,7 @@ void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName )
+void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
 {
     Abc_Ntk_t * pNtkTemp;
     assert( Abc_NtkIsLogic(pNtk) );
@@ -901,7 +1049,7 @@ void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName )
         fprintf( stdout, "Writing BLIF has failed.\n" );
         return;
     }
-    Io_WriteBlifInt( pNtkTemp, FileName );
+    Io_WriteBlifInt( pNtkTemp, FileName, pLutStruct );
     Abc_NtkDelete( pNtkTemp );
 }
 
diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c
index 39881875..87badfc4 100644
--- a/src/map/if/ifDec16.c
+++ b/src/map/if/ifDec16.c
@@ -194,7 +194,7 @@ static inline void If_CluSharp( word * pRes, word * pIn1, word * pIn2, int nVars
     int w, nWords = If_CluWordNum( nVars );
     for ( w = 0; w < nWords; w++ )
         pRes[w] = pIn1[w] & ~pIn2[w];
-}
+} 
 static inline void If_CluOr( word * pRes, word * pIn1, word * pIn2, int nVars )
 {
     int w, nWords = If_CluWordNum( nVars );
@@ -203,8 +203,10 @@ static inline void If_CluOr( word * pRes, word * pIn1, word * pIn2, int nVars )
 }
 static inline word If_CluAdjust( word t, int nVars )
 {
-    assert( nVars >= 0 && nVars < 6 );
-    t &= (1 << (1 << nVars)) - 1;
+    assert( nVars >= 0 && nVars <= 6 );
+    if ( nVars == 6 )
+        return t;
+    t &= (((word)1) << (1 << nVars)) - 1;
     if ( nVars == 0 )
         t |= t << (1<<nVars++);
     if ( nVars == 1 )
@@ -703,11 +705,11 @@ int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar )
 
                 if ( Cof0 == 0 )
                     State[0]++;
-                else if ( Cof0 == ~Truth6[iVar] )
+                else if ( Cof0 == ~0 )
                     State[1]++;
                 else if ( Cof1 == 0 )
                     State[2]++;
-                else if ( Cof1 == ~Truth6[iVar] )
+                else if ( Cof1 == ~0 )
                     State[3]++;
                 else if ( Cof0 == ~Cof1 )
                     State[4]++;
@@ -1074,28 +1076,76 @@ static inline int If_CluSupport( word * t, int nVars )
             Supp |= (1 << v);
     return Supp;
 }
+static inline void If_CluTruthShrink( word * pF, int nVars, int nVarsAll, unsigned Phase )
+{
+    word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp;
+    int i, k, Var = 0, Counter = 0;
+    assert( nVarsAll <= 16 );
+    for ( i = 0; i < nVarsAll; i++ )
+        if ( Phase & (1 << i) )
+        {
+            for ( k = i-1; k >= Var; k-- )
+            {
+                If_CluSwapAdjacent( pOut, pIn, k, nVarsAll );
+                pTemp = pIn; pIn = pOut, pOut = pTemp;
+                Counter++;
+            }
+            Var++;
+        }
+    assert( Var == nVars );
+    // swap if it was moved an odd number of times
+    if ( Counter & 1 )
+        If_CluCopy( pOut, pIn, nVarsAll );
+}
+int If_CluMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars )
+{
+    int v, iVar = 0, uSupp = 0;
+    assert( nVarsAll <= 16 );
+    for ( v = 0; v < nVarsAll; v++ )
+        if ( If_CluHasVar( t, nVarsAll, v ) )
+        {
+            uSupp |= (1 << v);
+            if ( pSupp )
+                pSupp[iVar] = pSupp[v];
+            iVar++;
+        }
+    if ( pnVars )
+        *pnVars = iVar;
+    if ( If_CluSuppIsMinBase( uSupp ) )
+        return 0;
+    If_CluTruthShrink( t, iVar, nVarsAll, uSupp );
+    return 1;
+}
 
 // returns the best group found
-If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int nLutRoot )
+If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int nLutRoot, If_Grp_t * pR, word * pFunc0, word * pFunc1 )
 {
     If_Grp_t G1 = {0}, R = {0}, * pHashed = NULL;
     word Truth, pTruth[CLU_WRD_MAX], pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX];
     int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2], pCanonPerm[CLU_VAR_MAX];
     int i, nSupp, uCanonPhase;
+    int nLutSize = p ? p->pPars->nLutSize : nVars;
     assert( nVars <= CLU_VAR_MAX );
     assert( nVars <= nLutLeaf + nLutRoot - 1 );
 
+    if ( pR )
+    {
+        pR->nVars = 0;
+        *pFunc0 = 0;
+        *pFunc1 = 0;
+    }
+
     // canonicize truth table
-    If_CluCopy( pTruth, pTruth0, p->pPars->nLutSize );
+    If_CluCopy( pTruth, pTruth0, nLutSize );
 
     if ( 0 )
     {
         uCanonPhase = If_CluSemiCanonicize( pTruth, nVars, pCanonPerm );
-        If_CluAdjustBig( pTruth, nVars, p->pPars->nLutSize );
+        If_CluAdjustBig( pTruth, nVars, nLutSize );
     }
 
 //    If_CluSemiCanonicizeVerify( pTruth, pTruth0, nVars, pCanonPerm, uCanonPhase );
-//    If_CluCopy( pTruth, pTruth0, p->pPars->nLutSize );
+//    If_CluCopy( pTruth, pTruth0, nLutSize );
 
 
  /*
@@ -1123,9 +1173,12 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int
 
 
     // check hash table
-    pHashed = If_CluHashLookup( p, pTruth );
-    if ( pHashed && pHashed->nVars != CLU_UNUSED )
-        return *pHashed;
+    if ( p )
+    {
+        pHashed = If_CluHashLookup( p, pTruth );
+        if ( pHashed && pHashed->nVars != CLU_UNUSED )
+            return *pHashed;
+    }
 
     // detect easy cofs
     G1 = If_CluDecUsingCofs( pTruth, nVars, nLutLeaf );
@@ -1169,7 +1222,7 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int
     }
 
     // derive
-    if ( 0 )
+    if ( pR )
     {
         If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, &G1 );
         if ( G1.nMyu == 2 )
@@ -1177,17 +1230,32 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int
         else
             Truth = If_CluDeriveNonDisjoint( pF, nVars, V2P, P2V, &G1, &R );
 
+        *pFunc0 = If_CluAdjust( pF[0], R.nVars );
+        *pFunc1 = If_CluAdjust( Truth, G1.nVars );
+
         // perform checking
         if ( 0 )
         {
             If_CluCheckGroup( pTruth, nVars, &G1 );
             If_CluVerify( pTruth, nVars, &G1, &R, Truth, pF );
         }
+        *pR = R;
     }
     return pHashed ? (*pHashed = G1) : G1;
 }
 
 
+// returns the best group found
+int If_CluCheckExt( If_Man_t * p, word * pTruth, int nVars, int nLutLeaf, int nLutRoot, char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 )
+{
+    If_Grp_t G, R;
+    G = If_CluCheck( p, pTruth, nVars, nLutLeaf, nLutRoot, &R, pFunc0, pFunc1 );
+    memcpy( pLut0, &R, sizeof(If_Grp_t) );
+    memcpy( pLut1, &G, sizeof(If_Grp_t) );
+//    memcpy( pLut2, &G2, sizeof(If_Grp_t) );
+    return (G.nVars > 0);
+}
+
 // computes delay of the decomposition
 float If_CluDelayMax( If_Grp_t * g, float * pDelays )
 {
@@ -1251,7 +1319,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
     }
 
     // derive the first group
-    G1 = If_CluCheck( p, (word *)If_CutTruth(pCut), nLeaves, nLutLeaf, nLutRoot );
+    G1 = If_CluCheck( p, (word *)If_CutTruth(pCut), nLeaves, nLutLeaf, nLutRoot, NULL, NULL, NULL );
     if ( G1.nVars == 0 )
         return ABC_INFINITY;
 
@@ -1334,7 +1402,7 @@ int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth, int nVars, int nLeave
         return 1;
 
     // derive the first group
-    G1 = If_CluCheck( p, (word *)pTruth, nLeaves, nLutLeaf, nLutRoot );
+    G1 = If_CluCheck( p, (word *)pTruth, nLeaves, nLutLeaf, nLutRoot, NULL, NULL, NULL );
     if ( G1.nVars == 0 )
     {
 //        printf( "-%d ", nLeaves );
@@ -1380,7 +1448,7 @@ void If_CluTest()
 
     Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" );
 
-    G = If_CluCheck( NULL, &t, nVars, nLutLeaf, nLutRoot );
+    G = If_CluCheck( NULL, &t, nVars, nLutLeaf, nLutRoot, NULL, NULL, NULL );
 
     If_CluPrintGroup( &G );
 }
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index c6aaa9c4..b0f3537c 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -127,8 +127,7 @@ void If_ManRestart( If_Man_t * p )
 ***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
-//    if ( p->nCutsUselessAll && p->pPars->fVerbose )
-    if ( p->nCutsUselessAll )
+    if ( p->pPars->fVerbose && p->nCutsUselessAll )
     {
         int i;
         for ( i = 0; i <= 16; i++ )
@@ -161,8 +160,8 @@ void If_ManStop( If_Man_t * p )
     if ( p->vSwitching )
         Vec_IntFree( p->vSwitching );
     // hash table
-    if ( p->nTableEntries )
-        printf( "Entries = %d.  Size = %d.\n", p->nTableEntries, p->nTableSize );
+    if ( p->pPars->fVerbose && p->nTableEntries )
+        printf( "Hash table:  Entries = %7d.  Size = %7d.\n", p->nTableEntries, p->nTableSize );
     ABC_FREE( p->pHashTable );
     if ( p->pMemEntries )
         Mem_FixedStop( p->pMemEntries, 0 );