Version abc70817

9 files changed, 660 insertions, 126 deletions

diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 7d8d0f0f..00d8911b 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1086,6 +1086,89 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Removes POs with suppsize less than 2 and PIs without fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, k, m;
+
+    // filter POs
+    k = m = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsPo(pObj) )
+        {
+            // remove constant nodes and PI pointers
+            if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 0 )
+            {
+                Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) );
+                if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 && !Abc_ObjIsPi(Abc_ObjFanin0(pObj)) )
+                    Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 );
+                pNtk->vObjs->pArray[pObj->Id] = NULL;
+                pObj->Id = (1<<26)-1;
+                pNtk->nObjCounts[pObj->Type]--;
+                pNtk->nObjs--;
+                Abc_ObjRecycle( pObj );
+                continue;
+            }
+            // remove buffers/inverters of PIs
+            if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 1 )
+            {
+                if ( Abc_ObjIsPi(Abc_ObjFanin0(Abc_ObjFanin0(pObj))) )
+                {
+                    Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) );
+                    if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 )
+                        Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 );
+                    pNtk->vObjs->pArray[pObj->Id] = NULL;
+                    pObj->Id = (1<<26)-1;
+                    pNtk->nObjCounts[pObj->Type]--;
+                    pNtk->nObjs--;
+                    Abc_ObjRecycle( pObj );
+                    continue;
+                }
+            }
+            Vec_PtrWriteEntry( pNtk->vPos, m++, pObj );
+        }
+        Vec_PtrWriteEntry( pNtk->vCos, k++, pObj );
+    }
+    Vec_PtrShrink( pNtk->vPos, m );
+    Vec_PtrShrink( pNtk->vCos, k );
+
+    // filter PIs
+    k = m = 0;
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsPi(pObj) )
+        {
+            if ( Abc_ObjFanoutNum(pObj) == 0 )
+            {
+                pNtk->vObjs->pArray[pObj->Id] = NULL;
+                pObj->Id = (1<<26)-1;
+                pNtk->nObjCounts[pObj->Type]--;
+                pNtk->nObjs--;
+                Abc_ObjRecycle( pObj );
+                continue;
+            }
+            Vec_PtrWriteEntry( pNtk->vPis, m++, pObj );
+        }
+        Vec_PtrWriteEntry( pNtk->vCis, k++, pObj );
+    }
+    Vec_PtrShrink( pNtk->vPis, m );
+    Vec_PtrShrink( pNtk->vCis, k );
+
+    return Abc_NtkDup( pNtk );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3a916fdc..1b5e2361 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -93,6 +93,7 @@ static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCone           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandNode           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTopmost        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTrim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcGet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -171,6 +172,7 @@ static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** arg
 
 static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDSec           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -257,6 +259,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "topmost",       Abc_CommandTopmost,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "trim",          Abc_CommandTrim,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
@@ -335,6 +338,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "dsec",          Abc_CommandDSec,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
@@ -5134,6 +5138,84 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTrim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, nLevels;
+    extern Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nLevels = 10;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+/* 
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLevels = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevels < 0 ) 
+                goto usage;
+            break;
+*/
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for logic circuits.\n" );
+        return 0;
+    }
+
+    pNtkRes = Abc_NtkTrim( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "The command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: trim [-h]\n" );
+    fprintf( pErr, "\t         removes POs fed by PIs and constants, and PIs w/o fanout\n" );
+//    fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -6085,6 +6167,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
+    extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -6200,10 +6284,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Network should be strashed. Command has failed.\n" );
         return 1;
     }
-//    pNtkRes = Abc_NtkDar( pNtk );
-    pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
 */
-    pNtkRes = NULL;
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+//    pNtkRes = Abc_NtkDar( pNtk );
+    pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -6211,7 +6301,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-
     return 0;
 usage:
     fprintf( pErr, "usage: test [-h]\n" );
@@ -6627,6 +6716,11 @@ int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     Abc_NtkIvyCuts( pNtk, nInputs );
     return 0;
@@ -6690,6 +6784,11 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
@@ -6790,6 +6889,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
     pNtkRes = Abc_NtkDRewrite( pNtk, pPars );
     if ( pNtkRes == NULL )
     {
@@ -6904,6 +7008,11 @@ int Abc_CommandDRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
     if ( pPars->nLeafMax < 4 || pPars->nLeafMax > 15 )
     {
         fprintf( pErr, "This command only works for cut sizes 4 <= K <= 15.\n" );
@@ -6986,6 +7095,11 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
     pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose );
     if ( pNtkRes == NULL )
     {
@@ -7054,6 +7168,11 @@ int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
     pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, fVerbose );
     if ( pNtkRes == NULL )
     {
@@ -7124,6 +7243,11 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
@@ -7192,6 +7316,11 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose );
     if ( pNtkRes == NULL )
@@ -7273,6 +7402,11 @@ int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose );
     if ( pNtkRes == NULL )
@@ -7359,6 +7493,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
     if ( pNtkRes == NULL )
@@ -7453,6 +7592,11 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose );
     if ( pNtkRes == NULL )
@@ -7557,6 +7701,11 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "The number of leaves is infeasible.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose );
     if ( pNtkRes == NULL )
@@ -7728,6 +7877,11 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
 
     pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
@@ -10417,9 +10571,10 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nMaxIters;
     int fForward;
     int fBackward;
+    int fOneStep;
     int fVerbose;
     int Mode;
-    extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose );
+    extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10429,10 +10584,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     Mode      =  5;
     fForward  =  0;
     fBackward =  0;
+    fOneStep  =  0;
     fVerbose  =  0;
     nMaxIters = 15;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10453,6 +10609,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             fBackward ^= 1;
             break;
+        case 's':
+            fOneStep ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -10497,7 +10656,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         // convert the network into an SOP network
         pNtkRes = Abc_NtkToLogic( pNtk );
         // perform the retiming
-        Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose );
+        Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fOneStep, fVerbose );
         // replace the current network
         Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         return 0;
@@ -10517,7 +10676,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform the retiming
-    Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fVerbose );
+    Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fOneStep, fVerbose );
     return 0;
 
 usage:
@@ -10532,6 +10691,7 @@ usage:
     fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode );
     fprintf( pErr, "\t-f     : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" );
     fprintf( pErr, "\t-b     : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" );
+    fprintf( pErr, "\t-s     : enables retiming one step only in mode 4 [default = %s]\n", fOneStep? "yes": "no" );
     fprintf( pErr, "\t-v     : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -10816,21 +10976,23 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fExdc;
     int fImp;
     int fRewrite;
+    int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFramesK = 1;
-    fExdc    = 1;
-    fImp     = 0;
-    fRewrite = 0;
-    fVerbose = 0;
+    nFramesK   = 1;
+    fExdc      = 1;
+    fImp       = 0;
+    fRewrite   = 0;
+    fLatchCorr = 0;
+    fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10854,6 +11016,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fRewrite ^= 1;
             break;
+        case 'l':
+            fLatchCorr ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -10883,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose );
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -10894,11 +11059,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
 //    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
+    fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -10919,11 +11085,12 @@ usage:
 int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pTemp;
     int c;
     int fLatchSweep;
     int fAutoSweep;
     int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10964,14 +11131,31 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    Abc_NtkCleanupSeq( pNtk, fLatchSweep, fAutoSweep, fVerbose );
+
+    // get the new network
+    pNtkRes = Abc_NtkDup( pNtk ); 
+    Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose );
+    if ( fLatchSweep )
+    {
+        pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 );
+        Abc_NtkDelete( pTemp );
+        pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose );
+        Abc_NtkDelete( pTemp );
+    }
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential cleanup has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
     fprintf( pErr, "usage: scleanup [-lavh]\n" );
     fprintf( pErr, "\t         performs sequential cleanup\n" );
     fprintf( pErr, "\t         - removes nodes/latches that do not feed into POs\n" );
-    fprintf( pErr, "\t         - removes and shared latches driven by constants\n" );
+    fprintf( pErr, "\t         - removes stuck-at and identical latches (latch sweep)\n" );
     fprintf( pErr, "\t         - replaces autonomous logic by free PI variables\n" );
     fprintf( pErr, "\t           (the latter may change sequential behaviour)\n" );
     fprintf( pErr, "\t-l     : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
@@ -11402,17 +11586,17 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
-    if ( Abc_NtkLatchNum(pNtk) == 0 )
-    {
-        printf( "The network has no latches. Used combinational command \"cec\".\n" );
-        return 0;
-    }
-
     pArgvNew = argv + globalUtilOptind;
     nArgcNew = argc - globalUtilOptind;
     if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
         return 1;
 
+    if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
+    {
+        printf( "The network has no latches. Used combinational command \"cec\".\n" );
+        return 0;
+    }
+
     // perform equivalence checking
     if ( fRetime )
         Abc_NtkSecRetime( pNtk1, pNtk2 );
@@ -11454,6 +11638,97 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
+    int fDelete1, fDelete2;
+    char ** pArgvNew;
+    int nArgcNew;
+    int c;
+    int fVerbose;
+    int fVeryVerbose;
+    int nFrames;
+
+    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames      = 0; // if 0, iterates through frames
+    fVerbose     = 1;
+    fVeryVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames <= 0 ) 
+                goto usage;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+        return 1;
+
+    if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
+    {
+        printf( "The network has no latches. Used combinational command \"cec\".\n" );
+        return 0;
+    }
+
+    // perform verification
+    Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose );
+
+    if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+    if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" );
+    fprintf( pErr, "\t         performs inductive sequential equivalence checking\n" );
+    fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
+    fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
+    fprintf( pErr, "\t         if no files are given, uses the current network and its spec\n");
+    fprintf( pErr, "\t         if one file is given, uses the current network and the file\n");
+    return 1;
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ca80fec8..4013b98d 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -23,6 +23,7 @@
 #include "dar.h"
 #include "cnf.h"
 #include "fra.h"
+#include "fraig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -79,11 +80,13 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
             if ( Abc_LatchIsInit1(pObj) )
                 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
     // perform the conversion of the internal nodes (assumes DFS ordering)
+//    pMan->fAddStrash = 1;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
 //        printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
     }
+    pMan->fAddStrash = 0;
     // create the POs
     Abc_NtkForEachCo( pNtk, pObj, i )
         Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
@@ -121,6 +124,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Abc_Ntk_t * pNtkNew;
     Aig_Obj_t * pObj;
     int i;
+    assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
@@ -147,6 +151,59 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
+  Description [This procedure should be called after seq sweeping, 
+  which changes the number of registers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew;
+    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
+    int i;
+//    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Aig_ManForEachPiSeq( pMan, pObj, i )
+        pObj->pData = Abc_NtkCi(pNtkNew, i);
+    // create as many latches as there are registers in the manager
+    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
+    {
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
+        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pObjLi->pData );
+        Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+        Abc_LatchSetInit0( pObjNew );
+    }
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    // rebuild the AIG
+    vNodes = Aig_ManDfs( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+        else
+            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Aig_ManForEachPo( pMan, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
   Description []
                
   SideEffects []
@@ -367,55 +424,23 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
 {
-    Abc_Ntk_t * pNtkAig;
-    Aig_Man_t * pMan;//, * pTemp;
-//    int * pArray;
+    Abc_Ntk_t * pNtkAig = NULL;
+    Aig_Man_t * pMan;
+    extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim );
 
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
-    if ( !Aig_ManCheck( pMan ) )
-    {
-        printf( "Abc_NtkDar: AIG check has failed.\n" );
-        Aig_ManStop( pMan );
-        return NULL;
-    }
-    // perform balance
-    Aig_ManPrintStats( pMan );
-/*
-    pArray = Abc_NtkGetLatchValues(pNtk);
-    Aig_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
-    free( pArray );
-*/
 
-//    Aig_ManDumpBlif( pMan, "aig_temp.blif" );
-//    pMan->pPars = Dar_ManDefaultRwrPars();
-    Dar_ManRewrite( pMan, NULL );
-    Aig_ManPrintStats( pMan );
-//    Dar_ManComputeCuts( pMan );
-
-/*
-{
-extern Aig_Cnf_t * Aig_ManDeriveCnf( Aig_Man_t * p );
-extern void Aig_CnfFree( Aig_Cnf_t * pCnf );
-Aig_Cnf_t * pCnf;
-pCnf = Aig_ManDeriveCnf( pMan );
-Aig_CnfFree( pCnf );
-}
-*/
-
-    // convert from the AIG manager
-    if ( Aig_ManLatchNum(pMan) )
-        pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
-    else
-        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
-    if ( pNtkAig == NULL )
-        return NULL;
+    // perform computation
+//    Fra_ManPartitionTest( pMan, 4 );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
+
     // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkAig ) )
+    if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
     {
         printf( "Abc_NtkDar: The network check has failed.\n" );
         Abc_NtkDelete( pNtkAig );
@@ -867,23 +892,146 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose )
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
         return NULL;
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
+//    pMan->nRegs = Abc_NtkLatchNum(pNtk);
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
-    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    else
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose )
+{
+    Fraig_Params_t Params;
+    Aig_Man_t * pMan;
+    Abc_Ntk_t * pMiter, * pTemp;
+    int RetValue;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return 0;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 0 )
+    {
+        extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
+        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
+        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
+        return 0;
+    }
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return 1;
+    }
+
+    // preprocess the miter by fraiging it
+    // (note that for each functional class, fraiging leaves one representative;
+    // so fraiging does not reduce the number of functions represented by nodes
+    Fraig_ParamsSetDefault( &Params );
+    pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
+    Abc_NtkDelete( pTemp );
+
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pMiter, 1 );
+    Abc_NtkDelete( pMiter );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+
+    // perform verification
+    RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose );
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Aig_ManReduceLaches( pMan, fVerbose );
+    pMan = Aig_ManConstReduce( pMan, fVerbose );
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose );
+    Aig_ManStop( pTemp );
+
+//    pMan = Aig_ManReduceLaches( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1 );
+
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index a33b9875..5dc63750 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -98,6 +98,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in
     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
     Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
+    Abc_AigCleanup(pNtkMiter->pManFunc);
 
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkMiter ) )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index ad8eec6a..4c061637 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -322,7 +322,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", 
         Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
     fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 );
-    fprintf( pFile, "Self-feed latches = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+    fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 63ba4843..67ecaae0 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
  
 static void  Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
-static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
+extern void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index d17ab1dd..c05823da 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -139,7 +139,11 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
             Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
         fprintf( stdout, " : " );
         Abc_NtkForEachLatch( pNtk, pObj, i )
+        {
+//            if ( Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) != XVSX )
+//                printf( " %s=", Abc_ObjName(pObj) );
             Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) );
+        }
         fprintf( stdout, " : " );
         Abc_NtkForEachPo( pNtk, pObj, i )
             Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 23b5b350..be80dc82 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -121,8 +121,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         Abc_ObjAddFanin( pNode1, pObj );
         Vec_PtrPush( vNodes, pNode1 );
         // assign names to latch and its input
-        Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
-
+//        Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
 //        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
     } 
     
@@ -142,7 +141,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         uLit = ((i + 1 + nInputs + nLatches) << 1);
         uLit1 = uLit  - Io_ReadAigerDecode( &pCur );
         uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
-        assert( uLit1 > uLit0 );
+//        assert( uLit1 > uLit0 );
         pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
         pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
         assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
@@ -171,66 +170,84 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
         Abc_ObjAddFanin( pObj, pNode0 );
     }
-
+ 
     // read the names if present
     pCur = pSymbols;
-    while ( pCur < pContents + nFileSize && *pCur != 'c' )
+    if ( *pCur != 'c' )
     {
-        // get the terminal type
-        pType = pCur;
-        if ( *pCur == 'i' )
-            vTerms = pNtkNew->vPis;
-        else if ( *pCur == 'l' )
-            vTerms = pNtkNew->vBoxes;
-        else if ( *pCur == 'o' )
-            vTerms = pNtkNew->vPos;
-        else
+        int Counter = 0;
+        while ( pCur < pContents + nFileSize && *pCur != 'c' )
+        {
+            // get the terminal type
+            pType = pCur;
+            if ( *pCur == 'i' )
+                vTerms = pNtkNew->vPis;
+            else if ( *pCur == 'l' )
+                vTerms = pNtkNew->vBoxes;
+            else if ( *pCur == 'o' )
+                vTerms = pNtkNew->vPos;
+            else
+            {
+                fprintf( stdout, "Wrong terminal type.\n" );
+                return NULL;
+            }
+            // get the terminal number
+            iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
+            // get the node
+            if ( iTerm >= Vec_PtrSize(vTerms) )
+            {
+                fprintf( stdout, "The number of terminal is out of bound.\n" );
+                return NULL;
+            }
+            pObj = Vec_PtrEntry( vTerms, iTerm );
+            if ( *pType == 'l' )
+                pObj = Abc_ObjFanout0(pObj);
+            // assign the name
+            pName = pCur;          while ( *pCur++ != '\n' );
+            // assign this name 
+            *(pCur-1) = 0;
+            Abc_ObjAssignName( pObj, pName, NULL );
+            if ( *pType == 'l' )
+            {
+                Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
+                Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
+            }
+            // mark the node as named
+            pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+        } 
+
+        // assign the remaining names
+        Abc_NtkForEachPi( pNtkNew, pObj, i )
         {
-            fprintf( stdout, "Wrong terminal type.\n" );
-            return NULL;
+            if ( pObj->pCopy ) continue;
+            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+            Counter++;
         }
-        // get the terminal number
-        iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
-        // get the node
-        if ( iTerm >= Vec_PtrSize(vTerms) )
+        Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
         {
-            fprintf( stdout, "The number of terminal is out of bound.\n" );
-            return NULL;
+            if ( pObj->pCopy ) continue;
+            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+            Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
+            Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
+            Counter++;
         }
-        pObj = Vec_PtrEntry( vTerms, iTerm );
-        if ( *pType == 'l' )
-            pObj = Abc_ObjFanout0(pObj);
-        // assign the name
-        pName = pCur;          while ( *pCur++ != '\n' );
-        // assign this name
-        *(pCur-1) = 0;
-        Abc_ObjAssignName( pObj, pName, NULL );
-        if ( *pType == 'l' )
-            Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
-        // mark the node as named
-        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
-    } 
-    // skipping the comments
-    free( pContents );
-    Vec_PtrFree( vNodes );
-
-    // assign the remaining names
-    Abc_NtkForEachPi( pNtkNew, pObj, i )
-    {
-        if ( pObj->pCopy ) continue;
-        Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
-    }
-    Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
-    {
-        if ( pObj->pCopy ) continue;
-        Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
-        Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL );
+        Abc_NtkForEachPo( pNtkNew, pObj, i )
+        {
+            if ( pObj->pCopy ) continue;
+            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+            Counter++;
+        }
+        if ( Counter )
+            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
     }
-    Abc_NtkForEachPo( pNtkNew, pObj, i )
+    else
     {
-        if ( pObj->pCopy ) continue;
-        Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+//        printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
+        Abc_NtkShortNames( pNtkNew );
     }
+    // skipping the comments
+    free( pContents );
+    Vec_PtrFree( vNodes );
 
     // remove the extra nodes
     Abc_AigCleanup( pNtkNew->pManFunc );
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 7c9da184..958e3d96 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -163,6 +163,12 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
         fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( !Abc_LatchIsInit0(pObj) )
+        {
+            fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
+            return;
+        }
 
     // set the node numbers to be used in the output file
     nNodes = 0;