Version abc80430

6 files changed, 506 insertions, 26 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 492fefae..e7896cb1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -98,6 +98,7 @@ static int Abc_CommandBidec          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandOrder          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReach          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 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 );
@@ -349,6 +350,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
+    Cmd_CommandAdd( pAbc, "Various",      "reach",         Abc_CommandReach,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "topmost",       Abc_CommandTopmost,          1 );
@@ -5605,6 +5607,116 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int nBddMax;
+    int nIterMax;
+    int fPartition;
+    int fReorder;
+    int fVerbose;
+    int c;
+    extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nBddMax    = 50000;
+    nIterMax   = 1000;
+    fPartition = 1;
+    fReorder   = 1;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBddMax < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIterMax < 0 ) 
+                goto usage;
+            break;
+        case 'p':
+            fPartition ^= 1;
+            break;
+        case 'r':
+            fReorder ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "The current network has no latches.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Reachability analysis works only for AIGs (run \"strash\").\n" );
+        return 1;
+    }
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( stdout, "The sequential miter has more than one output (run \"orpos\").\n" );
+        return 1;
+    }
+    Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
+    fprintf( pErr, "\t         verifies sequential miter using BDD-based reachability\n" );
+    fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
+    fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
+    fprintf( pErr, "\t-p     : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );  
+    fprintf( pErr, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -11925,10 +12037,11 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nStepsMax;
     int fFastAlgo;
     int fVerbose;
-    int c;
+    int c, nMaxIters;
     extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11940,13 +12053,25 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     fBackwardOnly = 0;
     fInitial = 1;
     nStepsMax = 100000;
-    fFastAlgo = 1;
+    fFastAlgo = 0;
+    nMaxIters = 20;
     fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Smfbiavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NSmfbiavh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nMaxIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMaxIters < 0 ) 
+                goto usage;
+            break;
         case 'S':
             if ( globalUtilOptind >= argc )
             {
@@ -12003,11 +12128,12 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform the retiming
     if ( fMinArea )
-        pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+        pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
     else if ( fFastAlgo )
         pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
     else
-        pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+//        pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+        pNtkRes = Abc_NtkDarRetimeMostFwd( pNtk, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Retiming has failed.\n" );
@@ -12018,12 +12144,13 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dretime [-S num] [-mfbiavh]\n" );
-    fprintf( pErr, "\t         new implementation of min-area retiming\n" );
-    fprintf( pErr, "\t-m     : toggle min-area and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
+    fprintf( pErr, "usage: dretime [-NS num] [-mfbiavh]\n" );
+    fprintf( pErr, "\t         new implementation of min-area (or most-forward) retiming\n" );
+    fprintf( pErr, "\t-m     : toggle min-area retiming and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
     fprintf( pErr, "\t-f     : enables forward-only retiming [default = %s]\n", fForwardOnly? "yes": "no" );
     fprintf( pErr, "\t-b     : enables backward-only retiming [default = %s]\n", fBackwardOnly? "yes": "no" );
     fprintf( pErr, "\t-i     : enables init state computation [default = %s]\n", fInitial? "yes": "no" );
+    fprintf( pErr, "\t-N num : the max number of one-frame iterations to perform [default = %d]\n", nMaxIters );
     fprintf( pErr, "\t-S num : the max number of forward retiming steps to perform [default = %d]\n", nStepsMax );
     fprintf( pErr, "\t-a     : enables a fast most-forward algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
     fprintf( pErr, "\t-v     : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 20557fb3..4b1a37c2 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1409,7 +1409,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
+    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
@@ -1431,24 +1431,24 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 {
-    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
+//    Aig_ManReduceLachesCount( pMan );
     if ( pMan->vFlopNums )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
-    pMan = Saig_ManRetimeMinArea( pTemp = pMan, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
     Aig_ManStop( pTemp );
 
+//    pMan = Aig_ManReduceLaches( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1 );
+
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;
@@ -1465,8 +1465,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBa
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
 {
+    extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );
+
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
@@ -1477,7 +1479,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+
+    pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
@@ -1499,6 +1504,40 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+{
+    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+
+    pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+    Aig_ManStop( pTemp );
+
+    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     []
+
+***********************************************************************/
 void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
 /*
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 171cbf0a..78e7cf6b 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -201,7 +201,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
-    int i;//, nDupGates;
+    int i, nDupGates;
     // create the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
     // make the mapper point to the new network
@@ -229,9 +229,9 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
         Abc_NtkDeleteObj( pNodeNew );
     // decouple the PO driver nodes to reduce the number of levels
-//    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-//    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
-//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index cf6f88ae..94c7dda8 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -186,7 +186,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
     Vec_Int_t * vCover;
-    int i;//, nDupGates;
+    int i, nDupGates;
     // create the new network
     if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
@@ -223,9 +223,9 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     if ( pIfMan->pPars->fUseBdds )
         Abc_NtkBddReorder( pNtkNew, 0 );
     // decouple the PO driver nodes to reduce the number of levels
-//    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-//    if ( nDupGates && If_ManReadVerbose(pIfMan) )
-//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( nDupGates && pIfMan->pPars->fVerbose )
+        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
new file mode 100644
index 00000000..42494b5c
--- /dev/null
+++ b/src/base/abci/abcReach.c
@@ -0,0 +1,313 @@
+/**CFile****************************************************************
+
+  FileName    [abcReach.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Performs reachability analysis.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the initial state and sets up the variable map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    DdNode ** pbVarsX, ** pbVarsY;
+    DdNode * bTemp, * bProd, * bVar;
+    Abc_Obj_t * pLatch;
+    int i;
+
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsX = ALLOC( DdNode *, dd->size );
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    bProd = b1;         Cudd_Ref( bProd );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
+        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+        // get the initial value of the latch
+        bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
+    FREE( pbVarsX );
+    FREE( pbVarsY );
+
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose )
+{
+    DdNode ** pbParts;
+    DdNode * bVar;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // extand the BDD manager to represent NS variables
+    assert( dd->size == Abc_NtkCiNum(pNtk) );
+    Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
+
+    // enable reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    else
+        Cudd_AutodynDisable( dd );
+
+    // compute the transition relation
+    pbParts = ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+    {
+        bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
+        pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
+    }
+    // free the global BDDs
+    Abc_NtkFreeGlobalBdds( pNtk, 0 );
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
+    }
+    return pbParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of unreachable states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    int fInternalReorder = 0;
+    Extra_ImageTree_t * pTree;
+    Extra_ImageTree2_t * pTree2;
+    DdNode * bReached, * bCubeCs;
+    DdNode * bCurrent, * bNext, * bTemp;
+    DdNode ** pbVarsY;
+    Abc_Obj_t * pLatch;
+    int i, nIters, nBddSize;
+    int nThreshold = 10000;
+
+    // collect the NS variables
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+
+    // start the image computation
+    bCubeCs  = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
+    if ( fPartition )
+        pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
+    else
+        pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
+    free( pbVarsY );
+    Cudd_RecursiveDeref( dd, bCubeCs );
+
+    // perform reachability analisys
+    bCurrent = bInitial;   Cudd_Ref( bCurrent );
+    bReached = bInitial;   Cudd_Ref( bReached );
+    for ( nIters = 1; nIters <= nIterMax; nIters++ )
+    {
+        // compute the next states
+        if ( fPartition )
+            bNext = Extra_bddImageCompute( pTree, bCurrent );           
+        else
+            bNext = Extra_bddImageCompute2( pTree2, bCurrent );         
+        Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bCurrent );
+        // remap these states into the current state vars
+        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                    Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // check if there are any new states
+        if ( Cudd_bddLeq( dd, bNext, bReached ) )
+            break;
+        // check the BDD size
+        nBddSize = Cudd_DagSize(bNext);
+        if ( nBddSize > nBddMax )
+            break;
+        // check the result
+        if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) )
+        {
+            printf( "The miter is proved REACHABLE in %d iterations.  ", nIters );
+            Cudd_RecursiveDeref( dd, bReached );
+            bReached = NULL;
+            break;
+        }
+        // get the new states
+        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
+        // minimize the new states with the reached states
+//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( dd, bTemp );
+        // add to the reached states
+        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );           Cudd_Ref( bReached );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bNext );
+        if ( fVerbose )
+            fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize );
+        if ( fInternalReorder && fReorder && nBddSize > nThreshold )
+        {
+            if ( fVerbose )
+                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
+            Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+            Cudd_AutodynDisable( dd );
+            if ( fVerbose )
+                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
+            nThreshold *= 2;
+        }
+        if ( fVerbose )
+            fprintf( stdout, "\r" );
+    }
+    Cudd_RecursiveDeref( dd, bNext );
+    // undo the image tree
+    if ( fPartition )
+        Extra_bddImageTreeDelete( pTree );
+    else
+        Extra_bddImageTreeDelete2( pTree2 );
+    if ( bReached == NULL )
+        return NULL;
+    // report the stats
+    if ( fVerbose )
+    {
+        double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
+        if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+            fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters );
+        else
+            fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
+        fflush( stdout );
+    }
+//PRB( dd, bReached );
+    Cudd_Deref( bReached );
+    if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+         printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
+    printf( "The miter is proved unreachable in %d iteration.  ", nIters );
+    return bReached;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs reachability to see if any .]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    DdManager * dd;
+    DdNode ** pbParts;
+    DdNode * bOutput, * bReached, * bInitial;
+    int i, clk = clock();
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkPoNum(pNtk) == 1 );
+    assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
+
+    // compute the global BDDs of the latches
+    dd = Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );    
+    if ( dd == NULL )
+    {
+        printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
+        return;
+    }
+    if ( fVerbose )
+        printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // save the output BDD
+    bOutput = Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
+
+    // create partitions
+    pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );
+
+    // create the initial state and the variable map
+    bInitial  = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose );  Cudd_Ref( bInitial );
+
+    // check the result
+    if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) )
+        printf( "The miter is proved REACHABLE in the initial state.  " );
+    else
+    {
+        // compute the reachable states
+        bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); 
+        if ( bReached != NULL )
+        {
+            Cudd_Ref( bReached );
+            Cudd_RecursiveDeref( dd, bReached );
+        }
+    }
+
+    // cleanup
+    Cudd_RecursiveDeref( dd, bOutput );
+    Cudd_RecursiveDeref( dd, bInitial );
+    for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
+        Cudd_RecursiveDeref( dd, pbParts[i] );
+    free( pbParts );
+    Extra_StopManager( dd );
+
+    // report the runtime
+    PRT( "Time", clock() - clk );
+    fflush( stdout );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 716f1618..ca2f2501 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -39,6 +39,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcQuant.c \
     src/base/abci/abcRec.c \
     src/base/abci/abcReconv.c \
+    src/base/abci/abcReach.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \
     src/base/abci/abcReorder.c \