Version abc90528

committer: Baruch Sterin <baruchs@gmail.com>

18 files changed, 586 insertions, 53 deletions

diff --git a/abclib.dsp b/abclib.dsp
index c3f70016..bef97f81 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3669,6 +3669,46 @@ SOURCE=.\src\aig\cgt\cgtSat.c
 # Begin Group "nal"
 
 # PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nal.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalFlop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalModels.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\nal090422\nalWrite.c
+# End Source File
 # End Group
 # Begin Group "gia"
 
@@ -3727,6 +3767,10 @@ SOURCE=.\src\aig\gia\giaEquiv.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaEra.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaFanout.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 111cc8a8..a385be3e 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -247,6 +247,33 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat )
+{
+    extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
+    Gia_Man_t * pGia;
+    Cec_ParCor_t CorPars, * pCorPars = &CorPars;
+    Cec_ManCorSetDefaultParams( pCorPars );
+    pCorPars->fLatchCorr = 1;
+    pCorPars->fUseCSat   = fUseCSat;
+    pCorPars->nBTLimit   = nConfs;
+    pGia = Gia_ManFromAigSimple( pAig );
+    Cec_ManLSCorrespondenceClasses( pGia, pCorPars );
+    Gia_ManReprToAigRepr( pAig, pGia );
+    Gia_ManStop( pGia );
+    return Aig_ManDupSimple( pAig );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implementation of new signal correspodence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat )
 {
     extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
@@ -262,6 +289,31 @@ Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat
     return Aig_ManDupSimple( pAig );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Implementation of fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose )
+{
+    Gia_Man_t * pGia;
+    Cec_ParFra_t FraPars, * pFraPars = &FraPars;
+    Cec_ManFraSetDefaultParams( pFraPars );
+    pFraPars->nBTLimit  = nConfs;
+    pFraPars->nItersMax = 20;
+    pFraPars->fVerbose  = fVerbose;
+    pGia = Gia_ManFromAigSimple( pAig );
+    Cec_ManSatSweeping( pGia, pFraPars );
+    Gia_ManReprToAigRepr( pAig, pGia );
+    Gia_ManStop( pGia );
+    return Aig_ManDupSimple( pAig );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 916414fc..6f70f7d3 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -9,6 +9,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaEmbed.c \
     src/aig/gia/giaEnable.c \
     src/aig/gia/giaEquiv.c \
+    src/aig/gia/giaEra.c \
     src/aig/gia/giaFanout.c \
     src/aig/gia/giaForce.c \
     src/aig/gia/giaFrames.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index c8d38331..a82b4d6c 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -309,7 +309,7 @@ extern ABC_DLL Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFil
 extern ABC_DLL Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
 extern ABC_DLL Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
 extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseComb( Ntl_Man_t * p );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize, int fVerbose );
 extern ABC_DLL Nwk_Man_t *     Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
 /*=== ntlInsert.c ==========================================================*/
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
@@ -354,6 +354,7 @@ extern ABC_DLL char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFile
 extern ABC_DLL int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName );
+extern ABC_DLL char *          Ntl_ModelCreateNetName( Ntl_Mod_t * p, const char * pName, int Num );
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName );
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName );
 extern ABC_DLL void            Ntl_ModelSetPioNumbers( Ntl_Mod_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index b4abe3bf..6afeba26 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -623,7 +623,7 @@ Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
+Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize, int fVerbose )
 {
     Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
@@ -645,7 +645,7 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
     // perform the traversal
     pAig = Ntl_ManCollapse( p, 1 );
     // check if there are register classes
-    pAig->vClockDoms = Ntl_ManTransformRegClasses( p, nMinDomSize, 1 );
+    pAig->vClockDoms = Ntl_ManTransformRegClasses( p, nMinDomSize, fVerbose );
     if ( pAig->vClockDoms )
     {
         if ( Vec_VecSize(pAig->vClockDoms) == 0 )
@@ -654,9 +654,10 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
             Aig_ManStop( pAig );
             pAig = NULL;
         }
-        else
+        else if ( fVerbose )
             printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) );
-        printf( "\n" );
+        if ( fVerbose )
+            printf( "\n" );
     }
     return pAig;
 }
@@ -706,7 +707,7 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
         Ntl_ManExtractNwk_rec( p, pFaninNet, pNtk, vCover, vMemory );
         Nwk_ObjAddFanin( pNode, pFaninNet->pCopy2 );
     }
-    if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 )
+    if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 || Kit_PlaGetVarNum(pNet->pDriver->pSop) == 0 )
         pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Kit_PlaIsConst0(pNet->pDriver->pSop) );
     else
     {
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 70f97d89..e98a3b46 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -219,6 +219,8 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pNode, * pNodeOld;
     int i, fCompl, Counter = 0;
+    char * pNameNew;
+//    int Lenght;
     assert( pAig->pReprs );
     pRoot = Ntl_ManRootModel( p );
     Aig_ManForEachObj( pAig, pObj, i )
@@ -276,13 +278,17 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
             printf( "Ntl_ManReduce(): Internal error! Net already has no driver.\n" );
         if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
             printf( "Ntl_ManReduce(): Internal error! Net already has a driver.\n" );
-
+/*
         // remove this net from the hash table (but do not remove from the array)
         Ntl_ModelDeleteNet( pRoot, pNet );
         // create new net with the same name
         pNetNew = Ntl_ModelFindOrCreateNet( pRoot, pNet->pName );
         // clean the name
         pNet->pName[0] = 0;
+*/
+        // create new net with a new name
+        pNameNew = Ntl_ModelCreateNetName( pRoot, "noname", (int)(ABC_PTRINT_T)pNet );
+        pNetNew = Ntl_ModelFindOrCreateNet( pRoot, pNameNew );
 
         // make the old node drive the new net without fanouts
         if ( !Ntl_ModelSetNetDriver( pNodeOld, pNetNew ) )
@@ -290,6 +296,7 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
 
         Counter++;
     }
+//    printf( "Nets without names = %d.\n", Counter );
 }
 
 /**Function*************************************************************
@@ -373,7 +380,7 @@ if ( fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose )
 {
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
@@ -392,9 +399,19 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
     }
 
     // perform fraiging for the given design
-    nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
-    pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
-    Aig_ManStop( pTemp );
+//    if ( fUseCSat )
+    if ( 0 )
+    {
+        extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose );
+        pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose );
+        Aig_ManStop( pTemp );
+    }
+    else
+    {
+        nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
+        pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -425,7 +442,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
 //Ntl_ManPrintStats( p );
 //Aig_ManPrintStats( pAig );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
+    pAigCol = Ntl_ManCollapseSeq( pNew, 0, fVerbose );
     if ( pAigCol == NULL )
     {
         Aig_ManStop( pAig );
@@ -457,7 +474,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
   SeeAlso     []
 
 ***********************************************************************/
-Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
+Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose )
 {
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
@@ -469,7 +486,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize, pPars->fVerbose );
     if ( pAigCol == NULL )
     {
         Aig_ManStop( pAig );
@@ -477,6 +494,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     }
 
     // perform LCORR for the given design
+    pPars->fScorrGia = fScorrGia;
+    pPars->fUseCSat  = fUseCSat;
     pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
     Aig_ManStop( pTemp );
 
@@ -507,7 +526,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize, pPars->fVerbose );
     if ( pAigCol == NULL )
     {
         Aig_ManStop( pAig );
@@ -545,7 +564,7 @@ Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize, pPars->fVerbose );
     if ( pAigCol == NULL )
     {
         Aig_ManStop( pAig );
@@ -724,7 +743,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     Ntl_Man_t * pNew;
     Aig_Man_t * pAigRed, * pAigCol;
     // collapse the AIG
-    pAigCol = Ntl_ManCollapseSeq( p, pPars->nMinDomSize );
+    pAigCol = Ntl_ManCollapseSeq( p, pPars->nMinDomSize, pPars->fVerbose );
     // transform the collapsed AIG
     pAigRed = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pAigRed );
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 4c9bb311..da7e2317 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -285,6 +285,88 @@ void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManStatsRegs( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+        if ( strcmp(pObj->pImplem->pName, "dff") == 0 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManStatsLuts( Nwk_Man_t * pNtk )
+{
+    return pNtk ? Nwk_ManNodeNum(pNtk) : -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManStatsLevs( Nwk_Man_t * pNtk )
+{
+    return pNtk ? Nwk_ManLevel(pNtk) : -1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManPrintStatsUpdate( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk,
+     int nRegInit, int nLutInit, int nLevInit, int Time )
+{
+    printf( "FF =%7d (%4.1f%%)  ",  Nwk_ManStatsRegs(p),    100.0*(nRegInit-Nwk_ManStatsRegs(p))/nRegInit );
+    if ( pNtk == NULL )
+        printf( "Mapping is not available.                  " );
+    else
+    {
+        printf( "Lut =%7d (%4.1f%%)  ", Nwk_ManStatsLuts(pNtk), 100.0*(nLutInit-Nwk_ManStatsLuts(pNtk))/nLutInit );
+        printf( "Lev =%4d (%4.1f%%)    ", Nwk_ManStatsLevs(pNtk), 100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit );
+    }
+    ABC_PRT( "Time", clock() - Time );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Deallocates the netlist manager.]
 
   Description []
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index d227b1b9..0b87c8be 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -65,6 +65,30 @@ Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, const char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Allocates memory for the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_ModelCreateNetName( Ntl_Mod_t * p, const char * pName, int Num )
+{
+    char * pResult;
+    char Buffer[1000];
+    assert( strlen(pName) < 900 );
+    do {
+        sprintf( Buffer, "%s%d", pName, Num++ );
+    } while ( Ntl_ModelFindNet( p, Buffer ) != NULL );
+    pResult = (char *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, strlen(Buffer) + 1 );
+    strcpy( pResult, Buffer );
+    return pResult;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resizes the table.]
 
   Description []
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 4099d738..e6e4cbdd 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -631,7 +631,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
     Ntl_Mod_t * pModel;
     int i, bzError;
     bz2file b;
-    if ( p->pNal )
+    if ( p->pNal && strncmp(pFileName+strlen(pFileName)-5,".blif",5) )
     {
         p->pNalW( p, pFileName );
         return;
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 12a72e2f..10b7b462 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -518,21 +518,9 @@ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
     Vec_Int_t * vTruth;
     Nwk_Obj_t * pObj;
     int i, Counter = 0;
-    Nwk_Obj_t * pNodeThis = pNtk->vObjs->pArray[72688];
-
     vTruth = Vec_IntAlloc( 1 << 16 );
     Nwk_ManForEachNode( pNtk, pObj, i )
-    {
-        if ( i == 641386 )
-        {
-            int x = 0;
-        }
         Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose );
-        if ( pNodeThis->nFanouts != 15 )
-        {
-            int s = 0;
-        }
-    }
     if ( fVerbose && Counter )
         printf( "Support minimization reduced support of %d nodes.\n", Counter );
     Vec_IntFree( vTruth );
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 41123ca4..6cb84800 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -280,8 +280,16 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
 
     if ( pPars->fScorrGia )
     {
-        extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
-        return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+        if ( pPars->fLatchCorrOpt )
+        {
+            extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
+            return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+        }
+        else
+        {
+            extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
+            return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+        }
     }
 
     // start the induction manager
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 138dc9a1..4540462d 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -82,7 +82,7 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
                 continue;
 //            pNtk->pManFunc = NULL;
             pNtk->pDesign = NULL;
-            if ( pNtk->pManFunc == pNtkSave->pManFunc )
+            if ( pNtkSave && pNtk->pManFunc == pNtkSave->pManFunc )
                 pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
         }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 946b7210..660bf3e1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -310,6 +310,7 @@ static int Abc_CommandAbc9Cec        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc9Force      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Embed      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Era        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Test       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbcTestNew     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -629,6 +630,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&force",        Abc_CommandAbc9Force,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&embed",        Abc_CommandAbc9Embed,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&if",           Abc_CommandAbc9If,           0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&era",          Abc_CommandAbc9Era,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&test",         Abc_CommandAbc9Test,         0 );
 
     Cmd_CommandAdd( pAbc, "Various",      "testnew",         Abc_CommandAbcTestNew,     0 );
@@ -18973,8 +18975,8 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-//        extern void * Nal_ManRead( char * pFileName );
         pAbc->pAbc8Ntl = NULL;
+//        extern void * Nal_ManRead( char * pFileName );
 //        pAbc->pAbc8Ntl = Nal_ManRead( pFileName );
 //        Ioa_WriteBlif( pAbc->pAbc8Ntl, "test_boxes.blif" );
         if ( pAbc->pAbc8Ntl == NULL )
@@ -19104,7 +19106,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
-    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize );
+    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize, int fVerbose );
 
     // set defaults
     fAig = 0;
@@ -19142,7 +19144,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fCollapsed )
         {
             extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0 );
+            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0, 0 );
             if ( fBlif )
                 Saig_ManDumpBlif( pTemp, pFileName );
             else
@@ -19632,7 +19634,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pAbc->pAbc8Lib == NULL )
     {
-        printf( "LUT library is not given. Using default LUT library.\n" );
+//        printf( "LUT library is not given. Using default LUT library.\n" );
         pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
     }
 
@@ -19774,7 +19776,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     // enable truth table computation if choices are selected
     if ( (c = Aig_ManChoiceNum( pAbc->pAbc8Aig )) )
     {
-        printf( "Performing LUT mapping with %d choices.\n", c );
+//        printf( "Performing LUT mapping with %d choices.\n", c );
         pPars->fExpRed = 0;
     }
     // enable truth table computation if cut minimization is selected
@@ -20813,17 +20815,19 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPartSize;
     int nConfLimit;
     int nLevelMax;
+    int fUseCSat;
     extern Aig_Man_t * Ntl_ManExtract( void * p );
-    extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+    extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose );
     extern void Ntl_ManFree( void * p );
 
     // set defaults
     nPartSize    = 0;
     nConfLimit   = 100;   
     nLevelMax    = 0;
+    fUseCSat     = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20860,6 +20864,9 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nLevelMax < 0 ) 
                 goto usage;
             break;
+        case 'c':
+            fUseCSat ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -20877,7 +20884,7 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fUseCSat, fVerbose );
     if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Fraig(): Tranformation of the AIG has failed.\n" );
@@ -20905,6 +20912,7 @@ usage:
     fprintf( stdout, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
     fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
     fprintf( stdout, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
+//    fprintf( stdout, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -21018,19 +21026,23 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     void * pNtlNew;
     int c;
+    int fScorrGia;
+    int fUseCSat;
     int nFramesP;
     int nConfMax;
     int fVerbose;
     extern Aig_Man_t * Ntl_ManExtract( void * p );
-    extern void * Ntl_ManLcorr( void * p, int nConfMax, int fVerbose );
+    extern void * Ntl_ManLcorr( void * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose );
     extern int Ntl_ManIsComb( void * p );
 
     // set defaults
+    fScorrGia  = 0;
+    fUseCSat   = 0;
     nFramesP   = 0;
     nConfMax   = 10000;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -21056,6 +21068,12 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMax < 0 ) 
                 goto usage;
             break;
+        case 'n':
+            fScorrGia ^= 1;
+            break;
+        case 'c':
+            fUseCSat ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -21079,7 +21097,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fVerbose );
+    pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fScorrGia, fUseCSat, fVerbose );
     if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Lcorr(): Tranformation of the AIG has failed.\n" );
@@ -21102,10 +21120,12 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *lcorr [-C num] [-vh]\n" );
+    fprintf( stdout, "usage: *lcorr [-C num] [-ncvh]\n" );
     fprintf( stdout, "\t         computes latch correspondence for the netlist\n" );
 //    fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
+    fprintf( stdout, "\t-n     : toggle using new AIG package [default = %s]\n", fScorrGia? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -21625,7 +21645,7 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
  
     // sweep the current design
     Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
-    if ( Counter == 0 )
+    if ( Counter == 0 && fVerbose )
         printf( "The netlist is unchanged by sweep.\n" );
 
     // if mapped, create new AIG and new mapped network
@@ -24508,6 +24528,7 @@ usage:
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
 }
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -24739,6 +24760,80 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp = NULL;
+    int c, fVerbose = 0;
+    int fMiter = 0;
+    int nStatesMax = 1000000;
+    extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-S\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nStatesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nStatesMax < 0 ) 
+                goto usage;
+            break;
+        case 'm':
+            fMiter ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Era(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManPiNum(pAbc->pAig) > 12 )
+    {
+        printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12.\n", Gia_ManPiNum(pAbc->pAig) );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pAig) == 0 )
+    {
+        printf( "Abc_CommandAbc9Era(): The network is combinational.\n" );
+        return 1;
+    }
+    Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &era [-S num] [-mvh]\n" );
+    fprintf( stdout, "\t          explicit reachability analysis for small sequential AIGs\n" );
+    fprintf( stdout, "\t-S num  : the max number of states to traverse (num > 0) [default = %d]\n", nStatesMax );
+    fprintf( stdout, "\t-m      : stop when the miter output is 1 [default = %s]\n", fMiter? "yes": "no" );
+    fprintf( stdout, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 5e9093e7..b77f9d77 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -20,6 +20,8 @@
 
 #include "abc.h"
 
+extern unsigned            Gia_ManRandom( int fReset );
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,13 +52,15 @@ static inline int  Abc_XsimAnd( int Value0, int Value1 )
 }
 static inline int  Abc_XsimRand2()   
 {
-    return (rand() & 1) ? XVS1 : XVS0;
+//    return (rand() & 1) ? XVS1 : XVS0;
+    return (Gia_ManRandom(0) & 1) ? XVS1 : XVS0;
 }
 static inline int  Abc_XsimRand3()   
 {
     int RetValue;
     do { 
-        RetValue = rand() & 3; 
+//        RetValue = rand() & 3; 
+        RetValue = Gia_ManRandom(0) & 3; 
     } while ( RetValue == 0 );
     return RetValue;
 }
@@ -108,7 +112,8 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS
     Abc_Obj_t * pObj;
     int i, f;
     assert( Abc_NtkIsStrash(pNtk) );
-    srand( 0x12341234 );
+//    srand( 0x12341234 );
+    Gia_ManRandom( 1 );
     // start simulation
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
     if ( fXInputs )
@@ -194,7 +199,8 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe
     Abc_Obj_t * pObj;
     int i, f;
     assert( Abc_NtkIsStrash(pNtk) );
-    srand( 0x12341234 );
+//    srand( 0x12341234 );
+    Gia_ManRandom( 1 );
     // initialize the values
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
     Abc_NtkForEachLatch( pNtk, pObj, i )
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e29a3009..ecc6302f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2343,13 +2343,17 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     FILE * pFile;
     unsigned * pTruth;
+    int fReverse = 0;
     int c;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'r':
+                fReverse ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -2394,7 +2398,7 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
     // convert to logic
     Abc_NtkToAig( pNtk );
     vTruth = Vec_IntAlloc( 0 );
-    pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, 0 );
+    pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse );
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
@@ -2408,8 +2412,9 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_truth [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_truth [-rh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes truth table into a file\n" );
+    fprintf( pAbc->Err, "\t-r     : toggle reversing bits in the truth table [default = %s]\n", fReverse? "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/ioReadBlif.c b/src/base/io/ioReadBlif.c
index b6eb29e3..f2c3e8c2 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -535,6 +535,71 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
   SeeAlso     []
 
 ***********************************************************************/
+int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate )
+{
+    Mio_Pin_t * pGatePin;
+    char * pName, * pNamePin;
+    int i, k, nSize, Length;
+    nSize = Vec_PtrSize(vTokens);
+    if ( nSize - 3 != Mio_GateReadInputs(pGate) )
+        return 0;
+    // check if the names are in order
+    for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+    {
+        pNamePin = Mio_PinReadName(pGatePin);
+        Length = strlen(pNamePin);
+        pName = Vec_PtrEntry(vTokens, i+2);
+        if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+            continue;
+        break;
+    }
+    if ( i == nSize - 3 )
+        return 1;
+    // reorder the pins
+    for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+    {
+        pNamePin = Mio_PinReadName(pGatePin);
+        Length = strlen(pNamePin);
+        for ( k = 2; k < nSize; k++ )
+        {
+            pName = Vec_PtrEntry(vTokens, k);
+            if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+            {
+                Vec_PtrPush( vTokens, pName );
+                break;
+            }
+        }
+    }
+    pNamePin = Mio_GateReadOutName(pGate);
+    Length = strlen(pNamePin);
+    for ( k = 2; k < nSize; k++ )
+    {
+        pName = Vec_PtrEntry(vTokens, k);
+        if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+        {
+            Vec_PtrPush( vTokens, pName );
+            break;
+        }
+    }
+    if ( Vec_PtrSize(vTokens) - nSize != nSize - 2 )
+        return 0;
+    Vec_PtrForEachEntryStart( vTokens, pName, k, nSize )
+        Vec_PtrWriteEntry( vTokens, k - nSize + 2, pName );
+    Vec_PtrShrink( vTokens, nSize );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
 {
     Mio_Library_t * pGenlib; 
@@ -581,6 +646,16 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         p->pNtkCur->pManFunc = pGenlib;
     }
 
+    // reorder the formal inputs to be in the same order as in the gate
+    if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate ) )
+    {
+        p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+        sprintf( p->sError, "Mismatch in the fanins of gate \"%s\".", (char*)vTokens->pArray[1] );
+        Io_ReadBlifPrintErrorMessage( p );
+        return 1;
+    }
+
+
     // remove the formal parameter names
     for ( i = 2; i < vTokens->nSize; i++ )
     {
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 95e7cd1d..2e2388d3 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -1828,6 +1828,7 @@ static char * Io_ReadBlifCleanName( char * pName )
 ***********************************************************************/
 static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
 {
+    extern int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate );
     Mio_Library_t * pGenlib; 
     Mio_Gate_t * pGate;
     Abc_Obj_t * pNode;
@@ -1868,6 +1869,13 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
         p->pNtk->pManFunc = pGenlib;
     }
 
+    // reorder the formal inputs to be in the same order as in the gate
+    if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate ) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Mismatch in the fanins of gate \"%s\".", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
+        return 0;
+    }
+
     // remove the formal parameter names
     for ( i = 2; i < vTokens->nSize; i++ )
     {
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 3aee2e44..738f217c 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -310,6 +310,130 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s )
     }
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Find the file name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_MainFileName( char * pFileName )
+{
+    static char Buffer[200];
+    char * pExtension;
+    assert( strlen(pFileName) < 190 );
+    pExtension = Extra_FileNameExtension( pFileName );
+    if ( pExtension == NULL )
+        sprintf( Buffer, "%s.opt", pFileName );
+    else
+    {
+        strncpy( Buffer, pFileName, pExtension-pFileName-1 );
+        sprintf( Buffer+(pExtension-pFileName-1), ".opt.%s", pExtension );
+    }
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [The main() procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int main_( int argc, char * argv[] )
+{
+    extern void Nwk_ManPrintStatsUpdate( void * p, void * pAig, void * pNtk,
+         int nRegInit, int nLutInit, int nLevInit, int Time );
+    char * pComs[20] = 
+    {
+/*00*/  "*r -am ",
+/*01*/  "*w -abc 1.aig",
+/*02*/  "*lcorr -nc",//; *ps",
+/*03*/  "*scorr -nc",//; *ps",
+/*04*/  "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps",
+/*05*/  "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", 
+/*06*/  "*w ",
+/*07*/  "*w -abc 2.aig",
+/*08*/  "miter -mc 1.aig 2.aig; sim -F 4 -W 4 -mv"
+    };
+    char Command[1000];
+    int i, nComs;
+    Abc_Frame_t * pAbc;
+    FILE * pFile;
+    int nRegInit, nLutInit, nLevInit;
+    int clkStart = clock();
+
+    // added to detect memory leaks:
+#if defined(_DEBUG) && defined(_MSC_VER) 
+    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
+#endif
+
+    // check that the file is present
+    if ( argc != 2 )
+    {
+        printf( "Expecting one command argument (file name).\n" );
+        return 0;
+    }
+    pFile = fopen( argv[1], "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", argv[1] );
+        return 0;
+    }
+    fclose( pFile );
+
+    // count the number of commands
+    for ( nComs = 0; nComs < 20; nComs++ )
+        if ( pComs[nComs] == NULL )
+            break;
+    // perform the commands
+    printf( "Reading design \"%s\"...\n", argv[1] );
+    pAbc = Abc_FrameGetGlobalFrame();
+    for ( i = 0; i < nComs; i++ )
+    {
+
+        if ( i == 0 )
+            sprintf( Command, "%s%s", pComs[i], argv[1] );
+        else if ( i == 6 )
+            sprintf( Command, "%s%s", pComs[i], Abc_MainFileName(argv[1]) );
+        else 
+            sprintf( Command, "%s", pComs[i] );
+        if ( Cmd_CommandExecute( pAbc, Command ) )
+        {
+            printf( "Internal command %d failed.\n", i );
+            return 0;
+        }
+        if ( i == 0 )
+        {
+            extern int Nwk_ManStatsRegs( void * p );
+            extern int Nwk_ManStatsLuts( void * pNtk );
+            extern int Nwk_ManStatsLevs( void * pNtk );
+            nRegInit = Nwk_ManStatsRegs( pAbc->pAbc8Ntl );
+            nLutInit = Nwk_ManStatsLuts( pAbc->pAbc8Nwk );
+            nLevInit = Nwk_ManStatsLevs( pAbc->pAbc8Nwk );
+        }
+        if ( i >= 1 && i <= 5 )
+        Nwk_ManPrintStatsUpdate( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk, 
+            nRegInit, nLutInit, nLevInit, clkStart );
+    }
+    Abc_Stop(); 
+    printf( "Writing optimized design \"%s\"...\n", Abc_MainFileName(argv[1]) );
+    ABC_PRT( "Total time", clock() - clkStart );
+    printf( "\n" );
+    return 0;  
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////