Updating LUT synthesis code.

8 files changed, 604 insertions, 127 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 9de9e735..0f200bfc 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3460,6 +3460,8 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis )
     // create PIs
     if ( fTrimPis )
     {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = ~0;
         Vec_PtrForEachEntry( Gia_Obj_t *, vLeaves, pObj, i )
             pObj->Value = Gia_ManAppendCi( pNew );
     }
diff --git a/src/aig/gia/giaMinLut.c b/src/aig/gia/giaMinLut.c
index 79bd32fd..9ac9e770 100644
--- a/src/aig/gia/giaMinLut.c
+++ b/src/aig/gia/giaMinLut.c
@@ -89,15 +89,12 @@ void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO
     *pvSimO = vSimO;
     printf( "Read %d words of simulation data for %d inputs and %d outputs (padded %d zero-patterns).\n", nWords, nIns, nOuts, nWords*64-nLines );
 }
-void Gia_ManSimInfoTransform( int fSmall )
+void Gia_ManSimInfoTransform( char * pFileName, char * pFileOut1, char * pFileOut2, int nIns, int nOuts )
 {
-    int nIns  = fSmall ? 32 : 64;
-    int nOuts = fSmall ? 10 : 35;
-    char * pFileName = fSmall ? "io_s.txt" : "io_l.txt";
     Vec_Wrd_t * vSimI, * vSimO;
     Vec_WrdReadText( pFileName, &vSimI, &vSimO, nIns, nOuts );
-    Vec_WrdDumpBin( Extra_FileNameGenericAppend(pFileName, ".simi"), vSimI, 1 );
-    Vec_WrdDumpBin( Extra_FileNameGenericAppend(pFileName, ".simo"), vSimO, 1 );
+    Vec_WrdDumpBin( pFileOut1 ? pFileOut1 : Extra_FileNameGenericAppend(pFileName, ".simi"), vSimI, 1 );
+    Vec_WrdDumpBin( pFileOut2 ? pFileOut2 : Extra_FileNameGenericAppend(pFileName, ".simo"), vSimO, 1 );
     Vec_WrdFree( vSimI );
     Vec_WrdFree( vSimO );
 }
@@ -180,8 +177,25 @@ int Gia_ManSimEvalOne( Gia_Man_t * p, Vec_Wrd_t * vSimO, Vec_Wrd_t * vSimO_new )
         Abc_TtOrXor( pSim0, pSimImpl, pSimGold, nWords );
     }
     Count = Abc_TtCountOnesVec( pSim0, nWords );
-    printf( "Number of failed patterns is %d (out of %d). The first one is %d.\n", 
-        Count, 64*nWords, Abc_TtFindFirstBit2(pSim0, nWords) );
+    printf( "Number of failed patterns is %d (%8.4f %% of %d). The first one is %d.\n", 
+        Count, 100.0*Count/(64*nWords), 64*nWords, Abc_TtFindFirstBit2(pSim0, nWords) );
+    ABC_FREE( pSim0 );
+    return Count;
+}
+int Gia_ManSimEvalOne2( Gia_Man_t * p, Vec_Wrd_t * vSimO, Vec_Wrd_t * vSimO_new )
+{
+    int i, Count = 0, nWords = Vec_WrdSize(vSimO) / Gia_ManCoNum(p);
+    word * pSim0 = ABC_CALLOC( word, nWords );
+    assert( Vec_WrdSize(vSimO) == Vec_WrdSize(vSimO_new) );
+    for ( i = 0; i < Gia_ManCoNum(p); i++ )
+    {
+        word * pSimGold = Vec_WrdEntryP( vSimO,     i * nWords );
+        word * pSimImpl = Vec_WrdEntryP( vSimO_new, i * nWords );
+        Abc_TtXor( pSim0, pSimImpl, pSimGold, nWords, 0 );
+        Count += Abc_TtCountOnesVec( pSim0, nWords );
+    }
+    printf( "Number of failed patterns is %d (%8.4f %% of %d). The first one is %d.\n", 
+        Count, 100.0*Count/(64*nWords*Gia_ManCoNum(p)), 64*nWords*Gia_ManCoNum(p), Abc_TtFindFirstBit2(pSim0, nWords) );
     ABC_FREE( pSim0 );
     return Count;
 }
@@ -204,29 +218,12 @@ Vec_Wrd_t * Gia_ManSimInfoTry( Gia_Man_t * p, Vec_Wrd_t * vSimI )
 }
 int Gia_ManSimInfoEval( Gia_Man_t * p, Vec_Wrd_t * vSimO, Vec_Wrd_t * vSimO_new )
 {
-    int nResult = Gia_ManSimEvalOne(p, vSimO, vSimO_new);
-    Vec_WrdDumpBin( "temp.simo", vSimO_new, 1 );
+    int nResult = Gia_ManSimEvalOne2(p, vSimO, vSimO_new);
+    //Vec_WrdDumpBin( "temp.simo", vSimO_new, 1 );
     printf( "Total errors = %d.  ", nResult );
-    printf( "Density of output patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimO_new), Vec_WrdSize(vSimO_new))/(64*Vec_WrdSize(vSimO_new)) );
+    printf( "Density of output patterns %8.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimO_new), Vec_WrdSize(vSimO_new))/(64*Vec_WrdSize(vSimO_new)) );
     return nResult;
 }
-void Gia_ManSimInfoTryTest( Gia_Man_t * p, int fSmall )
-{
-    abctime clk = Abc_Clock();
-    char * pFileNameI = fSmall ? "io_s.simi" : "io_l.simi";
-    char * pFileNameO = fSmall ? "io_s.simo" : "io_l.simo";
-    Vec_Wrd_t * vSimI = Vec_WrdReadBin( pFileNameI, 1 );
-    Vec_Wrd_t * vSimO = Vec_WrdReadBin( pFileNameO, 1 );
-    Vec_Wrd_t * vSimO_new;
-    printf( "Density of input  patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimI), Vec_WrdSize(vSimI))/(64*Vec_WrdSize(vSimI)) );
-    printf( "Density of output patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimO), Vec_WrdSize(vSimO))/(64*Vec_WrdSize(vSimO)) );
-    vSimO_new = Gia_ManSimInfoTry( p, vSimI );
-    Gia_ManSimInfoEval( p, vSimO, vSimO_new );
-    Vec_WrdFree( vSimI );
-    Vec_WrdFree( vSimO );
-    Vec_WrdFree( vSimO_new );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-}
 void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2, int fCompare )
 {
     abctime clk = Abc_Clock();
@@ -234,8 +231,8 @@ void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2,
     {
         Vec_Wrd_t * vSim1 = Vec_WrdReadBin( pFileName,  1 );
         Vec_Wrd_t * vSim2 = Vec_WrdReadBin( pFileName2, 1 );
-        printf( "Density of input  patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSim1), Vec_WrdSize(vSim1))/(64*Vec_WrdSize(vSim1)) );
-        printf( "Density of output patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSim2), Vec_WrdSize(vSim2))/(64*Vec_WrdSize(vSim2)) );
+        printf( "Density of input  patterns %8.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSim1), Vec_WrdSize(vSim1))/(64*Vec_WrdSize(vSim1)) );
+        printf( "Density of output patterns %8.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSim2), Vec_WrdSize(vSim2))/(64*Vec_WrdSize(vSim2)) );
         Gia_ManSimInfoEval( p, vSim1, vSim2 );
         Vec_WrdFree( vSim1 );
         Vec_WrdFree( vSim2 );
@@ -244,8 +241,8 @@ void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2,
     {
         Vec_Wrd_t * vSimI = Vec_WrdReadBin( pFileName, 1 );
         Vec_Wrd_t * vSimO = Gia_ManSimInfoTry( p, vSimI );
-        printf( "Density of input  patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimI), Vec_WrdSize(vSimI))/(64*Vec_WrdSize(vSimI)) );
-        printf( "Density of output patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimO), Vec_WrdSize(vSimO))/(64*Vec_WrdSize(vSimO)) );
+        printf( "Density of input  patterns %8.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimI), Vec_WrdSize(vSimI))/(64*Vec_WrdSize(vSimI)) );
+        printf( "Density of output patterns %8.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimO), Vec_WrdSize(vSimO))/(64*Vec_WrdSize(vSimO)) );
         Vec_WrdDumpBin( pFileName2, vSimO, 1 );
         Vec_WrdFree( vSimI );
         Vec_WrdFree( vSimO );
@@ -264,7 +261,7 @@ void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2,
   SeeAlso     []
 
 ***********************************************************************/
-word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose )
+word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare )
 {
     Gia_Obj_t * pObj;
     int i, k, nUsed = 0, nGood = 0;
@@ -287,8 +284,8 @@ word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp
     for ( k = 0; k < nMints; k++ )
     {
         nUsed += (pCounts[k] > 0);
-        nGood += (pCounts[k] > Thresh);
-        if ( pCounts[k] > Thresh )
+        nGood += (pCounts[k] >= Thresh);
+        if ( pCounts[k] >= Thresh )
             Abc_TtXorBit( pRes, k );
         //printf( "%d ", pCounts[k] );
     }
@@ -297,6 +294,7 @@ word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp
     printf( "Used %4d and good %4d (out of %4d).\n", nUsed, nGood, nMints ); 
     ABC_FREE( pSims );
     ABC_FREE( pCounts );
+    *pCare = nGood;
     return pRes;
 }
 void Gia_ManCollectSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp )
@@ -324,7 +322,7 @@ Vec_Int_t * Gia_ManCollectSupp( Gia_Man_t * p, int iOut, int nOuts )
         Gia_ManCollectSupp_rec( p, Gia_ObjFaninId0p(p, Gia_ManCo(p, iOut+i)), vSupp );
     return vSupp;
 }
-Gia_Man_t * Gia_ManSimInfoSynth( Gia_Man_t * p, char * pFileName, int nIns, int nOuts, int LutSize, int Thresh, int fVerbose )
+Gia_Man_t * Gia_ManPerformLNetOpt( Gia_Man_t * p, char * pFileName, int nIns, int nOuts, int Thresh, int fVerbose )
 {
     extern int Kit_TruthToGia2( Gia_Man_t * p, unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
     Gia_Man_t * pNew; Gia_Obj_t * pObj;
@@ -332,12 +330,12 @@ Gia_Man_t * Gia_ManSimInfoSynth( Gia_Man_t * p, char * pFileName, int nIns, int
     Vec_Int_t * vLeaves = Vec_IntAlloc( nIns );
     Vec_Wrd_t * vSimI = pFileName ? Vec_WrdReadBin( pFileName, 1 ) : NULL;  
     word * pTruth0 = ABC_CALLOC( word, Abc_Truth6WordNum(nIns) );
-    word * pTruth1 = ABC_CALLOC( word, Abc_Truth6WordNum(nIns) ); int g, k;
+    word * pTruth1 = ABC_CALLOC( word, Abc_Truth6WordNum(nIns) ); int g, k; float CareAve = 0;
     if ( vSimI )
     {
         int nPats = 64*Vec_WrdSize(vSimI)/Gia_ManCiNum(p);
-        printf( "Density of input  patterns %6.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimI), Vec_WrdSize(vSimI))/(64*Vec_WrdSize(vSimI)) );
-        printf( "The number of patterns %d with threshold %d (%6.2f %%).\n", nPats, Thresh, 100.0*Thresh/nPats );
+        printf( "Density of input  patterns %8.4f.\n", (float)Abc_TtCountOnesVec(Vec_WrdArray(vSimI), Vec_WrdSize(vSimI))/(64*Vec_WrdSize(vSimI)) );
+        printf( "Using patterns with count %d and higher as cares (%8.4f %% of all patterns).\n", Thresh, 100.0*Thresh/nPats );
     }
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
@@ -351,9 +349,10 @@ Gia_Man_t * Gia_ManSimInfoSynth( Gia_Man_t * p, char * pFileName, int nIns, int
     for ( g = 0; g < Gia_ManCoNum(p); g += nOuts )
     {
         Vec_Int_t * vSupp = Gia_ManCollectSupp( p, g, nOuts );
-        int Temp = fVerbose ? printf( "Group %3d / %3d / %3d : Supp = %3d   %s", g, nOuts, Gia_ManCoNum(p), Vec_IntSize(vSupp), vSimI ? "":"\n" ) : 0;
-        word * pCare = vSimI ? Gia_ManCountFraction( p, vSimI, vSupp, Thresh, fVerbose ) : ABC_FALLOC( word, Abc_Truth6WordNum(Vec_IntSize(vSupp)) );
+        int Care, Temp = fVerbose ? printf( "Group %3d / %3d / %3d : Supp = %3d   %s", g, nOuts, Gia_ManCoNum(p), Vec_IntSize(vSupp), vSimI ? "":"\n" ) : 0;
+        word * pCare = vSimI ? Gia_ManCountFraction( p, vSimI, vSupp, Thresh, fVerbose, &Care ) : ABC_FALLOC( word, Abc_Truth6WordNum(Vec_IntSize(vSupp)) );
         int nWords = Abc_Truth6WordNum( Vec_IntSize(vSupp) );
+        CareAve += 100.0*Care/(1 << nIns);
         assert( Vec_IntSize(vSupp) <= nIns );
         Vec_IntClear( vLeaves );
         Gia_ManForEachObjVec( vSupp, p, pObj, k )
@@ -376,6 +375,8 @@ Gia_Man_t * Gia_ManSimInfoSynth( Gia_Man_t * p, char * pFileName, int nIns, int
         Vec_IntFree( vSupp );
         Temp = 0;
     }
+    CareAve /= Gia_ManCoNum(p)/nOuts;
+    printf( "Average size of the care set = %8.4f %%.\n", CareAve );
     Gia_ManHashStop( pNew );
     Gia_ManForEachCo( p, pObj, k )
         pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
@@ -430,14 +431,15 @@ Gia_Man_t * Gia_ManDoMuxTransform( Gia_Man_t * p, int fReorder )
 {
     extern Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
-    extern int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit, int fReorder );
+    extern int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit, int fReorder, int fUseAdd );
     Gia_Man_t * pRes = NULL;
     Aig_Man_t * pMan = Gia_ManToAig( p, 0 );
     Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan );
     Abc_Ntk_t * pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
     pNtk->pName = Extra_UtilStrsav( pMan->pName );
     Aig_ManStop( pMan );
-    if ( Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew, 1000000, fReorder ) )
+    //pNtkNew = Abc_NtkBddToMuxes( pNtk, 1, 1000000, 1 );
+    if ( Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew, 1000000, fReorder, 0 ) )
     {
         Abc_Ntk_t * pStrash = Abc_NtkStrash( pNtkNew, 1, 1, 0 );
         pRes = Abc_NtkStrashToGia( pStrash );
@@ -457,37 +459,135 @@ int Gia_ManDoTest1( Gia_Man_t * p, int fReorder )
     Gia_ManStop( pNew );
     return Res;
 }
-Gia_Man_t * Gia_ManPerformMinLut( Gia_Man_t * p, int GroupSize, int LutSize, int fVerbose )
+Abc_Ntk_t * Gia_ManDoTest2( Gia_Man_t * p, int fReorder )
 {
-    Gia_Man_t * pNew = NULL;
+    extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs );
+    Abc_Ntk_t * pNtkNew;
+    Gia_Man_t * pTemp, * pNew;
+    pNew = Gia_ManDoMuxTransform( p, fReorder );
+    pNew = Gia_ManDoMuxMapping( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    pNtkNew = Abc_NtkFromMappedGia( pNew, 0, 0 );
+    pNtkNew->pName = Extra_UtilStrsav(p->pName);
+    Gia_ManStop( pNew );
+    Abc_NtkToSop( pNtkNew, 1, ABC_INFINITY );
+    return pNtkNew;
+}
+Abc_Ntk_t * Abc_NtkMapTransform( Gia_Man_t * p, int nOuts, int fUseFixed, int fVerbose )
+{
+    extern Abc_Ntk_t * Abc_NtkSpecialMapping( Abc_Ntk_t * pNtk, int fVerbose );
+    int i, k, g, nGroups = Gia_ManCoNum(p) / nOuts, CountsAll[3] = {0}; 
+    Abc_Obj_t * pObjNew, * pFaninNew;  Gia_Obj_t * pObj;
+    Abc_Ntk_t * pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    assert( Gia_ManCoNum(p) % nOuts == 0 );
+    pNtkNew->pName = Extra_UtilStrsav(p->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
+    Gia_ManFillValue( p );
+    Gia_ManForEachPi( p, pObj, i )
+        Abc_NtkCreatePi( pNtkNew );
+    Gia_ManForEachPo( p, pObj, i )
+        Abc_NtkCreatePo( pNtkNew );
+    assert( nOuts <= 64 );
+    for ( g = 0; g < nGroups; g++ )
+    {
+        Gia_Man_t * pNew;   Aig_Man_t * pMan;
+        Abc_Ntk_t * pNtk, * pNtkRes, * pNtkMap;
+        int pPos[64], Counter = 0, Counts[3] = {0};
+        for ( i = 0; i < nOuts; i++ )
+            pPos[i] = g*nOuts+i;
+        pNew = Gia_ManDupCones( p, pPos, nOuts, 1 );
+        if ( !fUseFixed )
+            pNtkMap = Gia_ManDoTest2( pNew, 1 );
+        else
+        {
+            pMan = Gia_ManToAig( pNew, 0 );
+            pNtk = Abc_NtkFromAigPhase( pMan );
+            Aig_ManStop( pMan );
+            pNtkRes = Abc_NtkBddToMuxes( pNtk, 1, 1000000, 1 );
+            Abc_NtkDelete( pNtk );
+            pNtkMap = Abc_NtkSpecialMapping( pNtkRes, 0 );
+            Abc_NtkDelete( pNtkRes );
+        }
+        Gia_ManStop( pNew );
+        Gia_ManForEachCi( p, pObj, i )
+            if ( ~pObj->Value )
+                Abc_NtkCi(pNtkMap, Counter++)->pCopy = Abc_NtkCi(pNtkNew, i);
+        assert( Counter == Abc_NtkCiNum(pNtkMap) );
+        Abc_NtkForEachNode( pNtkMap, pObjNew, i )
+        {
+            pObjNew->pCopy = Abc_NtkDupObj( pNtkNew, pObjNew, 0 );
+            pObjNew->pCopy->fPersist = pObjNew->fPersist;
+            if ( pObjNew->fPersist )
+                Counts[1]++;
+            else
+                Counts[0]++;
+            Abc_ObjForEachFanin( pObjNew, pFaninNew, k )
+                Abc_ObjAddFanin( pObjNew->pCopy, pFaninNew->pCopy );
+        }
+        Abc_NtkForEachCo( pNtkMap, pObjNew, i )
+            Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, g*nOuts+i), Abc_ObjFanin0(pObjNew)->pCopy );
+        Abc_NtkDelete( pNtkMap );
+
+        if ( fVerbose )
+        {
+        printf( "%3d / %3d :  ", g, nGroups );
+        printf( "Test   = %4d   ", Counts[0] );
+        printf( "MarkA  = %4d   ", Counts[1] );
+        printf( "MarkB  = %4d   ", Counts[2] );
+        printf( "\n" );
+        }
+
+        CountsAll[0] += Counts[0];
+        CountsAll[1] += Counts[1];
+        CountsAll[2] += Counts[2];
+    }
+    if ( fVerbose )
+    printf( "Total LUT count = %5d.  MarkA = %5d. MarkB = %5d.\n", CountsAll[0], CountsAll[1], CountsAll[2] );
+    // create names
+    Abc_NtkAddDummyPiNames( pNtkNew );
+    Abc_NtkAddDummyPoNames( pNtkNew );
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    // check the resulting AIG
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+Abc_Ntk_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fVerbose )
+{
+    int fPrintOnly = 0;
     int Res1, Res2, Result = 0;
     int g, nGroups = Gia_ManCoNum(p) / GroupSize;
     assert( Gia_ManCoNum(p) % GroupSize == 0 );
     assert( GroupSize <= 64 );
-    for ( g = 0; g < nGroups; g++ )
+    if ( fPrintOnly )
     {
-        Gia_Man_t * pNew;//, * pTemp;
-        int fTrimPis = 0;
-        int o, pPos[64];
-        for ( o = 0; o < GroupSize; o++ )
-            pPos[o] = g*GroupSize+o;
-        pNew = Gia_ManDupCones( p, pPos, GroupSize, fTrimPis );
-        printf( "%3d / %3d :  ", g, nGroups );
-        printf( "Test1 = %4d   ", Res1 = Gia_ManDoTest1(pNew, 0) );
-        printf( "Test2 = %4d   ", Res2 = Gia_ManDoTest1(pNew, 1) );
-        printf( "Test  = %4d   ", Abc_MinInt(Res1, Res2) );
-        printf( "\n" );
-        Result += Abc_MinInt(Res1, Res2);
-        //Gia_ManPrintStats( pNew, NULL );
-        Gia_ManStop( pNew );
+        for ( g = 0; g < nGroups; g++ )
+        {
+            Gia_Man_t * pNew;
+            int o, pPos[64];
+            for ( o = 0; o < GroupSize; o++ )
+                pPos[o] = g*GroupSize+o;
+            pNew = Gia_ManDupCones( p, pPos, GroupSize, 0 );
+            printf( "%3d / %3d :  ", g, nGroups );
+            printf( "Test1 = %4d   ", Res1 = Gia_ManDoTest1(pNew, 0) );
+            printf( "Test2 = %4d   ", Res2 = Gia_ManDoTest1(pNew, 1) );
+            printf( "Test  = %4d   ", Abc_MinInt(Res1, Res2) );
+            printf( "\n" );
+            Result += Abc_MinInt(Res1, Res2);
+            //Gia_ManPrintStats( pNew, NULL );
+            Gia_ManStop( pNew );
+        }
+        printf( "Total LUT count = %d.\n", Result );
+        return NULL;
+
     }
-    printf( "Total LUT count = %d.\n", Result );
-    return pNew;
+    return Abc_NtkMapTransform( p, GroupSize, fUseFixed, fVerbose );
 }
 
 #else
 
-Gia_Man_t * Gia_ManPerformMinLut( Gia_Man_t * p, int GroupSize, int LutSize, int fVerbose )
+Gia_Man_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fVerbose )
 {
     return NULL;
 }
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 7c54f3c4..f8e40b41 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1286,6 +1286,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     void * pAttrMan;
     int TotalMemory, i;
+    int fWarning = 0;
 //    int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
@@ -1310,9 +1311,11 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
 //            ABC_FREE( pObj->vFanouts.pArray );
         // these flags should be always zero
         // if this is not true, something is wrong somewhere
-        assert( pObj->fMarkA == 0 );
-        assert( pObj->fMarkB == 0 );
-        assert( pObj->fMarkC == 0 );
+//        assert( pObj->fMarkA == 0 );
+//        assert( pObj->fMarkB == 0 );
+//        assert( pObj->fMarkC == 0 );
+        if ( !fWarning && (pObj->fMarkA || pObj->fMarkB || pObj->fMarkC) )
+            { printf( "Flags A, B, or C are not zero.\n" ), fWarning = 1; }
     }
     // free the nodes
     if ( pNtk->pMmStep == NULL )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 84734e6f..ab80eef3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -485,8 +485,9 @@ static int Abc_CommandAbc9Of                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Pack               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Edge               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9MinLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9MinSim             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetSim             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetOpt             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetMap             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Unmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Struct             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Trace              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1210,8 +1211,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&pack",         Abc_CommandAbc9Pack,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&edge",         Abc_CommandAbc9Edge,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&satlut",       Abc_CommandAbc9SatLut,       0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&minlut",       Abc_CommandAbc9MinLut,       0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&minsim",       Abc_CommandAbc9MinSim,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetsim",      Abc_CommandAbc9LNetSim,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetopt",      Abc_CommandAbc9LNetOpt,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetmap",      Abc_CommandAbc9LNetMap,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&trace",        Abc_CommandAbc9Trace,        0 );
@@ -10411,7 +10413,7 @@ int Abc_CommandPutOnTop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Ntk_t * Abc_NtkPutOnTop( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtk2 );
 
-    Abc_Ntk_t * pNtk, * pNtk2, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtk2, * pNtkRes = NULL;
     char * FileName;
     int fComb = 0;
     int c;
@@ -10431,6 +10433,39 @@ int Abc_CommandPutOnTop( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
+    if ( argc > globalUtilOptind + 1 )
+    {
+        Abc_Ntk_t * pStrash;
+        for ( c = 1; c < argc; c++ )
+        {
+            Abc_Ntk_t * pTemp, * pLogic = Io_Read( argv[c], Io_ReadFileType(argv[c]), 1, 0 );
+            if ( pLogic == NULL )
+                return 1;
+            if ( Abc_NtkIsStrash(pLogic) )
+            {
+                pLogic = Abc_NtkToLogic( pTemp = pLogic );
+                Abc_NtkDelete( pTemp );
+            }
+            if ( pLogic == NULL )
+                return 1;
+            if ( pNtkRes == NULL )
+                pNtkRes = pLogic;
+            else
+            {
+                pNtkRes = Abc_NtkPutOnTop( pTemp = pNtkRes, pLogic );
+                Abc_NtkDelete( pTemp );
+                Abc_NtkDelete( pLogic );
+                if ( pNtkRes == NULL )
+                    return 1;
+            }
+        }
+        assert( Abc_NtkIsLogic(pNtkRes) );
+        pStrash = Abc_NtkStrash( pNtkRes, 1, 1, 0 );
+        Abc_FrameReplaceCurrentNetwork( pAbc, pStrash );
+        Abc_NtkDelete( pNtkRes );
+        return 0;
+    }
+
     // get the second network
     if ( argc != globalUtilOptind + 1 )
     {
@@ -10492,6 +10527,7 @@ usage:
     Abc_Print( -2, "\t         connects PIs of network in <file> to POs of current network\n" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : file name with the second network\n");
+    Abc_Print( -2, "\t       : (given several files, all networks are stacked on top of each other)\n");
     return 1;
 }
 
@@ -14054,6 +14090,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Dau_NetworkEnumTest();
     //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
     //Mnist_ExperimentWithScaling( nDecMax );
+    if ( Abc_FrameReadNtk(pAbc) )
+    {
+        extern Abc_Ntk_t * Abc_NtkSpecialMapping( Abc_Ntk_t * pNtk, int fVerbose );
+        Abc_Ntk_t * pNtkRes = Abc_NtkSpecialMapping( Abc_FrameReadNtk(pAbc), 0 );
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    }
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -40838,15 +40880,12 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9MinLut( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9LNetSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_ManSimInfoSynth( Gia_Man_t * p, char * pFileName, int nIns, int nOuts, int LutSize, int Thresh, int fVerbose );
-    //extern Gia_Man_t * Gia_ManPerformMinLut( Gia_Man_t * p, int GroupSize, int LutSize, int fVerbose );
-    Gia_Man_t * pTemp;
-    char * pFileName = NULL;
-    int c, nIns = 6, nOuts = 2, LutSize = 6, Limit = -1, fVerbose = 0;
+    extern void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2, int fCompare );
+    int c, nIns = 6, nOuts = 2, fCompare = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "IOKLvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IOcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -40868,19 +40907,94 @@ int Abc_CommandAbc9MinLut( Abc_Frame_t * pAbc, int argc, char ** argv )
             nOuts = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
-        case 'K':
+        case 'c':
+            fCompare ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+    if ( argc == globalUtilOptind + 3 )
+    {
+        extern void Gia_ManSimInfoTransform( char * pFileName, char * pFileOut1, char * pFileOut2, int nIns, int nOuts );
+        Gia_ManSimInfoTransform( argv[globalUtilOptind], argv[globalUtilOptind+1], argv[globalUtilOptind+2], nIns, nOuts );
+        return 0;
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty GIA network.\n" );
+        return 1;
+    }
+    if ( argc != globalUtilOptind + 2 )
+    {
+        Abc_Print( -1, "Expecting two file names on the command line.\n" );
+        return 1;
+    }
+    Gia_ManSimInfoPassTest( pAbc->pGia, argv[globalUtilOptind], argv[globalUtilOptind+1], fCompare );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &lnetsim [-IO num] [-cvh] <file> <file2> <file3>\n" );
+    Abc_Print( -2, "\t           performs specialized AIG simulation\n" );
+    Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",        nIns );
+    Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",         nOuts );
+    Abc_Print( -2, "\t-c       : toggles comparing simulation patterns [default = %s]\n",  fCompare? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",                 fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    Abc_Print( -2, "\t<file>   : file name with simulation information\n");
+    Abc_Print( -2, "\t<file2>  : file name with simulation information\n");
+    Abc_Print( -2, "\t<file3>  : file name with simulation information (optional)\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9LNetOpt( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManPerformLNetOpt( Gia_Man_t * p, char * pFileName, int nIns, int nOuts, int Thresh, int fVerbose );
+    Gia_Man_t * pTemp;
+    char * pFileName = NULL;
+    int c, nIns = 6, nOuts = 2, Limit = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IORvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
                 goto usage;
             }
-            LutSize = atoi(argv[globalUtilOptind]);
+            nIns = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
-        case 'L':
+        case 'O':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by a positive integer.\n" );
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nOuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" );
                 goto usage;
             }
             Limit = atoi(argv[globalUtilOptind]);
@@ -40894,6 +41008,10 @@ int Abc_CommandAbc9MinLut( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( argc > globalUtilOptind + 1 )
+    {
+        return 0;
+    }
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Empty GIA network.\n" );
@@ -40910,20 +41028,17 @@ int Abc_CommandAbc9MinLut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fclose( pFile );
         pFileName = argv[globalUtilOptind];
     }
-    //pTemp = Gia_ManPerformMinLut( pAbc->pGia, GroupSize, LutSize, fVerbose );
-    //Abc_FrameUpdateGia( pAbc, pTemp );
-    pTemp = Gia_ManSimInfoSynth( pAbc->pGia, pFileName, nIns, nOuts, LutSize, Limit, fVerbose );
+    pTemp = Gia_ManPerformLNetOpt( pAbc->pGia, pFileName, nIns, nOuts, Limit, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &minlut [-IOKL num] [-vh] <file>\n" );
-    Abc_Print( -2, "\t           performs specialized LUT mapping\n" );
-    Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",        nIns );
-    Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",         nOuts );
-    Abc_Print( -2, "\t-K num   : the LUT size for mapping [default = %d]\n",      LutSize );
-    Abc_Print( -2, "\t-L num   : patterns count after this limit [default = %d]\n", Limit );
-    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",        fVerbose? "yes": "no" );
+    Abc_Print( -2, "usage: &lnetopt [-IOR num] [-vh] <file>\n" );
+    Abc_Print( -2, "\t           performs specialized AIG optimization\n" );
+    Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",          nIns );
+    Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",           nOuts );
+    Abc_Print( -2, "\t-R num   : patterns are cares starting this value [default = %d]\n", Limit );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",          fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     Abc_Print( -2, "\t<file>   : file name with simulation information\n");
     return 1;
@@ -40940,17 +41055,37 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9MinSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9LNetMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2, int fCompare );
-    int c, fCompare = 0, fVerbose = 0;
+    extern Abc_Ntk_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fVerbose );
+    Abc_Ntk_t * pTemp;
+    char * pFileName = NULL;
+    int c, nIns = 6, nOuts = 2, fUseFixed = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IOfvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'c':
-            fCompare ^= 1;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nIns = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nOuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'f':
+            fUseFixed ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -40965,22 +41100,30 @@ int Abc_CommandAbc9MinSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty GIA network.\n" );
         return 1;
     }
-    if ( argc != globalUtilOptind + 2 )
+    if ( argc == globalUtilOptind + 1 )
     {
-        Abc_Print( -1, "Expecting two file names on the command line.\n" );
-        return 1;
+        FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for writing the proof.\n", argv[globalUtilOptind] );
+            return 0;
+        }
+        fclose( pFile );
+        pFileName = argv[globalUtilOptind];
     }
-    Gia_ManSimInfoPassTest( pAbc->pGia, argv[globalUtilOptind], argv[globalUtilOptind+1], fCompare );
+    pTemp = Gia_ManPerformLNetMap( pAbc->pGia, nOuts, fUseFixed, fVerbose );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &minsim [-cvh] <file> <file2>\n" );
-    Abc_Print( -2, "\t           performs specialized AIG simulation\n" );
-    Abc_Print( -2, "\t-c       : toggles comparing simulation patterns [default = %s]\n",  fCompare? "yes": "no" );
-    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",                 fVerbose? "yes": "no" );
+    Abc_Print( -2, "usage: &lnetmap [-IO num] [-fvh] <file>\n" );
+    Abc_Print( -2, "\t           performs specialized LUT mapping\n" );
+    Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",         nIns );
+    Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",          nOuts );
+    Abc_Print( -2, "\t-f       : toggles using fixed primitives [default = %s]\n", fUseFixed? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",         fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     Abc_Print( -2, "\t<file>   : file name with simulation information\n");
-    Abc_Print( -2, "\t<file2>  : file name with simulation information\n");
     return 1;
 }
 
@@ -48562,7 +48705,6 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManSimInfoTryTest( Gia_Man_t * p, int fSmall );
     extern void Gia_RsbEnumerateWindows( Gia_Man_t * p, int nInputsMax, int nLevelsMax );
     extern int Gia_ManSumTotalOfSupportSizes( Gia_Man_t * p );
     int c, fVerbose = 0;
@@ -48626,7 +48768,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        return 1;
 //    }
 //    Abc_FrameUpdateGia( pAbc, Abc_Procedure(pAbc->pGia) );
-    Gia_ManSimInfoTryTest( pAbc->pGia, fSwitch );
 //    printf( "AIG in \"%s\" has the sum of output support sizes equal to %d.\n", pAbc->pGia->pSpec, Gia_ManSumTotalOfSupportSizes(pAbc->pGia) );
     return 0;
 usage:
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index edc2b7de..8dc84ba0 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -783,6 +783,164 @@ int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs specialized mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static word s__Truths6[6] = {
+    ABC_CONST(0xAAAAAAAAAAAAAAAA),
+    ABC_CONST(0xCCCCCCCCCCCCCCCC),
+    ABC_CONST(0xF0F0F0F0F0F0F0F0),
+    ABC_CONST(0xFF00FF00FF00FF00),
+    ABC_CONST(0xFFFF0000FFFF0000),
+    ABC_CONST(0xFFFFFFFF00000000)
+};
+word Abc_ObjComputeTruth( Abc_Obj_t * pObj, Vec_Int_t * vSupp )
+{
+    int Index; word t0, t1, tc;
+    assert( Vec_IntSize(vSupp) <= 6 );
+    if ( (Index = Vec_IntFind(vSupp, Abc_ObjId(pObj))) >= 0 )
+        return s__Truths6[Index];
+    assert( Abc_ObjIsNode(pObj) );
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+        return Abc_NodeIsConst0(pObj) ? (word)0 : ~(word)0;
+    assert( Abc_ObjFaninNum(pObj) == 3 );
+    t0 = Abc_ObjComputeTruth( Abc_ObjFanin(pObj, 2), vSupp );
+    t1 = Abc_ObjComputeTruth( Abc_ObjFanin(pObj, 1), vSupp );
+    tc = Abc_ObjComputeTruth( Abc_ObjFanin(pObj, 0), vSupp );
+    return (tc & t1) | (~tc & t0);
+}
+Abc_Obj_t * Abc_NtkSpecialMap_rec( Abc_Ntk_t * pNew, Abc_Obj_t * pObj, Vec_Wec_t * vSupps, Vec_Int_t * vCover )
+{
+    if ( pObj->pCopy )
+        return pObj->pCopy;
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+        return NULL;
+    assert( Abc_ObjFaninNum(pObj) == 3 );
+    if ( pObj->fMarkA || pObj->fMarkB )
+    {
+        Abc_Obj_t * pFan0 = Abc_NtkSpecialMap_rec( pNew, Abc_ObjFanin(pObj, 2), vSupps, vCover );
+        Abc_Obj_t * pFan1 = Abc_NtkSpecialMap_rec( pNew, Abc_ObjFanin(pObj, 1), vSupps, vCover );
+        Abc_Obj_t * pFanC = Abc_NtkSpecialMap_rec( pNew, Abc_ObjFanin(pObj, 0), vSupps, vCover );
+        if ( pFan0 == NULL )
+            pFan0 = Abc_NodeIsConst0(Abc_ObjFanin(pObj, 2)) ? Abc_NtkCreateNodeConst0(pNew) : Abc_NtkCreateNodeConst1(pNew);
+        if ( pFan1 == NULL )
+            pFan1 = Abc_NodeIsConst0(Abc_ObjFanin(pObj, 1)) ? Abc_NtkCreateNodeConst0(pNew) : Abc_NtkCreateNodeConst1(pNew);
+        pObj->pCopy = Abc_NtkCreateNodeMux( pNew, pFanC, pFan1, pFan0 );
+        pObj->pCopy->fMarkA = pObj->fMarkA;
+        pObj->pCopy->fMarkB = pObj->fMarkB;
+    }
+    else
+    {
+        Abc_Obj_t * pTemp; int i; word Truth;
+        Vec_Int_t * vSupp = Vec_WecEntry( vSupps, Abc_ObjId(pObj) );
+        Abc_NtkForEachObjVec( vSupp, pObj->pNtk, pTemp, i )
+            Abc_NtkSpecialMap_rec( pNew, pTemp, vSupps, vCover );
+        pObj->pCopy = Abc_NtkCreateNode( pNew );   
+        Abc_NtkForEachObjVec( vSupp, pObj->pNtk, pTemp, i )
+            Abc_ObjAddFanin( pObj->pCopy, pTemp->pCopy );
+        Truth = Abc_ObjComputeTruth( pObj, vSupp );
+        pObj->pCopy->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNew->pManFunc, Vec_IntSize(vSupp), &Truth, vCover );
+        assert( Abc_SopGetVarNum((char *)pObj->pCopy->pData) == Vec_IntSize(vSupp) );
+    }
+    return pObj->pCopy;
+}
+Abc_Ntk_t * Abc_NtkSpecialMapping( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
+    Vec_Wec_t * vSupps = Vec_WecStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_Obj_t * pObj, * pFan0, * pFan1, * pFanC; int i, Count[2] = {0};
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Vec_IntPush( Vec_WecEntry(vSupps, i), i );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        Vec_Int_t * vSupp = Vec_WecEntry(vSupps, i);
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        assert( Abc_ObjFaninNum(pObj) == 3 );
+        pFan0 = Abc_ObjFanin( pObj, 2 );
+        pFan1 = Abc_ObjFanin( pObj, 1 );
+        pFanC = Abc_ObjFanin0( pObj );
+        assert( Abc_ObjIsCi(pFanC) );
+        if ( pFan0->fMarkA && pFan1->fMarkA )
+        {
+            pObj->fMarkB = 1;
+            Vec_IntPush( vSupp, Abc_ObjId(pObj) );
+            continue;
+        }
+        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Abc_ObjId(pFan0)), Vec_WecEntry(vSupps, Abc_ObjId(pFan1)), vSupp );
+        assert( Vec_IntFind(vSupp, Abc_ObjId(pFanC)) == -1 );
+        Vec_IntPushOrder( vSupp, Abc_ObjId(pFanC) );
+        if ( Vec_IntSize(vSupp) <= 6 )
+            continue;
+        Vec_IntClear( vSupp );
+        if ( !pFan0->fMarkA && !pFan1->fMarkA )
+        {
+            pObj->fMarkA = 1;
+            Vec_IntPush( vSupp, Abc_ObjId(pObj) );
+        }
+        else
+        {
+            Vec_IntPushOrder( vSupp, Abc_ObjId(pFan0) );
+            Vec_IntPushOrder( vSupp, Abc_ObjId(pFan1) );
+            Vec_IntPushOrder( vSupp, Abc_ObjId(pFanC) );
+        }
+    }
+
+    if ( fVerbose )
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        printf( "Node %4d : ", i );
+        if ( pObj->fMarkA )
+            printf( " MarkA  " );
+        else
+            printf( "        " );
+        if ( pObj->fMarkB )
+            printf( " MarkB  " );
+        else
+            printf( "        " );
+        Vec_IntPrint( Vec_WecEntry(vSupps, i) );
+    }
+
+    Abc_NtkCleanCopy( pNtk );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 0 )
+            Abc_ObjFanin0(pObj)->pCopy = Abc_NodeIsConst0(Abc_ObjFanin0(pObj)) ? Abc_NtkCreateNodeConst0(pNtkNew) : Abc_NtkCreateNodeConst1(pNtkNew);
+        else
+            Abc_NtkSpecialMap_rec( pNtkNew, Abc_ObjFanin0(pObj), vSupps, vCover );
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkCleanMarkAB( pNtk );
+    Vec_WecFree( vSupps );
+    Vec_IntFree( vCover );
+
+    Abc_NtkForEachNode( pNtkNew, pObj, i )
+    {
+        Count[0] += pObj->fMarkA,
+        Count[1] += pObj->fMarkB;
+        pObj->fPersist = pObj->fMarkA | pObj->fMarkB;
+        pObj->fMarkA = pObj->fMarkB = 0;
+    }
+    //printf( "Total = %3d.  Nodes = %3d. MarkA = %3d. MarkB = %3d.\n", Abc_NtkNodeNum(pNtkNew), 
+    //    Abc_NtkNodeNum(pNtkNew) - Count[0] - Count[1], Count[0], Count[1] );
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkSpecialMapping: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 3c28ce4f..cbf4bbb8 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -274,7 +274,7 @@ int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limi
     Abc_Obj_t * pObj, * pObjNew; int i;
     st__table * tBdd2Node;
     assert( Abc_NtkIsStrash(pNtk) );
-    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, Limit, 1, 1, fReorder, 0 );
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, Limit, 1, fReorder, 0, 0 );
     if ( dd == NULL )
     {
         printf( "Construction of global BDDs has failed.\n" );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index dec5ee45..5cf74ef9 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2982,13 +2982,13 @@ usage:
 ***********************************************************************/
 int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
 {
-    extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize );
+    extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules );
     char * pFileName;
-    int c, fOnlyAnds = 0;
+    int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0;
     int nLutSize = -1;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Kah" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3003,9 +3003,15 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
                 if ( nLutSize < 2 || nLutSize > 6 )
                     goto usage;
                 break;
+            case 'f':
+                fFixed ^= 1;
+                break;
             case 'a':
                 fOnlyAnds ^= 1;
                 break;
+            case 'm':
+                fNoModules ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -3019,6 +3025,8 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
+    if ( fFixed )
+        nLutSize = 6;
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
@@ -3031,16 +3039,18 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
         Abc_NtkDelete( pNtkTemp );
     }
     else if ( nLutSize >= 2 && nLutSize <= 6 )
-        Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize );
+        Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules );
     else
         Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_verilog [-K num] [-ah] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the current network in Verilog format\n" );
     fprintf( pAbc->Err, "\t-K num : write the network using instances of K-LUTs (2 <= K <= 6) [default = not used]\n" );
+    fprintf( pAbc->Err, "\t-f     : toggle using fixed format [default = %s]\n", fFixed? "yes":"no" );
     fprintf( pAbc->Err, "\t-a     : toggle writing expressions with only ANDs (without XORs and MUXes) [default = %s]\n", fOnlyAnds? "yes":"no" );
+    fprintf( pAbc->Err, "\t-m     : toggle writing additional modules [default = %s]\n", !fNoModules? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index 4c55b599..e05aed2e 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -639,10 +639,8 @@ int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
 char * Io_WriteVerilogGetName( char * pName )
 {
     static char Buffer[500];
-    int Length, i;
-    Length = strlen(pName);
-    // consider the case of a signal having name "0" or "1"
-    if ( !(Length == 1 && (pName[0] == '0' || pName[0] == '1')) )
+    int i, Length = strlen(pName);
+    if ( pName[0] < '0' || pName[0] > '9' )
     {
         for ( i = 0; i < Length; i++ )
             if ( !((pName[i] >= 'a' && pName[i] <= 'z') || 
@@ -679,7 +677,39 @@ void Io_WriteLutModule( FILE * pFile, int nLutSize )
     fprintf( pFile, "    assign out = TT[in];\n" );
     fprintf( pFile, "endmodule\n\n" );
 }
-void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize )
+void Io_WriteFixedModules( FILE * pFile )
+{    
+    fprintf( pFile, "module LUT6 #( parameter INIT = 64\'h0000000000000000 ) (\n" );
+    fprintf( pFile, "    output O,\n" );
+    fprintf( pFile, "    input I0,\n" );
+    fprintf( pFile, "    input I1,\n" );
+    fprintf( pFile, "    input I2,\n" );
+    fprintf( pFile, "    input I3,\n" );
+    fprintf( pFile, "    input I4,\n" );
+    fprintf( pFile, "    input I5\n" );
+    fprintf( pFile, ");\n" );
+    fprintf( pFile, "    assign O = INIT[ {I5, I4, I3, I2, I1, I0} ];\n" );
+    fprintf( pFile, "endmodule\n\n" );
+
+    fprintf( pFile, "module MUXF7 (\n" );
+    fprintf( pFile, "    output O,\n" );
+    fprintf( pFile, "    input I0,\n" );
+    fprintf( pFile, "    input I1,\n" );
+    fprintf( pFile, "    input S\n" );
+    fprintf( pFile, ");\n" );
+    fprintf( pFile, "    assign O = S ? I1 : I0;\n" );
+    fprintf( pFile, "endmodule\n\n" );
+
+    fprintf( pFile, "module MUXF8 (\n" );
+    fprintf( pFile, "    output O,\n" );
+    fprintf( pFile, "    input I0,\n" );
+    fprintf( pFile, "    input I1,\n" );
+    fprintf( pFile, "    input S\n" );
+    fprintf( pFile, ");\n" );
+    fprintf( pFile, "    assign O = S ? I1 : I0;\n" );
+    fprintf( pFile, "endmodule\n\n" );
+}
+void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed )
 {
     Abc_Ntk_t * pNtkBox;
     Abc_Obj_t * pObj, * pTerm;
@@ -719,6 +749,34 @@ void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize )
     // write LUT instances
     nDigits = Abc_Base10Log( Abc_NtkNodeNum(pNtk) );
     Counter = 0;
+    if ( fFixed )
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( pObj->fPersist )
+        {
+            int One = Abc_ObjFanin0(Abc_ObjFanin(pObj, 1))->fPersist && Abc_ObjFanin0(Abc_ObjFanin(pObj, 2))->fPersist;
+            fprintf( pFile, "  MUXF%d                       ", 7+One );
+            fprintf( pFile, " mux_%0*d (", nDigits, Counter++ );
+            fprintf( pFile, " %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+            for ( k = Abc_ObjFaninNum(pObj) - 1; k >= 0; k-- )
+                fprintf( pFile, ", %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin(pObj, k))) );
+            fprintf( pFile, " );\n" );
+        }
+        else
+        {
+            word Truth = Abc_SopToTruth( (char *)pObj->pData, Abc_ObjFaninNum(pObj) );
+            fprintf( pFile, "  LUT6 #(64\'h" );
+            fprintf( pFile, "%08x%08x", (unsigned)(Truth >> 32), (unsigned)Truth );
+            fprintf( pFile, ") lut_%0*d (", nDigits, Counter++ );
+            fprintf( pFile, " %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+            for ( k = 0; k < Abc_ObjFaninNum(pObj); k++ )
+                fprintf( pFile, ", %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin(pObj, k))) );
+            for (      ; k < 6; k++ )
+                fprintf( pFile, ", %*s", Length, "1\'b0" );
+            fprintf( pFile, " );\n" );
+        }
+    }
+    else
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         word Truth = Abc_SopToTruth( (char *)pObj->pData, Abc_ObjFaninNum(pObj) );
@@ -735,7 +793,7 @@ void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize )
         fprintf( pFile, "}, %*s );\n", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
     }
 }
-void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize )
+void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed )
 {
     // write inputs and outputs
 //    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
@@ -786,7 +844,7 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize )
             fprintf( pFile, ";\n\n" );
         }
         // write nodes
-        Io_WriteVerilogObjectsLut( pFile, pNtk, nLutSize );        
+        Io_WriteVerilogObjectsLut( pFile, pNtk, nLutSize, fFixed );        
         // write registers
         if ( Abc_NtkLatchNum(pNtk) > 0 )
         {
@@ -797,7 +855,7 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize )
     // finalize the file
     fprintf( pFile, "\nendmodule\n\n" );
 } 
-void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize )
+void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules )
 {
     FILE * pFile;
     Abc_Ntk_t * pNtkTemp;
@@ -827,11 +885,16 @@ void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize )
     // write the equations for the network
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     fprintf( pFile, "\n" );
-    Io_WriteLutModule( pFile, nLutSize );
-
+    if ( !fNoModules )
+    {
+        if ( fFixed )
+            Io_WriteFixedModules( pFile );
+        else
+            Io_WriteLutModule( pFile, nLutSize );
+    }
     pNtkTemp = Abc_NtkToNetlist( pNtk );
     Abc_NtkToSop( pNtkTemp, -1, ABC_INFINITY );
-    Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize );
+    Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize, fFixed );
     Abc_NtkDelete( pNtkTemp );
 
     fprintf( pFile, "\n" );