Version abc70217

17 files changed, 1071 insertions, 91 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index d19fbcef..bbe6b078 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -393,6 +393,8 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Ab
 static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );  }
 static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );    }
 static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) );    }
 
 // checking the AIG node types
 static inline bool        Abc_AigNodeIsConst( Abc_Obj_t * pNode )    { assert(Abc_NtkIsStrash(Abc_ObjRegular(pNode)->pNtk));  return Abc_ObjRegular(pNode)->Type == ABC_OBJ_CONST1;       }
@@ -527,11 +529,9 @@ extern void               Abc_AigPrintNode( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
 extern void               Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
 extern void               Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_AigUpdateStart( Abc_Aig_t * pMan );
+extern Vec_Ptr_t *        Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets );
 extern void               Abc_AigUpdateStop( Abc_Aig_t * pMan );
 extern void               Abc_AigUpdateReset( Abc_Aig_t * pMan );
-extern void               Abc_AigUpdateAdd( Abc_Aig_t * pMan, Abc_Obj_t * pObj );
-extern Vec_Ptr_t *        Abc_AigUpdateRead( Abc_Aig_t * pMan );
 /*=== abcAttach.c ==========================================================*/
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 /*=== abcBalance.c ==========================================================*/
@@ -555,6 +555,7 @@ extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
@@ -623,7 +624,7 @@ extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 extern void               Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
-extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
+extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
 extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
@@ -831,6 +832,7 @@ extern int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkCleanData( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index c92f3b57..35a37e1e 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -59,7 +59,8 @@ struct Abc_Aig_t_
     Vec_Ptr_t *       vStackReplaceNew;  // the nodes to be used for replacement
     Vec_Vec_t *       vLevels;           // the nodes to be updated
     Vec_Vec_t *       vLevelsR;          // the nodes to be updated
-    Vec_Ptr_t *       vUpdates;          // the added and removed nodes
+    Vec_Ptr_t *       vAddedCells;       // the added nodes
+    Vec_Ptr_t *       vUpdatedNets;      // the nodes whose fanouts have changed
 
     int               nStrash0;
     int               nStrash1;
@@ -163,8 +164,10 @@ void Abc_AigFree( Abc_Aig_t * pMan )
     assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
     assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
     // free the table
-    if ( pMan->vUpdates )
-        Vec_PtrFree( pMan->vUpdates );
+    if ( pMan->vAddedCells )
+        Vec_PtrFree( pMan->vAddedCells );
+    if ( pMan->vUpdatedNets )
+        Vec_PtrFree( pMan->vUpdatedNets );
     Vec_VecFree( pMan->vLevels );
     Vec_VecFree( pMan->vLevelsR );
     Vec_PtrFree( pMan->vStackReplaceOld );
@@ -326,8 +329,8 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
     pAnd->pCopy = NULL;
     // add the node to the list of updated nodes
-    if ( pMan->vUpdates )
-        Vec_PtrPush( pMan->vUpdates, pAnd );
+    if ( pMan->vAddedCells )
+        Vec_PtrPush( pMan->vAddedCells, pAnd );
     return pAnd;
 }
 
@@ -366,8 +369,8 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
     pAnd->pCopy = NULL;
     // add the node to the list of updated nodes
-    if ( pMan->vUpdates )
-        Vec_PtrPush( pMan->vUpdates, pAnd );
+//    if ( pMan->vAddedCells )
+//        Vec_PtrPush( pMan->vAddedCells, pAnd );
     return pAnd;
 }
 
@@ -548,9 +551,6 @@ void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
     // delete the cuts if defined
     if ( pThis->pNtk->pManCut )
         Abc_NodeFreeCuts( pThis->pNtk->pManCut, pThis );
-    // add the node to the list of updated nodes
-    if ( pMan->vUpdates )
-        Vec_PtrPush( pMan->vUpdates, pThis );
 }
 
 /**Function*************************************************************
@@ -961,6 +961,13 @@ void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     pNode0 = Abc_ObjFanin0( pNode );
     pNode1 = Abc_ObjFanin1( pNode );
 
+    // add the node to the list of updated nodes
+    if ( pMan->vUpdatedNets )
+    {
+        Vec_PtrPushUnique( pMan->vUpdatedNets, pNode0 );
+        Vec_PtrPushUnique( pMan->vUpdatedNets, pNode1 );
+    }
+
     // remove the node from the table
     Abc_AigAndDelete( pMan, pNode );
     // if the node is in the level structure, remove it
@@ -1368,10 +1375,13 @@ void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan )
+Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets )
 {
-    assert( pMan->vUpdates == NULL );
-    return pMan->vUpdates = Vec_PtrAlloc( 1000 );
+    assert( pMan->vAddedCells == NULL );
+    pMan->vAddedCells  = Vec_PtrAlloc( 1000 );
+    pMan->vUpdatedNets = Vec_PtrAlloc( 1000 );
+    *pvUpdatedNets = pMan->vUpdatedNets;
+    return pMan->vAddedCells;
 }
 
 /**Function*************************************************************
@@ -1387,8 +1397,11 @@ Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan )
 ***********************************************************************/
 void Abc_AigUpdateStop( Abc_Aig_t * pMan )
 {
-    assert( pMan->vUpdates != NULL );
-    Vec_PtrFree( pMan->vUpdates );
+    assert( pMan->vAddedCells != NULL );
+    Vec_PtrFree( pMan->vAddedCells );
+    Vec_PtrFree( pMan->vUpdatedNets );
+    pMan->vAddedCells = NULL;
+    pMan->vUpdatedNets = NULL;
 }
 
 /**Function*************************************************************
@@ -1404,41 +1417,9 @@ void Abc_AigUpdateStop( Abc_Aig_t * pMan )
 ***********************************************************************/
 void Abc_AigUpdateReset( Abc_Aig_t * pMan )
 {
-    assert( pMan->vUpdates != NULL );
-    Vec_PtrClear( pMan->vUpdates );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Add a new update.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_AigUpdateAdd( Abc_Aig_t * pMan, Abc_Obj_t * pObj )
-{
-    if ( pMan->vUpdates )
-        Vec_PtrPush( pMan->vUpdates, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read the updates array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Abc_AigUpdateRead( Abc_Aig_t * pMan )
-{
-    return pMan->vUpdates;
+    assert( pMan->vAddedCells != NULL );
+    Vec_PtrClear( pMan->vAddedCells );
+    Vec_PtrClear( pMan->vUpdatedNets );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 48ffa489..da4617ca 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -199,6 +199,76 @@ Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
     return vNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfsReverseNodes_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( !Abc_ObjIsNet(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // skip the CI
+    if ( Abc_ObjIsCo(pNode) )
+        return;
+    assert( Abc_ObjIsNode( pNode ) );
+    // visit the transitive fanin of the node
+    pNode = Abc_ObjFanout0Ntk(pNode);
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        Abc_NtkDfsReverseNodes_rec( pFanout, vNodes );
+    // add the node after the fanins have been added
+//    Vec_PtrPush( vNodes, pNode );
+    Vec_PtrFillExtra( vNodes, pNode->Level + 1, NULL );
+    pNode->pCopy = Vec_PtrEntry( vNodes, pNode->Level );
+    Vec_PtrWriteEntry( vNodes, pNode->Level, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the levelized array of TFO nodes.]
+
+  Description [Collects the levelized array of internal nodes, leaving out CIs/COs.
+  However it marks both CIs and COs with the current TravId.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrStart( Abc_AigLevel(pNtk) + 1 );
+    for ( i = 0; i < nNodes; i++ )
+    {
+        pObj = ppNodes[i];
+        assert( Abc_ObjIsCi(pObj) );
+        Abc_NodeSetTravIdCurrent( pObj );
+        pObj = Abc_ObjFanout0Ntk(pObj);
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            Abc_NtkDfsReverseNodes_rec( pFanout, vNodes );
+    }
+    return vNodes;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index f5c5536a..9a40fce9 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -486,6 +486,25 @@ void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanData( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pData = NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of nodes having non-trivial copies.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e7f8c8ea..ae00ce5c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -67,6 +67,7 @@ static int Abc_CommandRefactor       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandRestructure    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandResubstitute   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRr             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCascade        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandComb           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -96,6 +97,10 @@ static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDouble         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandQuaVar         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandQuaRel         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandQuaReach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -203,6 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Synthesis",    "restructure",   Abc_CommandRestructure,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "rr",            Abc_CommandRr,               1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "cascade",       Abc_CommandCascade,          1 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "comb",          Abc_CommandComb,             1 );
@@ -232,6 +238,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
+    Cmd_CommandAdd( pAbc, "Various",      "qvar",          Abc_CommandQuaVar,           1 );
+    Cmd_CommandAdd( pAbc, "Various",      "qrel",          Abc_CommandQuaRel,           1 );
+    Cmd_CommandAdd( pAbc, "Various",      "qreach",        Abc_CommandQuaReach,         1 );
+
     Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "icut",          Abc_CommandICut,             0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
@@ -3234,6 +3244,109 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandCascade( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, nLutSize;
+    int fCheck;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nLutSize = 12;
+    fCheck   = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kcvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        case 'c':
+            fCheck ^= 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_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Can only collapse a logic network or an AIG.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( Abc_NtkIsStrash(pNtk) )
+        pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose );
+    else
+    {
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose );
+        Abc_NtkDelete( pNtk );
+    }
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Cascade synthesis has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: cascade [-K <num>] [-cvh]\n" );
+    fprintf( pErr, "\t         performs LUT cascade synthesis for the current network\n" );
+    fprintf( pErr, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize );
+    fprintf( pErr, "\t-c     : check equivalence after synthesis [default = %s]\n", fCheck? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t         \n");
+    fprintf( pErr, "  A lookup-table cascade is a programmable architecture developed by\n");
+    fprintf( pErr, "  Professor Tsutomu Sasao (sasao@cse.kyutech.ac.jp) at Kyushu Institute\n");
+    fprintf( pErr, "  of Technology. This work received Takeda Techno-Entrepreneurship Award:\n");
+    fprintf( pErr, "  http://www.lsi-cad.com/sasao/photo/takeda.html\n");
+    fprintf( pErr, "\t         \n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -5536,6 +5649,293 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, iVar, fVerbose, RetValue;
+    extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    iVar = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iVar = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iVar < 0 ) 
+                goto usage;
+            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_NtkGetChoiceNum( pNtk ) )
+    {
+        fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" );
+        return 1;
+    }
+
+    // get the strashed network
+    pNtkRes = Abc_NtkStrash( pNtk, 0, 1 );
+    RetValue = Abc_NtkQuantify( pNtkRes, iVar, fVerbose );
+    // clean temporary storage for the cofactors
+    Abc_NtkCleanData( pNtkRes );
+    Abc_AigCleanup( pNtkRes->pManFunc );
+    // check the result 
+    if ( !RetValue )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: qvar [-I num] [-vh]\n" );
+    fprintf( pErr, "\t         quantifies one variable using the AIG\n" );
+    fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar );
+    fprintf( pErr, "\t-v     : toggle printing 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_CommandQuaRel( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, iVar, fInputs, fVerbose;
+    extern Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    iVar = 0;
+    fInputs = 1;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Iqvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iVar = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iVar < 0 ) 
+                goto usage;
+            break;
+        case 'q':
+            fInputs ^= 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_NtkGetChoiceNum( pNtk ) )
+    {
+        fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "This command works only for sequential circuits.\n" );
+        return 1;
+    }
+
+    // get the strashed network
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose );
+        Abc_NtkDelete( pNtk );
+    }
+    else
+        pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose );
+    // check if the result is available
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: qrel [-qvh]\n" );
+    fprintf( pErr, "\t         computes transition relation of the sequential network\n" );
+//    fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar );
+    fprintf( pErr, "\t-q     : perform quantification of inputs [default = %s]\n", fInputs? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing 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_CommandQuaReach( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, nIters, fVerbose;
+    extern Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtk, int nIters, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nIters   = 256;
+    fVerbose =   0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIters < 0 ) 
+                goto usage;
+            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_NtkGetChoiceNum( pNtk ) )
+    {
+        fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "This command works only for combinational transition relations.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
+    if ( Abc_NtkPoNum(pNtk) > 1 )
+    {
+        fprintf( pErr, "The transition relation should have one output.\n" );
+        return 1;
+    }
+    if ( Abc_NtkPiNum(pNtk) % 2 != 0 )
+    {
+        fprintf( pErr, "The transition relation should have an even number of inputs.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkReachability( pNtk, nIters, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: qreach [-I num] [-vh]\n" );
+    fprintf( pErr, "\t         computes unreachable states using AIG-based quantification\n" );
+    fprintf( pErr, "\t         assumes that the current network is a transition relation\n" );
+    fprintf( pErr, "\t         assumes that the initial state is composed of all zeros\n" );
+    fprintf( pErr, "\t-I num : the number of image computations to perform [default = %d]\n", nIters );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index 3b307ac2..40212c17 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -74,7 +74,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
 
     // print the size of the BDDs
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
 
     // allocate additional variables
     for ( i = 0; i < nInputs; i++ )
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
new file mode 100644
index 00000000..4ed7a774
--- /dev/null
+++ b/src/base/abci/abcCas.c
@@ -0,0 +1,111 @@
+/**CFile****************************************************************
+
+  FileName    [abcCas.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Decomposition of shared BDDs into LUT cascade.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+/* 
+    This LUT cascade synthesis algorithm is described in the paper:
+    A. Mishchenko and T. Sasao, "Encoding of Boolean functions and its 
+    application to LUT cascade synthesis", Proc. IWLS '02, pp. 115-120.
+    http://www.eecs.berkeley.edu/~alanmi/publications/2002/iwls02_enc.pdf
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose )
+{
+    DdManager * dd;
+    DdNode ** ppOutputs;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode;
+    char * pFileGeneric;
+    int fBddSizeMax = 500000;
+    int fReorder = 1;
+    int i, clk = clock();
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // compute the global BDDs
+    if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
+        return NULL;
+
+    if ( fVerbose )
+    {
+        DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
+        printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        PRT( "BDD construction time", clock() - clk );
+    }
+
+    // collect global BDDs
+    dd = Abc_NtkGlobalBddMan( pNtk );
+    ppOutputs = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        ppOutputs[i] = Abc_ObjGlobalBdd(pNode);
+
+    // call the decomposition
+    pFileGeneric = Extra_FileNameGeneric( pNtk->pSpec );
+    if ( !Abc_CascadeExperiment( pFileGeneric, dd, ppOutputs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), nLutSize, fCheck, fVerbose ) )
+    {
+        // the LUT size is too small
+    }
+
+    // for now, duplicate the network
+    pNtkNew = Abc_NtkDup( pNtk );
+
+    // cleanup
+    Abc_NtkFreeGlobalBdds( pNtk, 1 );
+    free( ppOutputs );
+    free( pFileGeneric );
+
+//    if ( pNtk->pExdc )
+//        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkCollapse: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index ce67aff7..341ff5b0 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -54,7 +54,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
     if ( fVerbose )
     {
         DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
-        printf( "The shared BDD size is %d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
         PRT( "BDD construction time", clock() - clk );
     }
 
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 200f4eec..235c3672 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -62,7 +62,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     if ( dd == NULL )
         return NULL;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
     // transform the result of mapping into a BDD network
     pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
     Extra_StopManager( dd );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 15a81723..cbd330da 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -294,7 +294,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 )
 {
     char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
@@ -313,7 +313,8 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 
     // start the new network
     pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
-    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
+//    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
+    sprintf( Buffer, "product" );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
     // perform strashing
@@ -324,10 +325,13 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     pRoot1 = Abc_NtkPo(pNtk1,0);
     pRoot2 = Abc_NtkPo(pNtk2,0);
     pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) );
-    pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) );
-
+    pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) ^ fCompl2 );
+    
     // create the miter of the two outputs
-    pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    if ( fOr )
+        pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    else
+        pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
 
     // make sure that everything is okay
diff --git a/src/base/abci/abcPlace.c b/src/base/abci/abcPlace.c
index 5ceffd6f..87c99e99 100644
--- a/src/base/abci/abcPlace.c
+++ b/src/base/abci/abcPlace.c
@@ -120,7 +120,7 @@ float Abc_PlaceEvaluateCut( Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld )
+void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets )
 {
     Abc_Obj_t * pObj, * pFanin;
     int i, k;
@@ -130,24 +130,26 @@ void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld )
     vCells = Vec_PtrAlloc( 16 );
     vNets = Vec_PtrAlloc( 32 );
 
-    // go through the modified nodes
-    Vec_PtrForEachEntry( vUpdates, pObj, i )
+    // go through the new nodes
+    Vec_PtrForEachEntry( vAddedCells, pObj, i )
     {
-        if ( pObj->Id > nNodesOld ) // pObj is a new node
-        {
-            Abc_PlaceCreateCell( pObj, 1 );
-            Abc_PlaceUpdateNet( pObj );
-
-            // add the new cell and its fanin nets to temporary storage
-            Vec_PtrPush( vCells, &(cells[pObj->Id]) );
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-                Vec_PtrPushUnique( vNets, &(nets[pFanin->Id]) );
-        }
-        else // pObj is an old node
-        {
-            Abc_PlaceUpdateNet( Abc_ObjFanin0(pObj) );
-            Abc_PlaceUpdateNet( Abc_ObjFanin1(pObj) );
-        }
+        assert( !Abc_ObjIsComplement(pObj) );
+        Abc_PlaceCreateCell( pObj, 1 );
+        Abc_PlaceUpdateNet( pObj );
+
+        // add the new cell and its fanin nets to temporary storage
+        Vec_PtrPush( vCells, &(cells[pObj->Id]) );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_PtrPushUnique( vNets, &(nets[pFanin->Id]) );
+    }
+
+    // go through the modified nets
+    Vec_PtrForEachEntry( vUpdatedNets, pObj, i )
+    {
+        assert( !Abc_ObjIsComplement(pObj) );
+        if ( Abc_ObjType(pObj) == ABC_OBJ_NONE ) // dead node
+            continue;
+        Abc_PlaceUpdateNet( pObj );
     }
 
     // update the placement
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
new file mode 100644
index 00000000..77d640c2
--- /dev/null
+++ b/src/base/abci/abcQuant.c
@@ -0,0 +1,389 @@
+/**CFile****************************************************************
+
+  FileName    [abcQuant.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [AIG-based variable quantification.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcQuant.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantifies one variable.]
+
+  Description []
+               
+  SideEffects [This procedure creates dangling nodes in the AIG.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pNext, * pFanin;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( iVar < Abc_NtkCiNum(pNtk) );
+
+    // collect the internal nodes
+    pObj = Abc_NtkCi( pNtk, iVar );
+    vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 );
+
+    // assign the cofactors of the CI node to be constants
+    pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) ); 
+    pObj->pData = Abc_AigConst1(pNtk); 
+
+    // quantify the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj )
+        {
+            pFanin = Abc_ObjFanin0(pObj);
+            if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                pFanin->pCopy = pFanin->pData = pFanin;
+            pFanin = Abc_ObjFanin1(pObj);
+            if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                pFanin->pCopy = pFanin->pData = pFanin;
+            pObj->pCopy = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            pObj->pData = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) );
+        }
+    }
+    Vec_PtrFree( vNodes );
+
+    // update the affected COs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            continue;
+        pFanin = Abc_ObjFanin0(pObj);
+        // get the result of quantification
+        pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
+        pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
+        if ( Abc_ObjRegular(pNext) == pFanin )
+            continue;
+        // update the fanins of the CO
+        Abc_ObjPatchFanin( pObj, pFanin, pNext );
+//        if ( Abc_ObjFanoutNum(pFanin) == 0 )
+//            Abc_AigDeleteNode( pNtk->pManFunc, pFanin );
+    }
+
+    // make sure the node has no fanouts
+//    pObj = Abc_NtkCi( pNtk, iVar );
+//    assert( Abc_ObjFanoutNum(pObj) == 0 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the transition relation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
+{
+    char Buffer[1000];
+    Vec_Ptr_t * vPairs;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pMiter;
+    int i, nLatches;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) );
+    nLatches = Abc_NtkLatchNum(pNtk);
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    sprintf( Buffer, "%s_TR", pNtk->pName );
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+//    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Abc_NtkCleanCopy( pNtk );
+    // create current state variables
+    Abc_NtkForEachLatchOutput( pNtk, pObj, i )
+    {
+        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+    }
+    // create next state variables
+    Abc_NtkForEachLatchInput( pNtk, pObj, i )
+        Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL );
+    // create PI variables
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 1 );
+    // restrash the nodes (assuming a topological order of the old network)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // create the function of the primary output
+    assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
+    vPairs = Vec_PtrAlloc( 2*nLatches );
+    Abc_NtkForEachLatchInput( pNtk, pObj, i )
+    {
+        Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
+        Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
+    }
+    pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
+    Vec_PtrFree( vPairs );
+    // add the primary output
+    Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), Abc_ObjNot(pMiter) );
+    Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
+
+    // quantify inputs
+    if ( fInputs )
+    {
+        assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
+        for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
+            Abc_NtkQuantify( pNtkNew, i, fVerbose );
+        Abc_NtkCleanData( pNtkNew );
+        Abc_AigCleanup( pNtkNew->pManFunc );
+        for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
+        {
+            pObj = Abc_NtkPi( pNtkNew, i );
+            assert( Abc_ObjFanoutNum(pObj) == 0 );
+            Abc_NtkDeleteObj( pObj );
+        }
+    }
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkTransRel: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one image computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkInitialState( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pMiter;
+    int i, nVars = Abc_NtkPiNum(pNtk)/2;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the new network 
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // compute the all-zero state in terms of the CS variables
+    pMiter = Abc_AigConst1(pNtkNew);
+    for ( i = 0; i < nVars; i++ )
+        pMiter = Abc_AigAnd( pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) );
+    // add the PO
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Swaps current state and next state variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSwapVariables( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1;
+    int i, nVars = Abc_NtkPiNum(pNtk)/2;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the new network 
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // update the PIs
+    for ( i = 0; i < nVars; i++ )
+    {
+        pObj0 = Abc_NtkPi( pNtk, i );
+        pObj1 = Abc_NtkPi( pNtk, i+nVars );
+        pMiter = pObj0->pCopy;
+        pObj0->pCopy = pObj1->pCopy;
+        pObj1->pCopy = pMiter;
+    }
+    // restrash
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // add the PO
+    pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs reachability analisys.]
+
+  Description [Assumes that the input is the transition relation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp;
+    int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
+    int fFixedPoint = 0;
+    int fSynthesis  = 1;
+
+    assert( Abc_NtkIsStrash(pNtkRel) );
+    assert( Abc_NtkLatchNum(pNtkRel) == 0 );
+    assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 );
+
+    // compute the network composed of the initial states
+    pNtkFront = Abc_NtkInitialState( pNtkRel );
+    pNtkReached = Abc_NtkDup( pNtkFront );
+//Abc_NtkShow( pNtkReached, 0, 0, 0 );
+
+    if ( fVerbose )
+        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
+
+    // perform iterations of reachability analysis
+    nNodesPrev = Abc_NtkNodeNum(pNtkFront);
+    nVars = Abc_NtkPiNum(pNtkRel)/2;
+    for ( i = 0; i < nIters; i++ )
+    {
+        clk = clock();
+        // get the set of next states
+        pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 );
+        Abc_NtkDelete( pNtkFront );
+        // quantify the current state variables
+        for ( v = 0; v < nVars; v++ )
+        {
+            Abc_NtkQuantify( pNtkNext, v, fVerbose );
+            if ( fSynthesis && (v % 3 == 2) )
+            {
+                Abc_NtkCleanData( pNtkNext );
+                Abc_AigCleanup( pNtkNext->pManFunc );
+
+                Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
+                pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
+                Abc_NtkDelete( pNtkTemp );
+            }
+        }
+        Abc_NtkCleanData( pNtkNext );
+        Abc_AigCleanup( pNtkNext->pManFunc );
+        if ( fSynthesis )
+        {
+            Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
+            pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
+            Abc_NtkDelete( pNtkTemp );
+
+            Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
+            Abc_NtkRefactor( pNtkReached, 10, 16, 0, 0, 0, 0 );
+            pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
+            Abc_NtkDelete( pNtkTemp );
+        }
+        // map the next states into the current states
+        pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
+        Abc_NtkDelete( pNtkTemp );
+        // check the termination condition
+        if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) )
+        {
+            fFixedPoint = 1;
+            printf( "Fixed point is reached!\n" );
+            Abc_NtkDelete( pNtkNext );
+            break;
+        }
+        // compute new front
+        pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 );
+        Abc_NtkDelete( pNtkNext );
+        // add the reached states
+        pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 );
+        Abc_NtkDelete( pNtkTemp );
+        // compress the size of Front
+        nNodesOld = Abc_NtkNodeNum(pNtkFront);
+        if ( fSynthesis )
+        {
+            Abc_NtkRewrite( pNtkFront, 0, 0, 0, 0, 0 );
+            pNtkFront = Abc_NtkBalance( pNtkTemp = pNtkFront, 0, 0, 0 );          
+            Abc_NtkDelete( pNtkTemp );
+
+            Abc_NtkRewrite( pNtkReached, 0, 0, 0, 0, 0 );
+            pNtkReached = Abc_NtkBalance( pNtkTemp = pNtkReached, 0, 0, 0 );          
+            Abc_NtkDelete( pNtkTemp );
+        }
+        nNodesNew = Abc_NtkNodeNum(pNtkFront);
+        // print statistics
+        if ( fVerbose )
+        {
+            printf( "I = %3d : Reached = %6d  Front = %6d  FrontM = %6d  %6.2f %%   ", 
+                i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesNew );
+            PRT( "T", clock() - clk );
+        }
+        nNodesPrev = Abc_NtkNodeNum(pNtkFront);
+    }
+    if ( !fFixedPoint )
+        fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
+
+    // report the stats
+    if ( fVerbose )
+    {
+//        nMints = 1;
+//        fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
+    }
+
+    // complement the output to represent the set of unreachable states
+    Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
+
+    // remove next state variables
+    for ( i = 2*nVars - 1; i >= nVars; i-- )
+    {
+        pObj = Abc_NtkPi( pNtkReached, i );
+        assert( Abc_ObjFanoutNum(pObj) == 0 );
+        Abc_NtkDeleteObj( pObj );
+    }
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkReached ) )
+    {
+        printf( "Abc_NtkReachability: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkReached );
+        return NULL;
+    }
+    return pNtkReached;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index a3209275..3d06dddf 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -38,7 +38,7 @@ static void        Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
 
 extern void  Abc_PlaceBegin( Abc_Ntk_t * pNtk );
 extern void  Abc_PlaceEnd( Abc_Ntk_t * pNtk );
-extern void  Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld );
+extern void  Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -61,7 +61,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
     Cut_Man_t * pManCut;
     Rwr_Man_t * pManRwr;
     Abc_Obj_t * pNode;
-    Vec_Ptr_t * vUpdates = NULL;
+    Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
     Dec_Graph_t * pGraph;
     int i, nNodes, nGain, fCompl;
     int clk, clkStart = clock();
@@ -74,7 +74,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
     if ( fPlaceEnable )
     {
         Abc_PlaceBegin( pNtk );
-        vUpdates = Abc_AigUpdateStart( pNtk->pManFunc );
+        vAddedCells = Abc_AigUpdateStart( pNtk->pManFunc, &vUpdatedNets );
     }
 
     // start the rewriting manager
@@ -132,7 +132,7 @@ Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
 
         // use the array of changed nodes to update placement
         if ( fPlaceEnable )
-            Abc_PlaceUpdate( vUpdates, nNodes );
+            Abc_PlaceUpdate( vAddedCells, vUpdatedNets );
     }
     Extra_ProgressBarStop( pProgress );
 Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 2ce80a8f..88ef009b 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" );
-    // start the new network (constants and CIs are already mappined after this step
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // restrash the nodes (assuming a topological order of the old network)
     Abc_NtkForEachNode( pNtk, pObj, i )
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 8fd2a12f..20804d19 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -84,7 +84,7 @@ clkBdd = clock() - clk;
 //    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
 
     // print the size of the BDDs
-    printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+    printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
 
     // perform naive BDD-based computation
     if ( fUseNaive )
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 7697fde1..ea0a4cd2 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -62,7 +62,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
 
     // create the transition relation (dereferenced global BDDs)
     bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose );              Cudd_Ref( bRelation );
@@ -221,7 +221,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
 {
     DdNode * bRelation, * bReached, * bCubeCs;
     DdNode * bCurrent, * bNext, * bTemp;
-    int nIters;
+    int nIters, nMints;
 
     // perform reachability analisys
     bCurrent  = bInitial;   Cudd_Ref( bCurrent );
@@ -258,9 +258,9 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
     // report the stats
     if ( fVerbose )
     {
-    fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
-    fprintf( stdout, "The number of minterms in the reachable state set = %d.\n", 
-                        (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) ); 
+        nMints = (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
+        fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+        fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
     }
 //PRB( dd, bReached );
     Cudd_Deref( bReached );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 4aa05d07..016ada60 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -3,6 +3,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcAuto.c \
     src/base/abci/abcBalance.c \
     src/base/abci/abcBmc.c \
+    src/base/abci/abcCas.c \
     src/base/abci/abcClpBdd.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
@@ -29,6 +30,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcPlace.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcProve.c \
+    src/base/abci/abcQuant.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \