Version abc60820

41 files changed, 4035 insertions, 230 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 03f5a66f..8bd48874 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -462,6 +462,7 @@ 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 bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
@@ -503,6 +504,7 @@ extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 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_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 );
@@ -519,6 +521,7 @@ extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkCreateBox( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 79669657..8448578e 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -256,6 +256,37 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    // go through the PO nodes and call for each of them
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_NtkNodeSupport_rec( Abc_ObjFanin0(pNode), vNodes );
+    // add unused CIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        if ( !Abc_NodeIsTravIdCurrent( pNode ) )
+            Vec_PtrPush( vNodes, pNode );
+    assert( Vec_PtrSize(vNodes) == Abc_NtkCiNum(pNtk) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of CI nodes in the support of the given nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
 {
     Vec_Ptr_t * vNodes;
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 7d4460bf..f9e529c7 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -54,10 +54,10 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     if ( pNtk->tName2Model )
         return Abc_NtkNetlistToLogicHie( pNtk );
     // start the network
-    if ( !Abc_NtkHasMapping(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
-    else
+    if ( Abc_NtkHasMapping(pNtk) )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
+    else
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc );
     // duplicate the nodes 
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index b8c0462d..1a07ebf2 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     }
     else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen();
-    else
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     // allocate constant node
     if ( !Abc_NtkIsNetlist(pNtk) )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index d993ca65..337ba428 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -409,6 +409,29 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the net with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet;
+    int ObjId;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL );
+    if ( ObjId == -1 )
+        return NULL;
+    pNet = Abc_NtkObj( pNtk, ObjId );
+    return pNet;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finds or creates the net.]
 
   Description []
@@ -568,7 +591,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen());
-    else
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     return pNode;
 }
@@ -596,7 +619,7 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen());
-    else
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     return pNode;
 }
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index ed76f396..bb0606f7 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -30,7 +30,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Abc_ShowFile( char * FileNameDot );
+extern void Abc_ShowFile( char * FileNameDot );
 static void Abc_ShowGetFileName( char * pName, char * pBuffer );
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index afa91c45..f756ef89 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -251,7 +251,12 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk )
     TotalArea = 0.0;
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        assert( pNode->pData );
+//        assert( pNode->pData );
+        if ( pNode->pData == NULL )
+        {
+            printf( "Node without mapping is encountered.\n" );
+            continue;
+        }
         TotalArea += Mio_GateReadArea( pNode->pData );
     }
     return TotalArea;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f3dbe357..c1327f43 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -74,6 +74,7 @@ static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReorder        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+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_CommandOneOutput      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -192,6 +193,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "reorder",       Abc_CommandReorder,          0 );
+    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",      "cone",          Abc_CommandOneOutput,        1 );
@@ -1627,6 +1629,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
+    int fVerbose;
     int fBddSizeMax;
     int fDualRail;
     int fReorder;
@@ -1637,11 +1640,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fVerbose = 1;
     fReorder = 1;
     fDualRail = 0;
-    fBddSizeMax = 1000000;
+    fBddSizeMax = 50000000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Brdh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Brdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1659,6 +1663,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDualRail ^= 1;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'r':
             fReorder ^= 1;
             break;
@@ -1683,11 +1690,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0 );
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -1700,11 +1707,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: collapse [-B num] [-rdh]\n" );
+    fprintf( pErr, "usage: collapse [-B num] [-rdvh]\n" );
     fprintf( pErr, "\t          collapses the network by constructing global BDDs\n" );
     fprintf( pErr, "\t-B num  : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
     fprintf( pErr, "\t-r      : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
     fprintf( pErr, "\t-d      : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
+    fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
 }
@@ -3462,6 +3470,93 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int c;
+    int fReverse;
+    int fVerbose;
+    extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
+    extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fReverse = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'r':
+            fReverse ^= 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 )
+//    {
+//        printf( "Currently this procedure does not work for sequential networks.\n" );
+//        return 1;
+//    }
+
+    // if the var order file is given, implement this order
+    pFileName = NULL;
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pFileName = argv[globalUtilOptind];
+        pFile = fopen( pFileName, "r" );
+        if ( pFile == NULL )
+        {
+            fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
+            return 1;
+        }
+        fclose( pFile );
+    }
+    if ( pFileName )
+        Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
+    else
+        Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: order [-rvh] <file>\n" );
+    fprintf( pErr, "\t         computes a good static CI variable order\n" );
+    fprintf( pErr, "\t-r     : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );  
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4583,7 +4678,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // run the command
 //    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+//    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5105,21 +5201,36 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUpdateLevel, fVerbose;
-    extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose );
+    int c, fUseZeroCost, fVerbose, nIters;
+    extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUpdateLevel = 1;
+    nIters       = 3;
+    fUseZeroCost = 1;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "zvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIters < 0 ) 
+                goto usage;
+            break;
+        case 'z':
+            fUseZeroCost ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5140,7 +5251,7 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyHaig( pNtk, fVerbose );
+    pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5151,9 +5262,10 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: haig [-vh]\n" );
-    fprintf( pErr, "\t         prints HAIG stats after one round of sequential rewriting\n" );
-//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "usage: haig [-Izvh]\n" );
+    fprintf( pErr, "\t         prints HAIG stats after sequential rewriting\n" );
+    fprintf( pErr, "\t-I num : the number of rewriting iterations [default = %d]\n", nIters );
+    fprintf( pErr, "\t-z     : toggle zero-cost replacements [default = %s]\n", fUseZeroCost? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index eed18e1b..1de087e8 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -46,14 +46,17 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
 Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
+    int clk = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
-
     // compute the global BDDs
     if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+    {
+        printf( "The shared BDD size is %d nodes.  ", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+        PRT( "BDD construction time", clock() - clk );
+    }
 
     // create the new network
     if ( fDualRail )
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 7d5ed6ec..42d5173a 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
-static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
 static Ivy_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
 
 static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
@@ -120,17 +120,17 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq )
+Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig )
 {
     Abc_Ntk_t * pNtkAig;
     int nNodes, fCleanup = 1;
     // convert from the AIG manager
     if ( fSeq )
-        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
+        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig );
     else
         pNtkAig = Abc_NtkFromAig( pNtk, pMan );
     // report the cleanup results
-    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+    if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
         printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
@@ -163,11 +163,11 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
     pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
     if ( pMan == NULL )
         return NULL;
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
@@ -179,21 +179,28 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
+    int i;
+
     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
     if ( pMan == NULL )
         return NULL;
 
-    Ivy_ManHaigStart( pMan );
-    Ivy_ManRewriteSeq( pMan, 0, fVerbose );
-    Ivy_ManHaigPrintStats( pMan );
-    Ivy_ManHaigStop( pMan );
+    Ivy_ManHaigStart( pMan, fVerbose );
+    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    for ( i = 1; i < nIters; i++ )
+        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+    Ivy_ManHaigPostprocess( pMan, fVerbose );
+
+    // write working AIG into the current network
+//    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 
+    // write HAIG into the current network
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
 
-//    pNtkAig = Abc_NtkIvyAfterHaig( pNtk, pMan, 1 );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    Ivy_ManHaigStop( pMan );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -239,7 +246,7 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
     if ( pMan == NULL )
         return NULL;
     Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -263,7 +270,9 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
     if ( pMan == NULL )
         return NULL;
     Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+//    Ivy_ManRewriteSeq( pMan, 1, 0 );
+//    Ivy_ManRewriteSeq( pMan, 1, 0 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -288,7 +297,7 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
         return NULL;
     pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
     Ivy_ManStop( pTemp );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -474,14 +483,14 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
 {
     Vec_Int_t * vNodes, * vLatches;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
-    Ivy_Obj_t * pNode;
+    Ivy_Obj_t * pNode, * pTemp;
     int i;
-    assert( Ivy_ManLatchNum(pMan) > 0 );
+//    assert( Ivy_ManLatchNum(pMan) > 0 );
     // perform strashing
     pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
@@ -493,7 +502,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
     {
         pObjNew = Abc_NtkCreateLatch( pNtk );
-        if ( Ivy_ObjInit(pNode) == IVY_INIT_DC )
+        if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
             Abc_LatchSetInitDc( pObjNew );
         else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
             Abc_LatchSetInit1( pObjNew );
@@ -505,14 +514,14 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     // rebuild the AIG
     Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
     {
-        // add the first fanins
+        // add the first fanin
         pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
         if ( Ivy_ObjIsBuf(pNode) )
         {
             pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
             continue;
         }
-        // add the first second
+        // add the second fanin
         pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
         // create the new node
         if ( Ivy_ObjIsExor(pNode) )
@@ -520,6 +529,22 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
         else
             pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
         pNode->TravId = Abc_EdgeFromNode( pObjNew );
+        // process the choice nodes
+        if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
+        {
+            pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
+            pFaninNew->fPhase = 0;
+            assert( !Ivy_IsComplement(pNode->pEquiv) );
+            for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
+            {
+                pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
+                pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
+                pFaninNew->pData = pFaninNew1;
+                pFaninNew = pFaninNew1;
+            }
+            pFaninNew->pData = NULL;
+//            printf( "Writing choice node %d.\n", pNode->Id );
+        }
     }
     // connect the PO nodes
     Abc_NtkForEachPo( pNtkOld, pObj, i )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index ecd44017..ea1beb8c 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -27,7 +27,6 @@
 static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
-static void        Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 6cbab1a6..0976b652 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -246,35 +246,47 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 {
     ProgressBar * pProgress;
     Vec_Ptr_t * vFuncsGlob;
-    Abc_Obj_t * pNode;
+    Abc_Obj_t * pNode, * pFanin;
     DdNode * bFunc;
     DdManager * dd;
-    int i, Counter;
+    int i, k, Counter;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtk->pManFunc );
 
     // start the manager
     assert( pNtk->pManGlob == NULL );
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // set reordering
     if ( fReorder )
         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
 
-    // set the elementary variables
+    // clean storage for local BDDs
     Abc_NtkCleanCopy( pNtk );
+    // set the elementary variables
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
+        if ( Abc_ObjFanoutNum(pNode) > 0 )
+        {
+            pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
+            Cudd_Ref( dd->vars[i] );
+        }
     // assign the constant node BDD
     pNode = Abc_NtkConst1( pNtk );
-    pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
+    if ( Abc_ObjFanoutNum(pNode) > 0 )
+    {
+        pNode->pCopy = (Abc_Obj_t *)dd->one;   
+        Cudd_Ref( dd->one );
+    }
 
     // collect the global functions of the COs
-    vFuncsGlob = Vec_PtrAlloc( 100 );
     Counter = 0;
+    vFuncsGlob = Vec_PtrAlloc( 100 );
     if ( fLatchOnly )
     {
         // construct the BDDs
         pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachLatch( pNtk, pNode, i )
         {
-//            Extra_ProgressBarUpdate( pProgress, i, NULL );
             bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
@@ -295,7 +307,6 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
         pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
-//            Extra_ProgressBarUpdate( pProgress, i, NULL );
             bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
@@ -305,12 +316,12 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
                 Cudd_Quit( dd );
                 return NULL;
             }
-            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );   Cudd_Ref( bFunc );
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );  Cudd_Ref( bFunc ); 
             Vec_PtrPush( vFuncsGlob, bFunc );
         }
         Extra_ProgressBarStop( pProgress );
     }
-
+/*
     // derefence the intermediate BDDs
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( pNode->pCopy ) 
@@ -318,6 +329,22 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
             Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
             pNode->pCopy = NULL;
         }
+*/
+/*
+    // make sure all nodes are derefed
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        if ( pNode->pCopy != NULL )
+            printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pNode->Id );
+        if ( pNode->vFanouts.nSize > 0 )
+            printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pNode->Id );
+    }
+*/
+    // reset references
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            pFanin->vFanouts.nSize++;
+
     // reorder one more time
     if ( fReorder )
     {
@@ -326,6 +353,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
     }
     pNtk->pManGlob = dd;
     pNtk->vFuncsGlob = vFuncsGlob;
+//    Cudd_PrintInfo( dd, stdout );
     return dd;
 }
 
@@ -342,7 +370,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 ***********************************************************************/
 DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
 {
-    DdNode * bFunc, * bFunc0, * bFunc1;
+    DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
     assert( !Abc_ObjIsComplement(pNode) );
     if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
     {
@@ -353,29 +381,87 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
         return NULL;
     }
     // if the result is available return
-    if ( pNode->pCopy )
-        return (DdNode *)pNode->pCopy;
-    // compute the result for both branches
-    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
-    if ( bFunc0 == NULL )
-        return NULL;
-    Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
-    if ( bFunc1 == NULL )
-        return NULL;
-    Cudd_Ref( bFunc1 );
-    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
-    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
-    // get the final result
-    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( dd, bFunc0 );
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    // set the result
-    assert( pNode->pCopy == NULL );
-    pNode->pCopy = (Abc_Obj_t *)bFunc;
-    // increment the progress bar
-    if ( pProgress )
-        Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL );
+    if ( pNode->pCopy == NULL )
+    {
+        Abc_Obj_t * pNodeC, * pNode0, * pNode1;
+        pNode0 = Abc_ObjFanin0(pNode);
+        pNode1 = Abc_ObjFanin1(pNode);
+        // check for the special case when it is MUX/EXOR
+//        if ( 0 )
+        if ( pNode0->pCopy == NULL && pNode1->pCopy == NULL &&
+             Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 && 
+             Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 && 
+             Abc_NodeIsMuxType(pNode) )
+        {
+            // deref the fanins
+            pNode0->vFanouts.nSize--;
+            pNode1->vFanouts.nSize--;
+            // recognize the MUX
+            pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
+            assert( Abc_ObjFanoutNum(pNodeC) > 1 );
+            // dereference the control once (the second time it will be derefed when BDDs are computed)
+            pNodeC->vFanouts.nSize--;
+
+            // compute the result for all branches
+            bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFuncC == NULL )
+                return NULL;
+            Cudd_Ref( bFuncC );
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc0 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc0 );
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc1 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc1 );
+
+            // complement the branch BDDs
+            bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjIsComplement(pNode0) );
+            bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjIsComplement(pNode1) );
+            // get the final result
+            bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 );   Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc0 );
+            Cudd_RecursiveDeref( dd, bFunc1 );
+            Cudd_RecursiveDeref( dd, bFuncC );
+            // add the number of used nodes
+            (*pCounter) += 3;
+        }
+        else
+        {
+            // compute the result for both branches
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc0 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc0 );
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc1 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc1 );
+            bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+            bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+            // get the final result
+            bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc0 );
+            Cudd_RecursiveDeref( dd, bFunc1 );
+            // add the number of used nodes
+            (*pCounter)++;
+        }
+        // set the result
+        assert( pNode->pCopy == NULL );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+        // increment the progress bar
+        if ( pProgress )
+            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
+    }
+    // prepare the return value
+    bFunc = (DdNode *)pNode->pCopy;
+    // dereference BDD at the node
+    if ( --pNode->vFanouts.nSize == 0 )
+    {
+        Cudd_Deref( bFunc );
+        pNode->pCopy = NULL;
+    }
     return bFunc;
 }
 
diff --git a/src/base/abci/abcOrder.c b/src/base/abci/abcOrder.c
new file mode 100644
index 00000000..c9ebdc12
--- /dev/null
+++ b/src/base/abci/abcOrder.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+  FileName    [abcOrder.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Exploring static BDD variable orders.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcOrder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Changes the order of primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose )
+{
+    Vec_Ptr_t * vSupp;
+    vSupp = Abc_NtkSupport( pNtk );
+    Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
+    Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given variable order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose )
+{
+    char Buffer[1000];
+    FILE * pFile;
+    Vec_Ptr_t * vSupp;
+    Abc_Obj_t * pObj;
+    pFile = fopen( pFileName, "r" );
+    vSupp = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
+    while ( fscanf( pFile, "%s", Buffer ) == 1 )
+    {
+        pObj = Abc_NtkFindTerm( pNtk, Buffer );
+        if ( pObj == NULL || !Abc_ObjIsCi(pObj) )
+        {
+            printf( "Name \"%s\" is not a PI name. Cannot use this order.\n", Buffer );
+            Vec_PtrFree( vSupp );
+            fclose( pFile );
+            return;
+        }
+        Vec_PtrPush( vSupp, pObj );
+    }
+    fclose( pFile );
+    if ( Vec_PtrSize(vSupp) != Abc_NtkCiNum(pNtk) )
+    {
+        printf( "The number of names in the order (%d) is not the same as the number of PIs (%d).\n", Vec_PtrSize(vSupp), Abc_NtkCiNum(pNtk) );
+        Vec_PtrFree( vSupp );
+        return;
+    }
+    Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
+    Vec_PtrFree( vSupp );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Changes the order of primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Vec_PtrSize(vSupp) == Abc_NtkCiNum(pNtk) );
+    // order CIs using the array
+    if ( fReverse )
+        Vec_PtrForEachEntry( vSupp, pObj, i )
+            Vec_PtrWriteEntry( pNtk->vCis, Vec_PtrSize(vSupp)-1-i, pObj );
+    else
+        Vec_PtrForEachEntry( vSupp, pObj, i )
+            Vec_PtrWriteEntry( pNtk->vCis, i, pObj );
+    // order PIs accordingly
+    Vec_PtrClear( pNtk->vPis );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjIsPi(pObj) )
+            Vec_PtrPush( pNtk->vPis, pObj );
+//    Abc_NtkForEachCi( pNtk, pObj, i )
+//        printf( "%s ", Abc_ObjName(pObj) );
+//    printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 5d35678d..2e338e48 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,6 +15,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
+    src/base/abci/abcOrder.c \
     src/base/abci/abcPga.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcProve.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 614fa812..6da1f4d8 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -32,6 +32,8 @@ static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadVer     ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadVerLib  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 
@@ -45,6 +47,7 @@ static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
@@ -71,6 +74,8 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_ver",      IoCommandReadVer,      1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_verlib",   IoCommandReadVerLib,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
 
@@ -84,6 +89,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_verlib",  IoCommandWriteVerLib,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
 }
 
@@ -659,6 +665,209 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    st_table * tDesign;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+    extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    tDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck );
+    if ( tDesign == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
+        return 1;
+    }
+
+    if ( st_count(tDesign) == 1 )
+    {
+        st_generator * gen;
+        char * pName;
+        // find the network
+        st_foreach_item( tDesign, gen, (char**)&pName, (char**)&pNtk )
+        {
+            st_free_gen(gen);
+            break;
+        }
+        st_free_table( tDesign );
+
+        // convert it into a logic network
+        pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+        if ( pNtk == NULL )
+        {
+            fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+            return 1;
+        }
+        // replace the current network
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    }
+    else
+    {
+        printf( "The design includes more than one module and is currently not used.\n" );
+    }
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_ver [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read a network in structural verilog (using current library)\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    st_table * tDesign;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+    extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
+    extern void Ver_ParseFreeLibrary( st_table * pLibVer );
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    tDesign = Ver_ParseFile( FileName, NULL, fCheck );
+    if ( tDesign == NULL )
+    {
+        fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
+        return 1;
+    }
+    printf( "The library contains %d gates.\n", st_count(tDesign) );
+
+    // convert gates into AIGs
+    {
+        st_table * tLibrary;
+        st_generator * gen;
+        char * pName;
+        // transform the gates into the library AIGs
+        tLibrary  = st_init_table( strcmp, st_strhash );
+        st_foreach_item( tDesign, gen, (char**)&pName, (char**)&pNtk )
+        {
+            // convert the netlist into SOP logic network
+            pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+            Abc_NtkDelete( pTemp );
+            // perform structural hashing
+            pNtk = Abc_NtkStrash( pTemp = pNtk, 0, 1 );
+            Abc_NtkDelete( pTemp );
+            // insert the new network into the new library
+            st_insert( tLibrary, pNtk->pName, (char *)pNtk );
+        }
+        st_free_table( tDesign );
+
+        // free old library
+        if ( Abc_FrameReadLibVer() )
+            Ver_ParseFreeLibrary( Abc_FrameReadLibVer() );
+        // read new library
+        Abc_FrameSetLibVer( tLibrary );
+    }
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_verlib [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read a gate library in structural verilog\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pTemp;
@@ -1472,6 +1681,61 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    st_table * tLibrary;
+    char * FileName;
+    int c;
+    extern void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName );
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+
+    // derive the netlist
+    tLibrary = Abc_FrameReadLibVer();
+    if ( tLibrary == NULL )
+    {
+        fprintf( pAbc->Out, "Verilog library is not specified.\n" );
+        return 0;
+    }
+    Io_WriteVerilogLibrary( tLibrary, FileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_verlib [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the current verilog library\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 11dd2db1..ade9051f 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -43,6 +43,7 @@ struct Io_ReadBlif_t_
     // the error message
     FILE *               Output;       // the output stream
     char                 sError[1000]; // the error string generated during parsing
+    int                  fError;       // set to 1 when error occurs
 };
 
 static Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName );
@@ -182,7 +183,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
             return NULL;
         }
     }
-    else
+    else if ( !p->fError )
         Abc_NtkFinalizeRead( pNtkMaster );
     // return the master network
     return pNtkMaster;
@@ -273,7 +274,11 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         if ( p->vTokens == NULL ) // some files do not have ".end" in the end
             break;
         if ( fStatus == 1 )
+        {
+            Extra_ProgressBarStop( pProgress );
+            Abc_NtkDelete( pNtk );
             return NULL;
+        }
     }
     if ( p->pNtkMaster == NULL )
     Extra_ProgressBarStop( pProgress );
@@ -487,6 +492,16 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
     // set the pointer to the functionality of the node
     Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, p->vCubes->pArray) );
 
+    // check the size
+    if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum(Abc_ObjData(pNode)) )
+    {
+        p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+        sprintf( p->sError, "The number of fanins (%d) of node %s is different from SOP size (%d).", 
+            Abc_ObjFaninNum(pNode), Abc_ObjName(Abc_ObjFanout(pNode,0)), Abc_SopGetVarNum(Abc_ObjData(pNode)) );
+        Io_ReadBlifPrintErrorMessage( p );
+        return 1;
+    }
+
     // return the last array of tokens
     *pvTokens = vTokens;
     return 0;
@@ -735,6 +750,7 @@ int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vToken
 ***********************************************************************/
 void Io_ReadBlifPrintErrorMessage( Io_ReadBlif_t * p )
 {
+    p->fError = 1;
     if ( p->LineCur == 0 ) // the line number is not given
         fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
     else // print the error message with the line number
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
index 902219aa..594bf4eb 100644
--- a/src/base/io/ioWriteVer.c
+++ b/src/base/io/ioWriteVer.c
@@ -36,6 +36,7 @@ static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -73,6 +74,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     }
 
     // write the equations for the network
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     Io_WriteVerilogInt( pFile, pNtk );
     fprintf( pFile, "\n" );
     fclose( pFile );
@@ -80,6 +82,49 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
 
 /**Function*************************************************************
 
+  Synopsis    [Write verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
+{
+    FILE * pFile;
+    st_generator * gen;
+    Abc_Ntk_t * pNtk, * pNetlist;
+    char * pName;
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteVerilogLibrary(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    fprintf( pFile, "// Verilog library \"%s\" written by ABC on %s\n", pFileName, Extra_TimeStamp() );
+    fprintf( pFile, "\n" );
+    // write modules
+    st_foreach_item( tLibrary, gen, (char**)&pName, (char**)&pNtk )
+    {
+        // create netlist
+        pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+        // write the equations for the network
+        Io_WriteVerilogInt( pFile, pNetlist );
+        fprintf( pFile, "\n" );
+        // delete the netlist
+        Abc_NtkDelete( pNetlist );
+    }
+
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes verilog.]
 
   Description []
@@ -92,7 +137,6 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
 void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     // write inputs and outputs
-    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
     Io_WriteVerilogPis( pFile, pNtk, 3 );
     fprintf( pFile, ",\n   " );
@@ -111,9 +155,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
     Io_WriteVerilogRegs( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
     }
+    if ( Io_WriteVerilogWiresCount(pNtk) > 0 )
+    {
     fprintf( pFile, "  wire" );
     Io_WriteVerilogWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
+    }
     // write the nodes
     if ( Abc_NtkHasMapping(pNtk) )
         Io_WriteVerilogGates( pFile, pNtk );
@@ -205,7 +252,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the wires.]
+  Synopsis    [Counts the number of wires.]
 
   Description []
                
@@ -214,15 +261,10 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pTerm, * pNet;
-    int LineLength;
-    int AddedLength;
-    int NameCounter;
-    int i, Counter, nNodes;
-
-    // count the number of wires
+    int i, nNodes;
     nNodes = Abc_NtkLatchNum(pNtk);
     Abc_NtkForEachNode( pNtk, pTerm, i )
     {
@@ -233,6 +275,30 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             continue;
         nNodes++;
     }
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of wires
+    nNodes = Io_WriteVerilogWiresCount( pNtk );
 
     // write the wires
     Counter = 0;
diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c
index feb7a47e..cdfd98b8 100644
--- a/src/base/main/libSupport.c
+++ b/src/base/main/libSupport.c
@@ -44,42 +44,71 @@ void open_libs() {
 #else
     DIR* dirp;
     struct dirent* dp;
+    char *env, *init_p, *p;
+    int done;
+
+    env = getenv ("ABC_LIB_PATH");
+    if (env == NULL) {
+      printf("Warning: ABC_LIB_PATH not defined. Looking into the current directory.\n");
+      init_p = malloc (2*sizeof(char));
+      init_p[0]='.'; init_p[1] = 0;
+    } else {
+      init_p = malloc ((strlen(env)+1)*sizeof(char));
+      strcpy (init_p, env);
+    }
 
-    dirp = opendir(".");
-    while ((dp = readdir(dirp)) != NULL) {
+    // Extract directories and read libraries
+    done = 0;
+    p = init_p;
+    while (!done) {
+      char *endp = strchr (p,':');
+      if (endp == NULL) done = 1; // last directory in the list
+      else *endp = 0; // end of string
+
+      dirp = opendir(p);
+      if (dirp == NULL) {
+        printf("Warning: directory in ABC_LIB_PATH does not exist (%s).\n", p);
+        continue;
+      }
+
+      while ((dp = readdir(dirp)) != NULL) {
         if ((strncmp("libabc_", dp->d_name, 7) == 0) &&
             (strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) {
 
-            // make sure we don't overflow the handle array
-            if (curr_lib >= MAX_LIBS) {
-                printf("Warning: maximum number of ABC libraries (%d) exceeded.  Not loading %s.\n",
-                       MAX_LIBS,
-                       dp->d_name);
-            }
-
-            // attempt to load it
-            else {
-                char* szPrefixed = malloc((strlen(dp->d_name) + 3) * sizeof(char));
-                strcpy(szPrefixed, "./");
-                strcat(szPrefixed, dp->d_name);
-
-                libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
-
-                // did the load succeed?
-                if (libHandles[curr_lib] != 0) {
-                    printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
-                    curr_lib++;
-                } else {
-                    printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
-                }
-
-                free(szPrefixed);
+          // make sure we don't overflow the handle array
+          if (curr_lib >= MAX_LIBS) {
+            printf("Warning: maximum number of ABC libraries (%d) exceeded.  Not loading %s.\n",
+                   MAX_LIBS,
+                   dp->d_name);
+          }
+          
+          // attempt to load it
+          else {
+            char* szPrefixed = malloc((strlen(dp->d_name) + strlen(p) + 2) * 
+                                      sizeof(char));
+            sprintf(szPrefixed, "%s/", p);
+            strcat(szPrefixed, dp->d_name);
+            libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
+            
+            // did the load succeed?
+            if (libHandles[curr_lib] != 0) {
+              printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
+              curr_lib++;
+            } else {
+              printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
             }
+            
+            free(szPrefixed);
+          }
         }
+      }
+      closedir(dirp);
+      p = endp+1;
     }
-    closedir(dirp);
-#endif
 
+    free(init_p);
+#endif
+    
     // null terminate the list of handles
     libHandles[curr_lib] = 0;    
 }
diff --git a/src/base/main/main.h b/src/base/main/main.h
index fe511314..80238a05 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -97,6 +97,7 @@ extern int             Abc_FrameReadNtkStoreSize();
 extern void *          Abc_FrameReadLibLut();                    
 extern void *          Abc_FrameReadLibGen();                    
 extern void *          Abc_FrameReadLibSuper();                  
+extern void *          Abc_FrameReadLibVer();                  
 extern void *          Abc_FrameReadManDd();                     
 extern void *          Abc_FrameReadManDec();                    
 extern char *          Abc_FrameReadFlag( char * pFlag ); 
@@ -107,6 +108,7 @@ extern void            Abc_FrameSetNtkStoreSize( int nStored );
 extern void            Abc_FrameSetLibLut( void * pLib );        
 extern void            Abc_FrameSetLibGen( void * pLib );        
 extern void            Abc_FrameSetLibSuper( void * pLib );      
+extern void            Abc_FrameSetLibVer( void * pLib );      
 extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
 #ifdef __cplusplus
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index a1011a36..068a8bfb 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -48,6 +48,7 @@ int         Abc_FrameReadNtkStoreSize()              { return s_GlobalFrame->nSt
 void *      Abc_FrameReadLibLut()                    { return s_GlobalFrame->pLibLut;      } 
 void *      Abc_FrameReadLibGen()                    { return s_GlobalFrame->pLibGen;      } 
 void *      Abc_FrameReadLibSuper()                  { return s_GlobalFrame->pLibSuper;    } 
+void *      Abc_FrameReadLibVer()                    { return s_GlobalFrame->pLibVer;      } 
 void *      Abc_FrameReadManDd()                     { if ( s_GlobalFrame->dd == NULL )      s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );  return s_GlobalFrame->dd;      } 
 void *      Abc_FrameReadManDec()                    { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart();                                        return s_GlobalFrame->pManDec; } 
 char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
@@ -57,6 +58,7 @@ void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored  =
 void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
 void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
 void        Abc_FrameSetLibSuper( void * pLib )      { s_GlobalFrame->pLibSuper = pLib;    } 
+void        Abc_FrameSetLibVer( void * pLib )        { s_GlobalFrame->pLibVer   = pLib;    } 
 void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );  } 
 
 /**Function*************************************************************
@@ -135,11 +137,13 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void Rwt_ManGlobalStop();
     extern void undefine_cube_size();
+    extern void Ver_ParseFreeLibrary( st_table * pLibVer );
 //    extern void Ivy_TruthManStop();
 //    Abc_HManStop();
     undefine_cube_size();
     Rwt_ManGlobalStop();
 //    Ivy_TruthManStop();
+    if ( p->pLibVer ) Ver_ParseFreeLibrary( p->pLibVer );
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index d2bca1ab..13c71759 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -72,6 +72,7 @@ struct Abc_Frame_t_
     void *          pLibLut;     // the current LUT library
     void *          pLibGen;     // the current genlib
     void *          pLibSuper;   // the current supergate library
+    void *          pLibVer;     // the current Verilog library
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/temp.c b/src/base/temp.c
new file mode 100644
index 00000000..55709247
--- /dev/null
+++ b/src/base/temp.c
@@ -0,0 +1,83 @@
+
+/**Function*************************************************************
+
+  Synopsis    [Command procedure to allow for static BDD variable ordering.]
+
+  Description [This procedure should be integrated in "abc\src\base\abci\abc.c"
+  similar to how procedure Abc_CommandReorder() is currently integrated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int c;
+    int fReverse;
+    int fVerbose;
+    extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
+    extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fReverse = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'r':
+            fReverse ^= 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 the var order file is given, implement this order
+    pFileName = NULL;
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pFileName = argv[globalUtilOptind];
+        pFile = fopen( pFileName, "r" );
+        if ( pFile == NULL )
+        {
+            fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
+            return 1;
+        }
+        fclose( pFile );
+    }
+    if ( pFileName )
+        Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
+    else
+        Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: order [-rvh] <file>\n" );
+    fprintf( pErr, "\t         computes a good static CI variable order\n" );
+    fprintf( pErr, "\t-r     : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );  
+    return 1;
+}
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 2409284e..a3cb714e 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -114,6 +114,7 @@ struct Ivy_Man_t_
     void *           pData;          // the temporary data
     void *           pCopy;          // the temporary data
     Ivy_Man_t *      pHaig;          // history AIG if present
+    int              nClassesSkip;   // the number of skipped classes
     // memory management
     Vec_Ptr_t *      vChunks;        // allocated memory pieces
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
@@ -395,7 +396,9 @@ extern Ivy_Obj_t *     Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t *
 extern Ivy_Obj_t *     Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
 /*=== ivyCheck.c ========================================================*/
 extern int             Ivy_ManCheck( Ivy_Man_t * p );
+extern int             Ivy_ManCheckFanoutNums( Ivy_Man_t * p );
 extern int             Ivy_ManCheckFanouts( Ivy_Man_t * p );
+extern int             Ivy_ManCheckChoices( Ivy_Man_t * p );
 /*=== ivyCut.c ==========================================================*/
 extern void            Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
 extern Ivy_Store_t *   Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
@@ -406,6 +409,7 @@ extern void            Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront,
 extern Vec_Vec_t *     Ivy_ManLevelize( Ivy_Man_t * p );
 extern Vec_Int_t *     Ivy_ManRequiredLevels( Ivy_Man_t * p );
 extern int             Ivy_ManIsAcyclic( Ivy_Man_t * p );
+extern int             Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig );
 /*=== ivyDsd.c ==========================================================*/
 extern int             Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
 extern void            Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
@@ -422,10 +426,10 @@ extern void            Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
 extern Ivy_Obj_t *     Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern int             Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 /*=== ivyHaig.c ==========================================================*/
-extern void            Ivy_ManHaigStart( Ivy_Man_t * p );
+extern void            Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
 extern void            Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
 extern void            Ivy_ManHaigStop( Ivy_Man_t * p );
-extern void            Ivy_ManHaigPrintStats( Ivy_Man_t * p );
+extern void            Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
 extern void            Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
 extern void            Ivy_ManHaigSimulate( Ivy_Man_t * p );
@@ -477,6 +481,8 @@ extern int             Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int f
 extern int             Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
 /*=== ivySeq.c =========================================================*/
 extern int             Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
+/*=== ivyShow.c =========================================================*/
+extern void            Ivy_ManShow( Ivy_Man_t * pMan, int fHaig );
 /*=== ivyTable.c ========================================================*/
 extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
@@ -497,6 +503,8 @@ extern void            Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj,
 extern int             Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
 extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
 extern Ivy_Obj_t *     Ivy_ObjReal( Ivy_Obj_t * pObj );
+extern void            Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig );
+extern void            Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
 
 #ifdef __cplusplus
 }
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index ebae64ff..55448f19 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -142,6 +142,29 @@ int Ivy_ManCheck( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Ivy_ManCheckFanoutNums( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i, Counter = 0;
+    Ivy_ManForEachObj( p, pObj, i )
+        if ( Ivy_ObjIsNode(pObj) )
+            Counter += (Ivy_ObjRefs(pObj) == 0);
+    if ( Counter )
+        printf( "Sequential AIG has %d dangling nodes.\n", Counter );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Ivy_ManCheckFanouts( Ivy_Man_t * p )
 {
     Vec_Ptr_t * vFanouts;
@@ -215,6 +238,34 @@ int Ivy_ManCheckFanouts( Ivy_Man_t * p )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks that each choice node has exactly one node with fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManCheckChoices( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj, * pTemp;
+    int i;
+    Ivy_ManForEachObj( p->pHaig, pObj, i )
+    {
+        if ( Ivy_ObjRefs(pObj) == 0 )
+            continue;
+        // count the number of nodes in the loop
+        assert( !Ivy_IsComplement(pObj->pEquiv) );
+        for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+            if ( Ivy_ObjRefs(pTemp) > 1 )
+                printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 314bed8d..c27cba31 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -39,18 +39,35 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManDfs_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
+void Ivy_ManDfs_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
 {
-    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
-        return;
     if ( Ivy_ObjIsMarkA(pObj) )
         return;
     Ivy_ObjSetMarkA(pObj);
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+    {
+        if ( p->pHaig == NULL && pObj->pEquiv )
+            Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
+        return;
+    }
+//printf( "visiting node %d\n", pObj->Id );
+/*
+    if ( pObj->Id == 87 || pObj->Id == 90 )
+    {
+        int y = 0;
+    }
+*/
     assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
-    Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
     if ( !Ivy_ObjIsBuf(pObj) )
-        Ivy_ManDfs_rec( Ivy_ObjFanin1(pObj), vNodes );
+        Ivy_ManDfs_rec( p, Ivy_ObjFanin1(pObj), vNodes );
+    if ( p->pHaig == NULL && pObj->pEquiv )
+        Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
     Vec_IntPush( vNodes, pObj->Id );
+
+//printf( "adding node %d with fanins %d and %d and equiv %d (refs = %d)\n", 
+//       pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id, 
+//       pObj->pEquiv? Ivy_Regular(pObj->pEquiv)->Id: -1, Ivy_ObjRefs(pObj) );
 }
 
 /**Function*************************************************************
@@ -76,9 +93,11 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
     // collect the nodes
     vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
     Ivy_ManForEachPo( p, pObj, i )
-        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+        Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
     // unmark the collected nodes
-    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+//    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+//        Ivy_ObjClearMarkA(pObj);
+    Ivy_ManForEachObj( p, pObj, i )
         Ivy_ObjClearMarkA(pObj);
     // make sure network does not have dangling nodes
     assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
@@ -101,7 +120,7 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
     Vec_Int_t * vNodes, * vLatches;
     Ivy_Obj_t * pObj;
     int i;
-    assert( Ivy_ManLatchNum(p) > 0 );
+//    assert( Ivy_ManLatchNum(p) > 0 );
     // make sure the nodes are not marked
     Ivy_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
@@ -112,15 +131,23 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
     // collect the nodes
     vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
     Ivy_ManForEachPo( p, pObj, i )
-        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+        Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
     Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
-        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+        Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
     // unmark the collected nodes
-    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+//    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+//        Ivy_ObjClearMarkA(pObj);
+    Ivy_ManForEachObj( p, pObj, i )
         Ivy_ObjClearMarkA(pObj);
     // make sure network does not have dangling nodes
 //    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
-    *pvLatches = vLatches;
+
+// temporary!!!
+
+    if ( pvLatches == NULL )
+        Vec_IntFree( vLatches );
+    else
+        *pvLatches = vLatches;
     return vNodes;
 }
 
@@ -261,47 +288,64 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
+    // skip the node if it is already visited
+    if ( Ivy_ObjIsTravIdPrevious(p, pObj) )
         return 1;
-    assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
-    // make sure the node is not visited
-    assert( !Ivy_ObjIsTravIdPrevious(p, pNode) );
     // check if the node is part of the combinational loop
-    if ( Ivy_ObjIsTravIdCurrent(p, pNode) )
+    if ( Ivy_ObjIsTravIdCurrent(p, pObj) )
     {
         fprintf( stdout, "Manager contains combinational loop!\n" );
-        fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n",  Ivy_ObjId(pNode) );
-        fprintf( stdout, " %d",  Ivy_ObjId(pNode) );
+        fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n",  Ivy_ObjId(pObj) );
+        fprintf( stdout, " %d",  Ivy_ObjId(pObj) );
         return 0;
     }
     // mark this node as a node on the current path
-    Ivy_ObjSetTravIdCurrent( p, pNode );
-    // check if the fanin is visited
-    if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) ) 
+    Ivy_ObjSetTravIdCurrent( p, pObj );
+    // explore equivalent nodes if pObj is the main node
+    if ( p->pHaig == NULL && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
     {
-        // traverse the fanin's cone searching for the loop
-        if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+        Ivy_Obj_t * pTemp;
+        assert( !Ivy_IsComplement(pObj->pEquiv) );
+        for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
         {
-            // return as soon as the loop is detected
-            fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin0(pNode)) );
-            return 0;
+            // traverse the fanin's cone searching for the loop
+            if ( !Ivy_ManIsAcyclic_rec(p, pTemp) )
+            {
+                // return as soon as the loop is detected
+                fprintf( stdout, " -> (%d", Ivy_ObjId(pObj) );
+                for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+                    fprintf( stdout, " %d", Ivy_ObjId(pTemp) );
+                fprintf( stdout, ")" );
+                return 0; 
+            }
         }
     }
-    // check if the fanin is visited
-    if ( Ivy_ObjIsNode(pNode) && !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) 
+    // quite if it is a CI node
+    if ( Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
     {
-        // traverse the fanin's cone searching for the loop
-        if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) )
-        {
-            // return as soon as the loop is detected
-            fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin1(pNode)) );
-            return 0;
-        }
+        // mark this node as a visited node
+        Ivy_ObjSetTravIdPrevious( p, pObj );
+        return 1;
+    }
+    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+    // traverse the fanin's cone searching for the loop
+    if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
+    {
+        // return as soon as the loop is detected
+        fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
+        return 0;
+    }
+    // traverse the fanin's cone searching for the loop
+    if ( Ivy_ObjIsNode(pObj) && !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pObj)) )
+    {
+        // return as soon as the loop is detected
+        fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
+        return 0;
     }
     // mark this node as a visited node
-    Ivy_ObjSetTravIdPrevious( p, pNode );
+    Ivy_ObjSetTravIdPrevious( p, pObj );
     return 1;
 }
 
@@ -325,30 +369,123 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
 ***********************************************************************/
 int Ivy_ManIsAcyclic( Ivy_Man_t * p )
 {
-    Ivy_Obj_t * pNode;
+    Ivy_Obj_t * pObj;
     int fAcyclic, i;
     // set the traversal ID for this DFS ordering
     Ivy_ManIncrementTravId( p );   
     Ivy_ManIncrementTravId( p );   
-    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
-    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
-    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
+    // pObj->TravId == pNet->nTravIds      means "pObj is on the path"
+    // pObj->TravId == pNet->nTravIds - 1  means "pObj is visited but is not on the path"
+    // pObj->TravId <  pNet->nTravIds - 1  means "pObj is not visited"
     // traverse the network to detect cycles
     fAcyclic = 1;
-    Ivy_ManForEachCo( p, pNode, i )
+    Ivy_ManForEachCo( p, pObj, i )
     {
-        if ( Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
-            continue;
         // traverse the output logic cone
-        if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+        if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
             continue;
         // stop as soon as the first loop is detected
-        fprintf( stdout, " (cone of CO \"%d\")\n", Ivy_ObjFaninId0(pNode) );
+        fprintf( stdout, " (cone of %s \"%d\")\n", Ivy_ObjIsLatch(pObj)? "latch" : "PO", Ivy_ObjId(pObj) );
         break;
     }
     return fAcyclic;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the levels of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManSetLevels_rec( Ivy_Obj_t * pObj, int fHaig )
+{
+    // quit if the node is visited
+    if ( Ivy_ObjIsMarkA(pObj) )
+        return pObj->Level;
+    Ivy_ObjSetMarkA(pObj);
+    // quit if this is a CI
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+        return 0;
+    assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
+    // get levels of the fanins
+    Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
+    if ( !Ivy_ObjIsBuf(pObj) )
+        Ivy_ManSetLevels_rec( Ivy_ObjFanin1(pObj), fHaig );
+    // get level of the node
+    if ( Ivy_ObjIsBuf(pObj) )
+        pObj->Level = 1 + Ivy_ObjFanin0(pObj)->Level;
+    else if ( Ivy_ObjIsNode(pObj) )
+        pObj->Level = Ivy_ObjLevelNew( pObj );
+    else assert( 0 );
+    // get level of other choices
+    if ( fHaig && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
+    {
+        Ivy_Obj_t * pTemp;
+        unsigned LevelMax = pObj->Level;
+        for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+        {
+            Ivy_ManSetLevels_rec( pTemp, fHaig );
+            LevelMax = IVY_MAX( LevelMax, pTemp->Level );
+        }
+        // get this level
+        pObj->Level = LevelMax;
+        for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+            pTemp->Level = LevelMax;
+    }
+    return pObj->Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the levels of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig )
+{
+    Ivy_Obj_t * pObj;
+    int i, LevelMax;
+    // check if CIs have choices
+    if ( fHaig )
+    {
+        Ivy_ManForEachCi( p, pObj, i )
+            if ( pObj->pEquiv )
+                printf( "CI %d has a choice, which will not be visualized.\n", pObj->Id );
+    }
+    // clean the levels
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->Level = 0;
+    // compute the levels
+    LevelMax = 0;
+    Ivy_ManForEachCo( p, pObj, i )
+    {
+        Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
+        LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
+    }
+    // compute levels of nodes without fanout
+    Ivy_ManForEachObj( p, pObj, i )
+        if ( (Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj)) && Ivy_ObjRefs(pObj) == 0 )
+        {
+            Ivy_ManSetLevels_rec( pObj, fHaig );
+            LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
+        }
+    // clean the marks
+    Ivy_ManForEachObj( p, pObj, i )
+        Ivy_ObjClearMarkA(pObj);
+    return LevelMax;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c
index 7ce71a60..ca68c3c6 100644
--- a/src/temp/ivy/ivyHaig.c
+++ b/src/temp/ivy/ivyHaig.c
@@ -26,16 +26,17 @@
 
 /* 
     HAIGing rules in working AIG:
-    - The node points to the representative of its class
-    - The pointer can be complemented if they have different polarity
+    - Each node in the working AIG has a pointer to the corresponding node in HAIG 
+      (this node is not necessarily the representative of the equivalence class of HAIG nodes)
+    - This pointer is complemented if the AIG node and its corresponding HAIG node have different phase
 
     Choice node rules in HAIG:
     - Equivalent nodes are linked into a ring
-    - Exactly one node in the ring has fanouts (this node is called representative)
-    - Pointer going from a node to the next node in the ring is complemented 
-      if the first node is complemented, compared to the representative node
-    - The representative node always has non-complemented pointer to the next node
-    - New nodes are inserted into the ring before the representative node
+    - Exactly one node in the ring has fanouts (this node is called the representative)
+    - The pointer going from a node to the next node in the ring is complemented 
+      if the first node is complemented, compared to the representative node of the equivalence class
+    - (consequence of the above) The representative node always has non-complemented pointer to the next node
+    - New nodes are inserted into the ring immediately after the representative node
 */
 
 // returns the representative node of the given HAIG node
@@ -52,7 +53,7 @@ static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
         if ( Ivy_ObjRefs(pTemp) > 0 )
             break;
     // return the representative node
-    assert( pTemp != pObj );
+    assert( Ivy_ObjRefs(pTemp) > 0 );
     return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
 }
 
@@ -65,8 +66,8 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
     assert( Ivy_ObjRefs(pObj) > 0 );
     if ( pObj->pEquiv == NULL )
         return 1;
-    Counter = 1;
     assert( !Ivy_IsComplement(pObj->pEquiv) );
+    Counter = 1;
     for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
         Counter++;
     return Counter;
@@ -87,10 +88,28 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManHaigStart( Ivy_Man_t * p )
+void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose )
 {
+    Vec_Int_t * vLatches;
+    Ivy_Obj_t * pObj;
+    int i;
     assert( p->pHaig == NULL );
     p->pHaig = Ivy_ManDup( p );
+
+    if ( fVerbose )
+    {
+        printf( "Starting : " );
+        Ivy_ManPrintStats( p->pHaig );
+    }
+
+    // collect latches of design D and set their values to be DC
+    vLatches = Vec_IntAlloc( 100 );
+    Ivy_ManForEachLatch( p->pHaig, pObj, i )
+    {
+        pObj->Init = IVY_INIT_DC;
+        Vec_IntPush( vLatches, pObj->Id );
+    }
+    p->pHaig->pData = vLatches;
 }
 
 /**Function*************************************************************
@@ -131,6 +150,7 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
     Ivy_Obj_t * pObj;
     int i;
     assert( p->pHaig != NULL );
+    Vec_IntFree( p->pHaig->pData );
     Ivy_ManStop( p->pHaig );
     p->pHaig = NULL;
     // remove dangling pointers to the HAIG objects
@@ -151,17 +171,54 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
 ***********************************************************************/
 void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
+    Ivy_Obj_t * pEquiv0, * pEquiv1;
     assert( p->pHaig != NULL );
     assert( !Ivy_IsComplement(pObj) );
     if ( Ivy_ObjType(pObj) == IVY_BUF )
         pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
     else if ( Ivy_ObjType(pObj) == IVY_LATCH )
-        pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+    {
+//        pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+        pEquiv0 = Ivy_ObjChild0Equiv(pObj);
+        pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
+        pObj->pEquiv = Ivy_Latch( p->pHaig, pEquiv0, pObj->Init );
+    }
     else if ( Ivy_ObjType(pObj) == IVY_AND )
-        pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+    {
+//        pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+        pEquiv0 = Ivy_ObjChild0Equiv(pObj);
+        pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
+        pEquiv1 = Ivy_ObjChild1Equiv(pObj);
+        pEquiv1 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv1)), Ivy_IsComplement(pEquiv1) );
+        pObj->pEquiv = Ivy_And( p->pHaig, pEquiv0, pEquiv1 );
+    }
     else assert( 0 );
     // make sure the node points to the representative
-    pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+//    pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the old node is in the TFI of the new node.]
+
+  Description [] 
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ObjIsInTfi_rec( Ivy_Obj_t * pObjNew, Ivy_Obj_t * pObjOld, int Levels )
+{
+    if ( pObjNew == pObjOld )
+        return 1;
+    if ( Levels == 0 || Ivy_ObjIsCi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
+        return 0;
+    if ( Ivy_ObjIsInTfi_rec( Ivy_ObjFanin0(pObjNew), pObjOld, Levels - 1 ) )
+        return 1;
+    if ( Ivy_ObjIsNode(pObjNew) && Ivy_ObjIsInTfi_rec( Ivy_ObjFanin1(pObjNew), pObjOld, Levels - 1 ) )
+        return 1;
+    return 0;
 }
 
 /**Function*************************************************************
@@ -180,10 +237,16 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
     Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
     Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
     int fCompl;
+//printf( "\nCreating choice for %d and %d in AIG\n", pObjOld->Id, Ivy_Regular(pObjNew)->Id );
+
     assert( p->pHaig != NULL );
-    // get pointers to the classes
+    assert( !Ivy_IsComplement(pObjOld) );
+    // get pointers to the representatives of pObjOld and pObjNew
     pObjOldHaig = pObjOld->pEquiv;
     pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
+    // get the classes
+    pObjOldHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjOldHaig)), Ivy_IsComplement(pObjOldHaig) );
+    pObjNewHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjNewHaig)), Ivy_IsComplement(pObjNewHaig) );
     // get regular pointers
     pObjOldHaigR = Ivy_Regular(pObjOldHaig);
     pObjNewHaigR = Ivy_Regular(pObjNewHaig);
@@ -192,17 +255,41 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
     // if the class is the same, nothing to do
     if ( pObjOldHaigR == pObjNewHaigR )
         return;
-    // combine classes
-    // assume the second node does not belong to a class
-    assert( pObjNewHaigR->pEquiv == NULL );
+    // if the second node belongs to a class, do not merge classes (for the time being)
+    if ( Ivy_ObjRefs(pObjOldHaigR) == 0 || pObjNewHaigR->pEquiv != NULL || 
+        Ivy_ObjRefs(pObjNewHaigR) > 0 || Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
+    {
+/*
+        if ( pObjNewHaigR->pEquiv != NULL )
+            printf( "c" );
+        if ( Ivy_ObjRefs(pObjNewHaigR) > 0 )
+            printf( "f" );
+        printf( " " );
+*/
+        p->pHaig->nClassesSkip++;
+        return;
+    }
+
     // add this node to the class of pObjOldHaig
+    assert( Ivy_ObjRefs(pObjOldHaigR) > 0 );
+    assert( !Ivy_IsComplement(pObjOldHaigR->pEquiv) );
     if ( pObjOldHaigR->pEquiv == NULL )
         pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
     else
         pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
     pObjOldHaigR->pEquiv = pObjNewHaigR;
+//printf( "Setting choice node %d -> %d.\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
     // update the class of the new node
-    Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+//    Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+//printf( "Creating choice for %d and %d in HAIG\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
+
+//    if ( pObjOldHaigR->Id == 13 )
+//    {
+//        Ivy_ManShow( p, 0 );
+//        Ivy_ManShow( p->pHaig, 1 );
+//    }
+//    if ( !Ivy_ManIsAcyclic( p->pHaig ) )
+//        printf( "HAIG contains a cycle\n" );
 }
 
 /**Function*************************************************************
@@ -227,17 +314,16 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
         if ( Ivy_ObjIsTerm(pObj) || i == 0 )
             continue;
         if ( Ivy_ObjRefs(pObj) == 0 )
-        {
-            assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) );
             continue;
-        }
         Counter = Ivy_HaigObjCountClass( pObj );
         nChoiceNodes += (int)(Counter > 1);
         nChoices += Counter - 1;
+//        if ( Counter > 1 )
+//            printf( "Choice node %d %s\n", pObj->Id, Ivy_ObjIsLatch(pObj)? "(latch)": "" );
     }
     *pnChoices = nChoices;
     return nChoiceNodes;
-}
+} 
 
 /**Function*************************************************************
 
@@ -250,19 +336,35 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManHaigPrintStats( Ivy_Man_t * p )
+void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose )
 {
     int nChoices, nChoiceNodes;
+
     assert( p->pHaig != NULL );
-    printf( "Original : " );
-    Ivy_ManPrintStats( p );
-    printf( "HAIG     : " );
-    Ivy_ManPrintStats( p->pHaig );
-
-    // print choice node stats
-    nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
-    printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices ); 
-    Ivy_ManHaigSimulate( p );
+
+    if ( fVerbose )
+    {
+        printf( "Final    : " );
+        Ivy_ManPrintStats( p );
+        printf( "HAIG     : " );
+        Ivy_ManPrintStats( p->pHaig );
+
+        // print choice node stats
+        nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
+        printf( "Total choice nodes = %d. Total choices = %d. Skipped classes = %d.\n", 
+            nChoiceNodes, nChoices, p->pHaig->nClassesSkip ); 
+    }
+
+    if ( Ivy_ManIsAcyclic( p->pHaig ) )
+    {
+        if ( fVerbose )
+            printf( "HAIG is acyclic\n" );
+    }
+    else
+        printf( "HAIG contains a cycle\n" );
+
+    if ( fVerbose )
+        Ivy_ManHaigSimulate( p );
 }
 
 
@@ -289,6 +391,32 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
 
 /**Function*************************************************************
 
+  Synopsis    [Applies the simulation rules.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Ivy_Init_t Ivy_ManHaigSimulateChoice( Ivy_Init_t In0, Ivy_Init_t In1 )
+{
+    assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
+    if ( (In0 == IVY_INIT_0 && In1 == IVY_INIT_1) || (In0 == IVY_INIT_1 && In1 == IVY_INIT_0) )
+    {
+         printf( "Compatibility fails.\n" );
+         return IVY_INIT_0;
+    }
+    if ( In0 == IVY_INIT_DC && In1 == IVY_INIT_DC )
+        return IVY_INIT_DC;
+    if ( In0 != IVY_INIT_DC )
+        return In0;
+    return In1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Simulate HAIG using modified 3-valued simulation.]
 
   Description []
@@ -300,39 +428,85 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
 ***********************************************************************/
 void Ivy_ManHaigSimulate( Ivy_Man_t * p )
 {
-    Vec_Int_t * vNodes, * vLatches;
-    Ivy_Obj_t * pObj;
+    Vec_Int_t * vNodes, * vLatches, * vLatchesD;
+    Ivy_Obj_t * pObj, * pTemp;
     Ivy_Init_t In0, In1;
     int i, k, Counter;
+    int fVerbose = 0;
+
+    // check choices
+    Ivy_ManCheckChoices( p );
+
+    // switch to HAIG
     assert( p->pHaig != NULL );
     p = p->pHaig;
+
+if ( fVerbose )
+Ivy_ManForEachPi( p, pObj, i )
+printf( "Setting PI %d\n", pObj->Id );
+
     // collect latches and nodes in the DFS order
     vNodes = Ivy_ManDfsSeq( p, &vLatches );
+
+if ( fVerbose )
+Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+printf( "Collected node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
+
     // set the PI values
-    Ivy_ManConst1(p)->Init = IVY_INIT_0;
+    Ivy_ManConst1(p)->Init = IVY_INIT_1;
     Ivy_ManForEachPi( p, pObj, i )
         pObj->Init = IVY_INIT_0;
+
     // set the latch values
     Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
         pObj->Init = IVY_INIT_DC;
+    // set the latches of D to be determinate
+    vLatchesD = p->pData;
+    Ivy_ManForEachNodeVec( p, vLatchesD, pObj, i )
+        pObj->Init = IVY_INIT_0;
+
     // perform several rounds of simulation
-    for ( k = 0; k < 5; k++ )
+    for ( k = 0; k < 10; k++ )
     {
         // count the number of non-determinate values
         Counter = 0;
         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
             Counter += ( pObj->Init == IVY_INIT_DC );
-        printf( "Iter %d : Non-determinate = %d\n", k, Counter );               
+        printf( "Iter %d : Non-determinate = %d\n", k, Counter );    
+        
         // simulate the internal nodes
         Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         {
+if ( fVerbose )
+printf( "Processing node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
             In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
             In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
             pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
+            // simulate the equivalence class if the node is a representative
+            if ( pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
+            {
+if ( fVerbose )
+printf( "Processing choice node %d\n", pObj->Id );
+                In0 = pObj->Init;
+                assert( !Ivy_IsComplement(pObj->pEquiv) );
+                for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+                {
+if ( fVerbose )
+printf( "Processing secondary node %d\n", pTemp->Id );
+                    In1 = Ivy_InitNotCond( pTemp->Init, Ivy_IsComplement(pTemp->pEquiv) );
+                    In0 = Ivy_ManHaigSimulateChoice( In0, In1 );
+                }
+                pObj->Init = In0;
+            }
         }
+
         // simulate the latches
         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        {
             pObj->Level = Ivy_ObjFanin0(pObj)->Init;
+if ( fVerbose )
+printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
+        }
         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
             pObj->Init = pObj->Level, pObj->Level = 0;
     }
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index e3b8a5b8..786949e7 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -58,7 +58,7 @@ Ivy_Man_t * Ivy_ManStart()
     Ivy_ManStartMemory( p );
     // create the constant node
     p->pConst1 = Ivy_ManFetchMemory( p );
-    p->pConst1->fPhase = 1;
+//    p->pConst1->fPhase = 1;
     Vec_PtrPush( p->vObjs, p->pConst1 );
     p->nCreated = 1;
     // start the table
@@ -118,6 +118,9 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
     // free arrays
     Vec_IntFree( vNodes );
     Vec_IntFree( vLatches );
+    // make sure structural hashing did not change anything
+    assert( Ivy_ManNodeNum(p)  == Ivy_ManNodeNum(pNew) );
+    assert( Ivy_ManLatchNum(p) == Ivy_ManLatchNum(pNew) );
     // check the resulting network
     if ( !Ivy_ManCheck(pNew) )
         printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
@@ -182,7 +185,7 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
                
   SideEffects []
 
-  SeeAlso     []
+  SeeAlso     [] 
 
 ***********************************************************************/
 int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index e8924b5b..36af3920 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -114,6 +114,11 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Ivy_ObjType(pObj)]++;
     p->nCreated++;
+
+//    printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " );
+//    Ivy_ObjPrintVerbose( pObj, p->pHaig==NULL );
+//    printf( "\n" );
+
     // if HAIG is defined, create a corresponding node
     if ( p->pHaig )
         Ivy_ManHaigCreateObj( p, pObj );
@@ -192,8 +197,6 @@ void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
     // add the first fanin
     pObj->pFanin0 = NULL;
     pObj->pFanin1 = NULL;
-
-//    Ivy_ManCheckFanouts( p );
 }
 
 /**Function*************************************************************
@@ -324,7 +327,14 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     assert( pObjOld != Ivy_Regular(pObjNew) );
     // if HAIG is defined, create the choice node
     if ( p->pHaig )
+    {
+//        if ( pObjOld->Id == 31 )
+//        {
+//            Ivy_ManShow( p, 0 );
+//            Ivy_ManShow( p->pHaig, 1 );
+//        }
         Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
+    }
     // if the new object is complemented or already used, add the buffer
     if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
         pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
@@ -388,6 +398,19 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
         Vec_PtrPush( p->vBufs, pObjOld );
 //    Ivy_ManCheckFanouts( p );
 //    printf( "\n" );
+/*
+    if ( p->pHaig )
+    {
+        int x;
+        Ivy_ManShow( p, 0 );
+        Ivy_ManShow( p->pHaig, 1 );
+        x = 0;
+    }
+*/
+//    if ( Ivy_ManCheckFanoutNums(p) )
+//    {
+//        int x = 0;
+//    }
 }
 
 /**Function*************************************************************
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwr.c
index 64331579..3f8720ba 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwr.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [ivyRwtPre.c]
+  FileName    [ivyRwt.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - May 11, 2006.]
 
-  Revision    [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+  Revision    [$Id: ivyRwt.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 11660e42..44a35d33 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -58,6 +58,9 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
     int clk, clkStart = clock();
+    // set the DC latch values
+    Ivy_ManForEachLatch( p, pNode, i )
+        pNode->Init = IVY_INIT_DC;
     // start the rewriting manager
     pManRwt = Rwt_ManStart( 0 );
     p->pData = pManRwt;
@@ -92,12 +95,6 @@ clk = clock();
             Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
             if ( fCompl ) Dec_GraphComplement( pGraph );
 Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
-/*
-            if ( !Ivy_ManIsAcyclic(p) )
-            {
-                int x = 0;
-            }
-*/
         }
     }
 Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
@@ -109,6 +106,8 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
     p->pData = NULL;
     // fix the levels
     Ivy_ManResetLevels( p );
+//    if ( Ivy_ManCheckFanoutNums(p) )
+//        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
     // check
     if ( !Ivy_ManCheck(p) )
         printf( "Ivy_ManRewritePre(): The check has failed.\n" );
@@ -139,7 +138,8 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
     Dec_Graph_t * pGraph;
     Ivy_Store_t * pStore;
     Ivy_Cut_t * pCut;
-    Ivy_Obj_t * pFanin;
+    Ivy_Obj_t * pFanin;//, * pFanout;
+    Vec_Ptr_t * vFanout;
     unsigned uPhase, uTruthBest, uTruth;
     char * pPerm;
     int nNodesSaved, nNodesSaveCur;
@@ -154,6 +154,7 @@ p->timeCut += clock() - clk;
 
     // go through the cuts
 clk = clock();
+    vFanout = Vec_PtrAlloc( 100 );
     for ( c = 1; c < pStore->nCuts; c++ )
     {
         pCut = pStore->pCuts + c;
@@ -193,6 +194,9 @@ clk2 = clock();
         // label MFFC with current ID
         Ivy_ManIncrementTravId( pMan );
         nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
+        // label fanouts with the current ID
+//        Ivy_ObjForEachFanout( pMan, pNode, vFanout, pFanout, i )
+//            Ivy_ObjSetTravIdCurrent( pMan, pFanout );
         // unmark the fanin boundary
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
@@ -233,11 +237,19 @@ p->timeEval += clock() - clk2;
                 Vec_PtrPush( p->vFanins, pFanin );
         }
     }
+    Vec_PtrFree( vFanout );
 p->timeRes += clock() - clk;
 
     if ( GainBest == -1 )
         return -1;
 
+/*
+    printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
+    for ( i = 0; i < pCut->nSize; i++ )
+        printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+    printf( " }\n" );
+*/
+
     // copy the leaves
     Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
 
@@ -250,10 +262,9 @@ p->timeRes += clock() - clk;
     if ( GainBest > 0 )
     {
         Ivy_Cut_t * pCut = p->pCut;
-        printf( "Useful cut : {" );
+        printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
         for ( i = 0; i < pCut->nSize; i++ )
-            printf( "   %5d[%2d](%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]), 
-                Ivy_ObjRefs( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) );
+            printf( " %5d(%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
         printf( " }\n" );
     }
 */
@@ -974,18 +985,19 @@ void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
                
   SideEffects []
 
-  SeeAlso     []
+  SeeAlso     [] 
 
 ***********************************************************************/
 static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
 {
-    int iLeaf;
+    int nLats, iLeaf;
     assert( !Ivy_IsComplement(pFanin) );
     if ( !Ivy_ObjIsLatch(pFanin) )
         return Ivy_LeafCreate( pFanin->Id, 0 );
-    iLeaf = Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
-    assert( Ivy_LeafLat(iLeaf) < IVY_LEAF_MASK );
-    return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
+    iLeaf = Ivy_CutReadLeaf(Ivy_ObjFanin0(pFanin));
+    nLats = Ivy_LeafLat(iLeaf);
+    assert( nLats < IVY_LEAF_MASK );
+    return 1 + iLeaf;
 }
 
 /**Function*************************************************************
diff --git a/src/temp/ivy/ivyShow.c b/src/temp/ivy/ivyShow.c
new file mode 100644
index 00000000..3105081e
--- /dev/null
+++ b/src/temp/ivy/ivyShow.c
@@ -0,0 +1,326 @@
+/**CFile****************************************************************
+
+  FileName    [ivyShow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Visualization of HAIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyShow.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
+{
+    extern void Abc_ShowFile( char * FileNameDot );
+    static Counter = 0;
+    char FileNameDot[200];
+    FILE * pFile;
+    // create the file name
+//    Ivy_ShowGetFileName( pMan->pName, FileNameDot );
+    sprintf( FileNameDot, "temp%02d.dot", Counter++ );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    fclose( pFile );
+    // generate the file
+    Ivy_WriteDotAig( pMan, FileNameDot, fHaig );
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the graph structure of AIG for DOT.]
+
+  Description [Useful for graph visualization using tools such as GraphViz: 
+  http://www.graphviz.org/]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
+{
+    FILE * pFile;
+    Ivy_Obj_t * pNode, * pTemp, * pPrev;
+    int LevelMax, Level, i;
+
+    if ( Ivy_ManNodeNum(pMan) > 200 )
+    {
+        fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" );
+        return;
+    }
+    if ( (pFile = fopen( pFileName, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // compute levels
+    LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig );
+
+    // write the DOT header
+    fprintf( pFile, "# %s\n",  "AIG structure generated by IVY package" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "digraph AIG {\n" );
+    fprintf( pFile, "size = \"7.5,10\";\n" );
+//  fprintf( pFile, "ranksep = 0.5;\n" );
+//  fprintf( pFile, "nodesep = 0.5;\n" );
+    fprintf( pFile, "center = true;\n" );
+//  fprintf( pFile, "orientation = landscape;\n" );
+//  fprintf( pFile, "edge [fontsize = 10];\n" );
+//  fprintf( pFile, "edge [dir = none];\n" );
+    fprintf( pFile, "edge [dir = back];\n" );
+    fprintf( pFile, "\n" );
+
+    // labels on the left of the picture
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  node [shape = plaintext];\n" );
+    fprintf( pFile, "  edge [style = invis];\n" );
+    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
+    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
+    // generate node names with labels
+    for ( Level = LevelMax; Level >= 0; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d", Level );
+        fprintf( pFile, " [label = " );
+        // label name
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "];\n" );
+    }
+
+    // genetate the sequence of visible/invisible nodes to mark levels
+    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
+    for ( Level = LevelMax; Level >= 0; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d",  Level );
+        // the connector
+        if ( Level != 0 )
+            fprintf( pFile, " ->" );
+        else
+            fprintf( pFile, ";" );
+    }
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate title box on top
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle1;\n" );
+    fprintf( pFile, "  title1 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=20,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "%s", "AIG structure visualized by ABC" );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
+    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate statistics box
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle2;\n" );
+    fprintf( pFile, "  title2 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=18,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Ivy_ManNodeNum(pMan), LevelMax );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate the COs
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    // the labeling node of this level
+    fprintf( pFile, "  Level%d;\n",  LevelMax );
+    // generate the CO nodes
+    Ivy_ManForEachCo( pMan, pNode, i )
+    {
+        if ( fHaig || pNode->pEquiv == NULL )
+            fprintf( pFile, "  Node%d%s [label = \"%d%s\"", pNode->Id, 
+                (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
+        else
+            fprintf( pFile, "  Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id, 
+                (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":""), 
+                    Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
+        fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"invtriangle") );
+        fprintf( pFile, ", color = coral, fillcolor = coral" );
+        fprintf( pFile, "];\n" );
+    }
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate nodes of each rank
+    for ( Level = LevelMax - 1; Level > 0; Level-- )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  Level );
+        Ivy_ManForEachObj( pMan, pNode, i )
+        {
+            if ( (int)pNode->Level != Level )
+                continue;
+            if ( fHaig || pNode->pEquiv == NULL )
+                fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
+            else 
+                fprintf( pFile, "  Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, 
+                    Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
+            fprintf( pFile, ", shape = ellipse" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate the CI nodes
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    // the labeling node of this level
+    fprintf( pFile, "  Level%d;\n",  0 );
+    // generate constant node
+    if ( Ivy_ObjRefs(Ivy_ManConst1(pMan)) > 0 )
+    {
+        pNode = Ivy_ManConst1(pMan);
+        // check if the costant node is present
+        fprintf( pFile, "  Node%d [label = \"Const1\"", pNode->Id );
+        fprintf( pFile, ", shape = ellipse" );
+        fprintf( pFile, ", color = coral, fillcolor = coral" );
+        fprintf( pFile, "];\n" );
+    }
+    // generate the CI nodes
+    Ivy_ManForEachCi( pMan, pNode, i )
+    {
+        if ( fHaig || pNode->pEquiv == NULL )
+            fprintf( pFile, "  Node%d%s [label = \"%d%s\"", pNode->Id, 
+                (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":"") );
+        else
+            fprintf( pFile, "  Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id, 
+                (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":""), 
+                    Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
+        fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"triangle") );
+        fprintf( pFile, ", color = coral, fillcolor = coral" );
+        fprintf( pFile, "];\n" );
+    }
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate invisible edges from the square down
+    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+    Ivy_ManForEachCo( pMan, pNode, i )
+        fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
+
+    // generate edges
+    Ivy_ManForEachObj( pMan, pNode, i )
+    {
+        if ( !Ivy_ObjIsNode(pNode) && !Ivy_ObjIsCo(pNode) && !Ivy_ObjIsBuf(pNode) )
+            continue;
+        // generate the edge from this node to the next
+        fprintf( pFile, "Node%d%s",  pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
+        fprintf( pFile, " -> " );
+        fprintf( pFile, "Node%d%s",  Ivy_ObjFaninId0(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin0(pNode))? "_out":"") );
+        fprintf( pFile, " [" );
+        fprintf( pFile, "style = %s", Ivy_ObjFaninC0(pNode)? "dotted" : "bold" );
+//        if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
+//        fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
+        fprintf( pFile, "]" );
+        fprintf( pFile, ";\n" );
+        if ( !Ivy_ObjIsNode(pNode) )
+            continue;
+        // generate the edge from this node to the next
+        fprintf( pFile, "Node%d",  pNode->Id );
+        fprintf( pFile, " -> " );
+        fprintf( pFile, "Node%d%s",  Ivy_ObjFaninId1(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin1(pNode))? "_out":"") );
+        fprintf( pFile, " [" );
+        fprintf( pFile, "style = %s", Ivy_ObjFaninC1(pNode)? "dotted" : "bold" );
+//        if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
+//        fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
+        fprintf( pFile, "]" );
+        fprintf( pFile, ";\n" );
+        // generate the edges between the equivalent nodes
+        if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
+        {
+            pPrev = pNode;
+            for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
+            {
+                fprintf( pFile, "Node%d",  pPrev->Id );
+                fprintf( pFile, " -> " );
+                fprintf( pFile, "Node%d",  pTemp->Id );
+                fprintf( pFile, " [style = %s]", Ivy_IsComplement(pTemp->pEquiv)? "dotted" : "bold" );
+                fprintf( pFile, ";\n" );
+                pPrev = pTemp;
+            }
+            // connect the last node with the first
+            fprintf( pFile, "Node%d",  pPrev->Id );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d",  pNode->Id );
+            fprintf( pFile, " [style = %s]", Ivy_IsComplement(pPrev->pEquiv)? "dotted" : "bold" );
+            fprintf( pFile, ";\n" );
+        }
+    }
+
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c
index fe9c3570..2ac0ae49 100644
--- a/src/temp/ivy/ivyTable.c
+++ b/src/temp/ivy/ivyTable.c
@@ -167,7 +167,7 @@ void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew )
         return;
     pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == pObj->Id ); // node should be in the table
-    *pPlace = ObjIdNew;
+    *pPlace = ObjIdNew; 
 }
 
 /**Function*************************************************************
@@ -203,7 +203,7 @@ int Ivy_TableCountEntries( Ivy_Man_t * p )
 void Ivy_TableResize( Ivy_Man_t * p )
 {
     int * pTableOld, * pPlace;
-    int nTableSizeOld, Counter, e, clk;
+    int nTableSizeOld, Counter, nEntries, e, clk;
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
@@ -224,7 +224,8 @@ clk = clock();
         assert( *pPlace == 0 ); // should not be in the table
         *pPlace = pTableOld[e];
     }
-    assert( Counter == Ivy_ManHashObjNum(p) );
+    nEntries = Ivy_ManHashObjNum(p);
+//    assert( Counter == nEntries );
 //    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
 //    PRT( "Time", clock() - clk );
     // replace the table and the parameters
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index a23e76c9..3c53bd21 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -612,6 +612,98 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
     return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints node in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig )
+{
+    Ivy_Obj_t * pTemp;
+    assert( !Ivy_IsComplement(pObj) );
+    printf( "Node %5d : ", Ivy_ObjId(pObj) );
+    if ( Ivy_ObjIsConst1(pObj) )
+        printf( "constant 1" );
+    else if ( Ivy_ObjIsPi(pObj) )
+        printf( "PI" );
+    else if ( Ivy_ObjIsPo(pObj) )
+        printf( "PO" );
+    else if ( Ivy_ObjIsLatch(pObj) )
+        printf( "latch %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
+    else if ( Ivy_ObjIsBuf(pObj) )
+        printf( "buffer %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
+    else
+        printf( "AND( %5d%s, %5d%s )", 
+            Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "), 
+            Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") );
+    printf( " (refs = %3d)", Ivy_ObjRefs(pObj) );
+    if ( !fHaig )
+    {
+        if ( pObj->pEquiv == NULL )
+            printf( " HAIG node not given" );
+        else
+            printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") );
+        return;
+    }
+    if ( pObj->pEquiv == NULL )
+        return;
+    // there are choices
+    if ( Ivy_ObjRefs(pObj) > 0 )
+    {
+        // print equivalence class
+        printf( "  { %5d ", pObj->Id );
+        assert( !Ivy_IsComplement(pObj->pEquiv) );
+        for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+            printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") );
+        printf( " }" );
+        return;
+    }
+    // this is a secondary node
+    for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) );
+    assert( Ivy_ObjRefs(pTemp) > 0 );
+    printf( "  class of %d", pTemp->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints node in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
+{
+    Vec_Int_t * vNodes;
+    Ivy_Obj_t * pObj;
+    int i;
+    printf( "PIs: " );
+    Ivy_ManForEachPi( p, pObj, i )
+        printf( " %d", pObj->Id );
+    printf( "\n" );
+    printf( "POs: " );
+    Ivy_ManForEachPo( p, pObj, i )
+        printf( " %d", pObj->Id );
+    printf( "\n" );
+    printf( "Latches: " );
+    Ivy_ManForEachLatch( p, pObj, i )
+        printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
+    printf( "\n" );
+    vNodes = Ivy_ManDfsSeq( p, NULL );
+    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        Ivy_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
+    printf( "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index e7ba865a..c208c8ee 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -12,7 +12,7 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyObj.c \
     src/temp/ivy/ivyOper.c \
     src/temp/ivy/ivyResyn.c \
-    src/temp/ivy/ivyRwrPre.c \
+    src/temp/ivy/ivyRwr.c \
     src/temp/ivy/ivySeq.c \
     src/temp/ivy/ivyTable.c \
     src/temp/ivy/ivyUtil.c
diff --git a/src/temp/ver/ver.h b/src/temp/ver/ver.h
new file mode 100644
index 00000000..ea1613c0
--- /dev/null
+++ b/src/temp/ver/ver.h
@@ -0,0 +1,111 @@
+/**CFile****************************************************************
+
+  FileName    [ver.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: ver.h,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __VER_H__
+#define __VER_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ver_Man_t_       Ver_Man_t;
+typedef struct Ver_Stream_t_    Ver_Stream_t;
+
+struct Ver_Man_t_
+{
+    // input file stream
+    char *          pFileName;
+    Ver_Stream_t *  pReader;
+    ProgressBar *   pProgress;
+    // current network and library
+    Abc_Ntk_t *     pNtkCur;       // the network under construction
+    st_table *      pLibrary;      // the current design library
+    st_table *      pGateLib;      // the current technology library
+    // error recovery
+    FILE *          Output;
+    int             fTopLevel;
+    int             fError;
+    char            sError[2000];
+    // intermediate structures
+    Vec_Ptr_t *     vNames;  
+    Vec_Ptr_t *     vStackFn;
+    Vec_Int_t *     vStackOp;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== verCore.c ========================================================*/
+extern st_table *     Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
+extern void           Ver_ParsePrintErrorMessage( Ver_Man_t * p );
+/*=== verFormula.c ========================================================*/
+extern DdNode *       Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage );
+/*=== verParse.c ========================================================*/
+extern int            Ver_ParseSkipComments( Ver_Man_t * p );
+extern char *         Ver_ParseGetName( Ver_Man_t * p );
+/*=== verStream.c ========================================================*/
+extern Ver_Stream_t * Ver_StreamAlloc( char * pFileName );
+extern void           Ver_StreamFree( Ver_Stream_t * p );
+extern char *         Ver_StreamGetFileName( Ver_Stream_t * p );
+extern int            Ver_StreamGetFileSize( Ver_Stream_t * p );
+extern int            Ver_StreamGetCurPosition( Ver_Stream_t * p );
+extern int            Ver_StreamGetLineNumber( Ver_Stream_t * p );
+
+extern int            Ver_StreamIsOkey( Ver_Stream_t * p );
+extern char           Ver_StreamScanChar( Ver_Stream_t * p );
+extern char           Ver_StreamPopChar( Ver_Stream_t * p );
+extern void           Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip );
+extern void           Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop );
+extern char *         Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c
new file mode 100644
index 00000000..8ef38aad
--- /dev/null
+++ b/src/temp/ver/verCore.c
@@ -0,0 +1,933 @@
+/**CFile****************************************************************
+
+  FileName    [verCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of structural Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verCore.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// types of verilog signals
+typedef enum { 
+    VER_SIG_NONE = 0,
+    VER_SIG_INPUT,
+    VER_SIG_OUTPUT,
+    VER_SIG_INOUT,
+    VER_SIG_REG,
+    VER_SIG_WIRE
+} Ver_SignalType_t;
+
+static void Ver_ParseFreeData( Ver_Man_t * p );
+static void Ver_ParseInternal( Ver_Man_t * p, int fCheck );
+static int  Ver_ParseModule( Ver_Man_t * p );
+static int  Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType );
+static int  Ver_ParseAssign( Ver_Man_t * p );
+static int  Ver_ParseAlways( Ver_Man_t * p );
+static int  Ver_ParseInitial( Ver_Man_t * p );
+static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate );
+
+static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
+static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
+static Abc_Obj_t * Ver_ParseCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
+static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck )
+{
+    Ver_Man_t * p;
+    st_table * pLibrary;
+    // start the file reader    
+    p = ALLOC( Ver_Man_t, 1 );
+    memset( p, 0, sizeof(Ver_Man_t) );
+    p->pFileName = pFileName;
+    p->pReader   = Ver_StreamAlloc( pFileName );
+    p->pLibrary  = st_init_table( st_ptrcmp, st_ptrhash );
+    p->pGateLib  = pGateLib;
+    p->Output    = stdout;
+    p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) );
+    p->vNames    = Vec_PtrAlloc( 100 );
+    p->vStackFn  = Vec_PtrAlloc( 100 );
+    p->vStackOp  = Vec_IntAlloc( 100 );
+    // parse the file
+    Ver_ParseInternal( p, fCheck );
+    // stop the parser
+    assert( p->pNtkCur == NULL );
+    pLibrary = p->pLibrary;
+    Ver_StreamFree( p->pReader );
+    Extra_ProgressBarStop( p->pProgress );
+    Vec_PtrFree( p->vNames   );
+    Vec_PtrFree( p->vStackFn );
+    Vec_IntFree( p->vStackOp );
+    free( p );
+    return pLibrary;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseFreeLibrary( st_table * pLibVer )
+{
+    st_generator * gen;
+    Abc_Ntk_t * pNtk;
+    char * pName;
+    st_foreach_item( pLibVer, gen, (char**)&pName, (char**)&pNtk )
+        Abc_NtkDelete( pNtk );
+    st_free_table( pLibVer );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseFreeData( Ver_Man_t * p )
+{
+    if ( p->pNtkCur )
+    {
+        Abc_NtkDelete( p->pNtkCur );
+        p->pNtkCur = NULL;
+    }
+    if ( p->pLibrary )
+    {
+        Ver_ParseFreeLibrary( p->pLibrary );
+        p->pLibrary = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck )
+{
+    char * pToken;
+    while ( 1 )
+    {
+        // get the next token
+        pToken = Ver_ParseGetName( pMan );
+        if ( pToken == NULL )
+            break;
+        if ( strcmp( pToken, "module" ) )
+        {
+            sprintf( pMan->sError, "Cannot read \"module\" directive." );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+        // parse the module
+        if ( !Ver_ParseModule( pMan ) )
+            return;
+        // check the network for correctness
+        if ( fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) )
+        {
+            pMan->fTopLevel = 1;
+            sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+        // add the module to the hash table
+        if ( st_is_member( pMan->pLibrary, pMan->pNtkCur->pName ) )
+        {
+            pMan->fTopLevel = 1;
+            sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+        st_insert( pMan->pLibrary, pMan->pNtkCur->pName, (char *)pMan->pNtkCur );
+        pMan->pNtkCur = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the error message including the file name and line number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
+{
+    p->fError = 1;
+    if ( p->fTopLevel ) // the line number is not given
+        fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
+    else // print the error message with the line number
+        fprintf( p->Output, "%s (line %d): %s\n", 
+            p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
+    // free the data
+    Ver_ParseFreeData( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one Verilog module.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseModule( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    char * pWord;
+    int RetValue;
+    char Symbol;
+
+    // start the current network
+    assert( pMan->pNtkCur == NULL );
+    pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX );
+//    pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BDD );
+
+    // get the network name
+    pWord = Ver_ParseGetName( pMan );
+    pNtk->pName = Extra_UtilStrsav( pWord );
+    pNtk->pSpec = Extra_UtilStrsav( pMan->pFileName );
+
+    // create constant nodes and nets
+    Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
+    Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
+    Ver_ParseCreateConst( pNtk, "1'b0", 0 );
+    Ver_ParseCreateConst( pNtk, "1'b1", 1 );
+
+    // make sure we stopped at the opening paranthesis
+    if ( Ver_StreamScanChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // skip to the end of parantheses
+    while ( 1 )
+    {
+        Ver_StreamSkipToChars( p, ",/)" );
+        while ( Ver_StreamScanChar(p) == '/' )
+        {
+            Ver_ParseSkipComments( pMan );
+            Ver_StreamSkipToChars( p, ",/)" );
+        }
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol== ')' )
+            break;
+    }
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return 0;
+    Symbol = Ver_StreamPopChar(p);
+    assert( Symbol == ';' );
+
+    // parse the inputs/outputs/registers/wires/inouts
+    while ( 1 )
+    {
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        if ( !strcmp( pWord, "input" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_INPUT );
+        else if ( !strcmp( pWord, "output" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT );
+        else if ( !strcmp( pWord, "reg" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_REG );
+        else if ( !strcmp( pWord, "wire" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE );
+        else if ( !strcmp( pWord, "inout" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_INOUT );
+        else 
+            break;
+        if ( RetValue == 0 )
+            return 0;
+    }
+
+    // parse the remaining statements
+    while ( 1 )
+    {
+        Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
+        if ( !strcmp( pWord, "assign" ) )
+            RetValue = Ver_ParseAssign( pMan );
+        else if ( !strcmp( pWord, "always" ) )
+            RetValue = Ver_ParseAlways( pMan );
+        else if ( !strcmp( pWord, "initial" ) )
+            RetValue = Ver_ParseInitial( pMan );
+        else if ( !strcmp( pWord, "endmodule" ) )
+        {
+            // if nothing is known, set the functionality to be black box
+            Abc_NtkFinalizeRead( pNtk );
+            break;
+        }
+        else if ( pMan->pGateLib && st_lookup(pMan->pGateLib, pWord, (char**)&pNtkTemp) ) // gate library
+            RetValue = Ver_ParseGate( pMan, pNtkTemp );
+        else if ( pMan->pLibrary && st_lookup(pMan->pLibrary, pWord, (char**)&pNtkTemp) ) // current design
+            RetValue = Ver_ParseGate( pMan, pNtkTemp );
+        else
+        {
+            printf( "Cannot find \"%s\".\n", pWord );
+            Ver_StreamSkipToChars( p, ";" );
+            Ver_StreamPopChar(p);
+
+//            sprintf( pMan->sError, "Cannot find \"%s\" in the library.", pWord );
+//            Ver_ParsePrintErrorMessage( pMan );
+//            return 0;
+        }
+        if ( RetValue == 0 )
+            return 0;
+        // get new word
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+    }
+
+    if ( pNtk->ntkFunc == ABC_FUNC_BDD )
+    {
+        Abc_Obj_t * pObj;
+        pObj = Abc_ObjFanin0( Abc_NtkFindNet( pNtk, "1'b0" ) );
+        pObj->pData = Cudd_ReadLogicZero( pNtk->pManFunc );
+        pObj = Abc_ObjFanin0( Abc_NtkFindNet( pNtk, "1'b1" ) );
+        pObj->pData = Cudd_ReadOne( pNtk->pManFunc );
+        Cudd_Ref( Cudd_ReadOne( pNtk->pManFunc ) );
+        Cudd_Ref( Cudd_ReadOne( pNtk->pManFunc ) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    char * pWord;
+    char Symbol;
+    while ( 1 )
+    {
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
+            Ver_ParseCreatePi( pNtk, pWord );
+        if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
+            Ver_ParseCreatePo( pNtk, pWord );
+        if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
+            Abc_NtkFindOrCreateNet( pNtk, pWord );
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ',' )
+            continue;
+        if ( Symbol == ';' )
+            return 1;
+        break;
+    }
+    sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." );
+    Ver_ParsePrintErrorMessage( pMan );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseAssign( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNode, * pNet;
+    char * pWord, * pName, * pEquation;
+    DdNode * bFunc;
+    char Symbol;
+    int i, Length;
+
+    // convert from the mapped netlist into the BDD netlist
+    if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+    {
+        pNtk->ntkFunc = ABC_FUNC_BDD;
+        pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    }
+    else if ( pNtk->ntkFunc != ABC_FUNC_BDD )
+    {
+        sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    while ( 1 )
+    {
+        // get the name of the output signal
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // get the fanout net
+        pNet = Abc_NtkFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // get the equal sign
+        if ( Ver_StreamPopChar(p) != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get the second name
+        pEquation = Ver_StreamGetWord( p, ",;" );
+        if ( pEquation == NULL )
+            return 0;
+
+        // parse the formula
+        bFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
+        if ( bFunc == NULL )
+        {
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Cudd_Ref( bFunc );
+        // create the node with the given inputs
+        pNode = Abc_NtkCreateNode( pMan->pNtkCur );
+        pNode->pData = bFunc;
+        Abc_ObjAddFanin( pNet, pNode );
+        // connect to fanin nets
+        for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
+        {
+            // get the name of this signal
+            Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
+            pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
+            pName[Length] = 0;
+            // find the corresponding net
+            pNet = Abc_NtkFindNet( pNtk, pName );
+            if ( pNet == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            Abc_ObjAddFanin( pNode, pNet );
+        }
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ',' )
+            continue;
+        if ( Symbol == ';' )
+            return 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseAlways( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNet, * pNet2;
+    char * pWord, * pWord2;
+    char Symbol;
+    // parse the directive 
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    if ( strcmp( pWord, "begin" ) )
+    {
+        sprintf( pMan->sError, "Cannot parse the always statement (expected \"begin\")." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // iterate over the initial states
+    while ( 1 )
+    {
+        // get the name of the output signal
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // look for the end of directive
+        if ( !strcmp( pWord, "end" ) )
+            break;
+        // get the fanout net
+        pNet = Abc_NtkFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // get the equal sign
+        if ( Ver_StreamPopChar(p) != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the always statement for %s (expected equality sign).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get the second name
+        pWord2 = Ver_ParseGetName( pMan );
+        if ( pWord2 == NULL )
+            return 0;
+        // get the fanin net
+        pNet2 = Abc_NtkFindNet( pNtk, pWord2 );
+        if ( pNet2 == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // create the latch
+        Ver_ParseCreateLatch( pNtk, pNet2->pData, pNet->pData );
+        // remove the last symbol
+        Symbol = Ver_StreamPopChar(p);
+        assert( Symbol == ';' );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseInitial( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNode, * pNet;
+    char * pWord, * pEquation;
+    char Symbol;
+    // parse the directive 
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    if ( strcmp( pWord, "begin" ) )
+    {
+        sprintf( pMan->sError, "Cannot parse the initial statement (expected \"begin\")." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // iterate over the initial states
+    while ( 1 )
+    {
+        // get the name of the output signal
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // look for the end of directive
+        if ( !strcmp( pWord, "end" ) )
+            break;
+        // get the fanout net
+        pNet = Abc_NtkFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // get the equal sign
+        if ( Ver_StreamPopChar(p) != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the initial statement for %s (expected equality sign).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get the second name
+        pEquation = Ver_StreamGetWord( p, ";" );
+        if ( pEquation == NULL )
+            return 0;
+        // find the corresponding latch
+        pNode = Abc_ObjFanin0(pNet);
+        assert( Abc_ObjIsLatch(pNode) );
+        // set the initial state
+        if ( pEquation[0] == '2' )
+            Abc_LatchSetInitDc( pNode );
+        else if ( pEquation[0] == '1')
+            Abc_LatchSetInit1( pNode );
+        else if ( pEquation[0] == '0' )
+            Abc_LatchSetInit0( pNode );
+        else
+        {
+            sprintf( pMan->sError, "Incorrect initial value of the latch %s (expected equality sign).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // remove the last symbol
+        Symbol = Ver_StreamPopChar(p);
+        assert( Symbol == ';' );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNetFormal, * pNetActual;
+    Abc_Obj_t * pObj, * pNode;
+    char * pWord, Symbol;
+    int i, fCompl;
+
+    // convert from the mapped netlist into the BDD netlist
+    if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+    {
+        pNtk->ntkFunc = ABC_FUNC_MAP;
+        pNtk->pManFunc = pMan->pGateLib;
+    }
+    else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
+    {
+        sprintf( pMan->sError, "The network %s appears to contain both mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // clean the PI/PO pointers
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+        pObj->pCopy = NULL;
+    // parse the directive and set the pointers to the PIs/POs of the gate
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // parse pairs of formal/actural inputs
+    while ( 1 )
+    {
+        // process one pair of formal/actual parameters
+        if ( Ver_StreamPopChar(p) != '.' )
+        {
+            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the formal name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // get the formal net
+        if ( Abc_NtkIsNetlist(pNtkGate) )
+            pNetFormal = Abc_NtkFindNet( pNtkGate, pWord );
+        else // if ( Abc_NtkIsStrash(pNtkGate) )
+            pNetFormal = Abc_NtkFindTerm( pNtkGate, pWord );
+        if ( pNetFormal == NULL )
+        {
+            sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // open the paranthesis
+        if ( Ver_StreamPopChar(p) != '(' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the actual name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // check if the name is complemented
+        fCompl = (pWord[0] == '~');
+        if ( fCompl )
+            pWord++;
+        // get the actual net
+        pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord );
+        if ( pNetActual == NULL )
+        {
+            sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // close the paranthesis
+        if ( Ver_StreamPopChar(p) != ')' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // process the pair
+        if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) )  // PI net
+            Abc_ObjFanin0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
+        else if ( Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) )  // P0 net
+        {
+            assert( fCompl == 0 );
+            Abc_ObjFanout0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
+        }
+        else
+        {
+            sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // check if it is the end of gate
+        Ver_ParseSkipComments( pMan );
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ')' )
+            break;
+        // skip comma
+        if ( Symbol != ',' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Ver_ParseSkipComments( pMan );
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // make sure each input net is driven
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+        if ( pObj->pCopy == NULL )
+        {
+            sprintf( pMan->sError, "Formal input %s of gate %s has no actual input.", Abc_ObjFanout0(pObj)->pData, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+/*
+    // make sure each output net is driving something
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+        if ( pObj->pCopy == NULL )
+        {
+            sprintf( pMan->sError, "Formal output %s of gate %s has no actual output.", Abc_ObjFanin0(pObj)->pData, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+*/
+    // create a new node 
+    pNode = Abc_NtkCreateNode( pMan->pNtkCur );
+    // connect to fanin nets
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+        Abc_ObjAddFanin( pNode, pObj->pCopy );
+    // connect to fanout nets
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+        if ( pObj->pCopy )
+            Abc_ObjAddFanin( pObj->pCopy, pNode );
+    // set the functionality
+    pNode->pData = pNtkGate;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates PI terminal and net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet, * pTerm;
+    // get the PI net
+    pNet  = Abc_NtkFindNet( pNtk, pName );
+    if ( pNet )
+        printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
+    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
+    // add the PI node
+    pTerm = Abc_NtkCreatePi( pNtk );
+    Abc_ObjAddFanin( pNet, pTerm );
+    return pTerm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates PO terminal and net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet, * pTerm;
+    // get the PO net
+    pNet  = Abc_NtkFindNet( pNtk, pName );
+    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
+        printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
+    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
+    // add the PO node
+    pTerm = Abc_NtkCreatePo( pNtk );
+    Abc_ObjAddFanin( pTerm, pNet );
+    return pTerm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create a constant 0 node driving the net with this name.]
+
+  Description [Assumes that the net already exists.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 )
+{
+    Abc_Obj_t * pNet, * pTerm;
+    pTerm = fConst1? Abc_NodeCreateConst1(pNtk) : Abc_NodeCreateConst0(pNtk);
+    pNet  = Abc_NtkFindNet(pNtk, pName);    assert( pNet );
+    Abc_ObjAddFanin( pNet, pTerm );
+    return pTerm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create a latch with the given input/output.]
+
+  Description [By default, the latch value is unknown (ABC_INIT_NONE).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO )
+{
+    Abc_Obj_t * pLatch, * pNet;
+    // create a new latch and add it to the network
+    pLatch = Abc_NtkCreateLatch( pNtk );
+    // get the LI net
+    pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI );
+    Abc_ObjAddFanin( pLatch, pNet );
+    // get the LO net
+    pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO );
+    Abc_ObjAddFanin( pNet, pLatch );
+    return pLatch;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c
new file mode 100644
index 00000000..7edb5bd9
--- /dev/null
+++ b/src/temp/ver/verFormula.c
@@ -0,0 +1,408 @@
+/**CFile****************************************************************
+
+  FileName    [verFormula.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Formula parser to read Verilog assign statements.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the list of operation symbols to be used in expressions
+#define VER_PARSE_SYM_OPEN    '('   // opening paranthesis
+#define VER_PARSE_SYM_CLOSE   ')'   // closing paranthesis
+#define VER_PARSE_SYM_CONST0  '0'   // constant 0
+#define VER_PARSE_SYM_CONST1  '1'   // constant 1
+#define VER_PARSE_SYM_NEGBEF1 '!'   // negation before the variable
+#define VER_PARSE_SYM_NEGBEF2 '~'   // negation before the variable
+#define VER_PARSE_SYM_AND     '&'   // logic AND
+#define VER_PARSE_SYM_OR      '|'   // logic OR
+#define VER_PARSE_SYM_XOR     '^'   // logic XOR
+#define VER_PARSE_SYM_MUX1    '?'   // first symbol of MUX
+#define VER_PARSE_SYM_MUX2    ':'   // second symbol of MUX
+
+// the list of opcodes (also specifying operation precedence)
+#define VER_PARSE_OPER_NEG    10    // negation
+#define VER_PARSE_OPER_AND     9    // logic AND
+#define VER_PARSE_OPER_XOR     8    // logic EXOR   (a'b | ab')   
+#define VER_PARSE_OPER_OR      7    // logic OR
+#define VER_PARSE_OPER_EQU     6    // equvalence   (a'b'| ab )
+#define VER_PARSE_OPER_MUX     5    // MUX          (a'b | ac )
+#define VER_PARSE_OPER_MARK    1    // OpStack token standing for an opening paranthesis
+
+// these are values of the internal Flag
+#define VER_PARSE_FLAG_START   1    // after the opening parenthesis 
+#define VER_PARSE_FLAG_VAR     2    // after operation is received
+#define VER_PARSE_FLAG_OPER    3    // after operation symbol is received
+#define VER_PARSE_FLAG_OPERMUX 4    // after operation symbol is received
+#define VER_PARSE_FLAG_ERROR   5    // when error is detected
+
+static DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper );
+static int      Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Parser of the formula encountered in assign statements.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
+{
+    DdNode * bFunc, * bTemp;
+    char * pTemp;
+    int nParans, Flag;
+    int Oper, Oper1, Oper2;
+    int v;
+
+    // clear the stacks and the names
+    Vec_PtrClear( vNames );
+    Vec_PtrClear( vStackFn );
+    Vec_IntClear( vStackOp );
+
+    // make sure that the number of opening and closing parantheses is the same
+    nParans = 0;
+    for ( pTemp = pFormula; *pTemp; pTemp++ )
+        if ( *pTemp == '(' )
+            nParans++;
+        else if ( *pTemp == ')' )
+            nParans--;
+    if ( nParans != 0 )
+    {
+        sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parantheses ()." );
+        return NULL;
+    }
+
+    // add parantheses
+    pTemp = pFormula + strlen(pFormula) + 2;
+    *pTemp-- = 0; *pTemp = ')';
+    while ( --pTemp != pFormula )
+        *pTemp = *(pTemp - 1);
+    *pTemp = '(';
+
+    // perform parsing
+    Flag = VER_PARSE_FLAG_START;
+    for ( pTemp = pFormula; *pTemp; pTemp++ )
+    {
+        switch ( *pTemp )
+        {
+        // skip all spaces, tabs, and end-of-lines
+        case ' ':
+        case '\t':
+        case '\r':
+        case '\n':
+        case '\\': // skip name opening statement
+            continue;
+
+        // treat Constant 0 as a variable
+        case VER_PARSE_SYM_CONST0:
+            Vec_PtrPush( vStackFn, b0 );   Cudd_Ref( b0 );
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Flag = VER_PARSE_FLAG_VAR; 
+            break;
+
+        // the same for Constant 1
+        case VER_PARSE_SYM_CONST1:
+            Vec_PtrPush( vStackFn, b1 );    Cudd_Ref( b1 );
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Flag = VER_PARSE_FLAG_VAR; 
+            break;
+
+        case VER_PARSE_SYM_NEGBEF1:
+        case VER_PARSE_SYM_NEGBEF2:
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {// if NEGBEF follows a variable, AND is assumed
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG );
+            break;
+
+        case VER_PARSE_SYM_AND:
+        case VER_PARSE_SYM_OR:
+        case VER_PARSE_SYM_XOR:
+        case VER_PARSE_SYM_MUX1:
+        case VER_PARSE_SYM_MUX2:
+            if ( Flag != VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            if ( *pTemp == VER_PARSE_SYM_AND )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_AND );
+            else if ( *pTemp == VER_PARSE_SYM_OR )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_OR );
+            else if ( *pTemp == VER_PARSE_SYM_XOR )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR );
+            else if ( *pTemp == VER_PARSE_SYM_MUX1 )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
+//            else if ( *pTemp == VER_PARSE_SYM_MUX2 )
+//                Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
+            Flag = VER_PARSE_FLAG_OPER; 
+            break;
+
+        case VER_PARSE_SYM_OPEN:
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a paranthesis." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK );
+            // after an opening bracket, it feels like starting over again
+            Flag = VER_PARSE_FLAG_START; 
+            break;
+
+        case VER_PARSE_SYM_CLOSE:
+            if ( Vec_IntSize( vStackOp ) )
+            {
+                while ( 1 )
+                {
+                    if ( !Vec_IntSize( vStackOp ) )
+                    {
+                        sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
+                        Flag = VER_PARSE_FLAG_ERROR; 
+                        break;
+                    }
+                    Oper = Vec_IntPop( vStackOp );
+                    if ( Oper == VER_PARSE_OPER_MARK )
+                        break;
+                    // skip the second MUX operation
+//                    if ( Oper == VER_PARSE_OPER_MUX2 )
+//                    {
+//                        Oper = Vec_IntPop( vStackOp );
+//                        assert( Oper == VER_PARSE_OPER_MUX1 );
+//                    }
+
+                    // perform the given operation
+                    if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper ) == NULL )
+                    {
+                        sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
+                        return NULL;
+                    }
+                }
+            }
+            else
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            if ( Flag != VER_PARSE_FLAG_ERROR )
+                Flag = VER_PARSE_FLAG_VAR; 
+            break;
+
+
+        default:
+            // scan the next name
+            v = Ver_FormulaParserFindVar( pTemp, vNames );
+            pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1;
+
+            // assume operation AND, if vars follow one another
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." );
+                return NULL;
+            }
+            bTemp = Cudd_bddIthVar(dd, v);
+            Vec_PtrPush( vStackFn, bTemp );  Cudd_Ref( bTemp );
+            Flag = VER_PARSE_FLAG_VAR; 
+            break;
+        }
+
+        if ( Flag == VER_PARSE_FLAG_ERROR )
+            break;      // error exit
+        else if ( Flag == VER_PARSE_FLAG_START )
+            continue;  //  go on parsing
+        else if ( Flag == VER_PARSE_FLAG_VAR )
+            while ( 1 )
+            {  // check if there are negations in the OpStack     
+                if ( !Vec_IntSize(vStackOp) )
+                    break;
+                Oper = Vec_IntPop( vStackOp );
+                if ( Oper != VER_PARSE_OPER_NEG )
+                {
+                    Vec_IntPush( vStackOp, Oper );
+                    break;
+                }
+                else
+                {
+                      Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) );
+                }
+            }
+        else // if ( Flag == VER_PARSE_FLAG_OPER )
+            while ( 1 )
+            {  // execute all the operations in the OpStack
+               // with precedence higher or equal than the last one
+                Oper1 = Vec_IntPop( vStackOp ); // the last operation
+                if ( !Vec_IntSize(vStackOp) ) 
+                {  // if it is the only operation, push it back
+                    Vec_IntPush( vStackOp, Oper1 );
+                    break;
+                }
+                Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
+                if ( Oper2 >= Oper1 )  
+                {  // if Oper2 precedence is higher or equal, execute it
+                    if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper2 ) == NULL )
+                    {
+                        sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
+                        return NULL;
+                    }
+                    Vec_IntPush( vStackOp,  Oper1 );     // push the last operation back
+                }
+                else
+                {  // if Oper2 precedence is lower, push them back and done
+                    Vec_IntPush( vStackOp, Oper2 );
+                    Vec_IntPush( vStackOp, Oper1 );
+                    break;
+                }
+            }
+    }
+
+    if ( Flag != VER_PARSE_FLAG_ERROR )
+    {
+        if ( Vec_PtrSize(vStackFn) )
+        {    
+            bFunc = Vec_PtrPop(vStackFn);
+            if ( !Vec_PtrSize(vStackFn) )
+                if ( !Vec_IntSize(vStackOp) )
+                {
+                    Cudd_Deref( bFunc );
+                    return bFunc;
+                }
+                else
+                    sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" );
+            else
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" );
+        }
+        else
+            sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" );
+    }
+    Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the operation on the top entries in the stack.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper )
+{
+    DdNode * bArg0, * bArg1, * bArg2, * bFunc;
+    // perform the given operation
+    bArg2 = Vec_PtrPop( vStackFn );
+    bArg1 = Vec_PtrPop( vStackFn );
+    if ( Oper == VER_PARSE_OPER_AND )
+        bFunc = Cudd_bddAnd( dd, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_XOR )
+        bFunc = Cudd_bddXor( dd, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_OR )
+        bFunc = Cudd_bddOr( dd, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_EQU )
+        bFunc = Cudd_bddXnor( dd, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_MUX )
+    {
+        bArg0 = Vec_PtrPop( vStackFn );
+        bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 );  Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bArg0 );
+        Cudd_Deref( bFunc );
+    }
+    else
+        return NULL;
+    Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bArg1 );
+    Cudd_RecursiveDeref( dd, bArg2 );
+    Vec_PtrPush( vStackFn,  bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the new variable found.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
+{
+    char * pTemp, * pTemp2;
+    int nLength, nLength2, i;
+    // find the end of the string delimited by other characters
+    pTemp = pString;
+    while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && 
+            *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && 
+            *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && 
+            *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && 
+            *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
+            pTemp++;
+    // look for this string in the array
+    nLength = pTemp - pString;
+    for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
+    {
+        nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 );
+        if ( nLength2 != nLength )
+            continue;
+        pTemp2   = Vec_PtrEntry( vNames, 2*i + 1 );
+        if ( strncmp( pTemp, pTemp2, nLength ) )
+            continue;
+        return i;
+    }
+    // could not find - add and return the number
+    Vec_PtrPush( vNames, (void *)nLength );
+    Vec_PtrPush( vNames, pString );
+    return i;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ver/verParse.c b/src/temp/ver/verParse.c
new file mode 100644
index 00000000..c8497932
--- /dev/null
+++ b/src/temp/ver/verParse.c
@@ -0,0 +1,111 @@
+/**CFile****************************************************************
+
+  FileName    [verParse.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Performs some Verilog parsing tasks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verParse.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Skips the comments of they are present.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSkipComments( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    char Symbol;
+    // skip spaces
+    Ver_StreamSkipChars( p, " \t\n\r" );
+    if ( !Ver_StreamIsOkey(pMan->pReader) )
+        return 1;
+    // read the first symbol
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol != '/' )
+        return 1;
+    Ver_StreamPopChar( p );
+    // read the second symbol
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol == '/' )
+    { // skip till the end of line
+        Ver_StreamSkipToChars( p, "\n" );
+        return Ver_ParseSkipComments( pMan );
+    }
+    if ( Symbol == '*' )
+    { // skip till the next occurance of */
+        Ver_StreamPopChar( p );
+        do {
+            Ver_StreamSkipToChars( p, "*" );
+            Ver_StreamPopChar( p );
+        } while ( Ver_StreamScanChar( p ) != '/' );
+        Ver_StreamPopChar( p );
+        return Ver_ParseSkipComments( pMan );
+    }
+    sprintf( pMan->sError, "Cannot parse after symbol \"/\"." );
+    Ver_ParsePrintErrorMessage( pMan );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses a Verilog name that can be being with a slash.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ver_ParseGetName( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    char Symbol;
+    char * pWord;
+    if ( !Ver_StreamIsOkey(p) )
+        return NULL;
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return NULL;
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol == '\\' )
+        Ver_StreamPopChar( p );
+    pWord = Ver_StreamGetWord( p, " \t\n\r(),;" );
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return NULL;
+    return pWord;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ver/verStream.c b/src/temp/ver/verStream.c
new file mode 100644
index 00000000..7956b13c
--- /dev/null
+++ b/src/temp/ver/verStream.c
@@ -0,0 +1,435 @@
+/**CFile****************************************************************
+
+  FileName    [verStream.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Input file stream, which knows nothing about Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verStream.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define VER_BUFFER_SIZE        1048576    // 1M   - size of the data chunk stored in memory
+#define VER_OFFSET_SIZE           4096    // 4K   - load new data when less than this is left
+#define VER_WORD_SIZE             4096    // 4K   - the largest token that can be returned
+
+#define VER_MINIMUM(a,b)       (((a) < (b))? (a) : (b))
+
+struct Ver_Stream_t_
+{
+    // the input file
+    char *           pFileName;     // the input file name
+    FILE *           pFile;         // the input file pointer
+    int              nFileSize;     // the total number of bytes in the file
+    int              nFileRead;     // the number of bytes currently read from file
+    int              nLineCounter;  // the counter of lines processed
+    // temporary storage for data 
+    char *           pBuffer;       // the buffer
+    int              nBufferSize;   // the size of the buffer
+    char *           pBufferCur;    // the current reading position
+    char *           pBufferEnd;    // the first position not used by currently loaded data
+    char *           pBufferStop;   // the position where loading new data will be done
+    // tokens given to the user
+    char             pChars[VER_WORD_SIZE+5]; // temporary storage for a word (plus end-of-string and two parantheses)
+    int              nChars;        // the total number of characters in the word
+    // status of the parser
+    int              fStop;         // this flag goes high when the end of file is reached
+};
+
+static void Ver_StreamReload( Ver_Stream_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the file reader for the given file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ver_Stream_t * Ver_StreamAlloc( char * pFileName )
+{
+    Ver_Stream_t * p;
+    FILE * pFile;
+    int nCharsToRead;
+    // check if the file can be opened
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Ver_StreamAlloc(): Cannot open input file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    // start the file reader    
+    p = ALLOC( Ver_Stream_t, 1 );
+    memset( p, 0, sizeof(Ver_Stream_t) );
+    p->pFileName   = pFileName;
+    p->pFile       = pFile;
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    p->nFileSize = ftell( pFile );  
+    rewind( pFile ); 
+    // allocate the buffer
+    p->pBuffer = ALLOC( char, VER_BUFFER_SIZE+1 );
+    p->nBufferSize = VER_BUFFER_SIZE;
+    p->pBufferCur  = p->pBuffer;
+    // determine how many chars to read
+    nCharsToRead = VER_MINIMUM(p->nFileSize, VER_BUFFER_SIZE);
+    // load the first part into the buffer
+    fread( p->pBuffer, nCharsToRead, 1, p->pFile );
+    p->nFileRead = nCharsToRead;
+    // set the ponters to the end and the stopping point
+    p->pBufferEnd  = p->pBuffer + nCharsToRead;
+    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE;
+    // start the arrays
+    p->nLineCounter = 1; // 1-based line counting
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads new data into the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamReload( Ver_Stream_t * p )
+{
+    int nCharsUsed, nCharsToRead;
+    assert( !p->fStop );
+    assert( p->pBufferCur > p->pBufferStop );
+    assert( p->pBufferCur < p->pBufferEnd );
+    // figure out how many chars are still not processed
+    nCharsUsed = p->pBufferEnd - p->pBufferCur;
+    // move the remaining data to the beginning of the buffer
+    memmove( p->pBuffer, p->pBufferCur, nCharsUsed );
+    p->pBufferCur = p->pBuffer;
+    // determine how many chars we will read
+    nCharsToRead = VER_MINIMUM( p->nBufferSize - nCharsUsed, p->nFileSize - p->nFileRead );
+    // read the chars
+    fread( p->pBuffer + nCharsUsed, nCharsToRead, 1, p->pFile );
+    p->nFileRead += nCharsToRead;
+    // set the ponters to the end and the stopping point
+    p->pBufferEnd  = p->pBuffer + nCharsUsed + nCharsToRead;
+    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamFree( Ver_Stream_t * p )
+{
+    if ( p->pFile )
+        fclose( p->pFile );
+    FREE( p->pBuffer );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ver_StreamGetFileName( Ver_Stream_t * p )
+{
+    return p->pFileName;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamGetFileSize( Ver_Stream_t * p )
+{
+    return p->nFileSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the current reading position.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamGetCurPosition( Ver_Stream_t * p )
+{
+    return p->nFileRead - (p->pBufferEnd - p->pBufferCur);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the line number for the given token.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamGetLineNumber( Ver_Stream_t * p )
+{
+    return p->nLineCounter;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamIsOkey( Ver_Stream_t * p )
+{
+    return !p->fStop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char Ver_StreamScanChar( Ver_Stream_t * p )
+{
+    assert( !p->fStop );
+    return *p->pBufferCur;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current symbol and moves to the next.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char Ver_StreamPopChar( Ver_Stream_t * p )
+{
+    assert( !p->fStop );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // check if there are symbols left
+    if ( p->pBufferCur == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return -1;
+    }
+    return *p->pBufferCur++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips the current symbol and all symbols from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip )
+{
+    char * pChar, * pTemp;
+    assert( !p->fStop );
+    assert( pCharsToSkip != NULL );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // skip the symbols
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // skip symbols as long as they are in the list
+        for ( pTemp = pCharsToSkip; *pTemp; pTemp++ )
+            if ( *pChar == *pTemp )
+                break;
+        if ( *pTemp == 0 ) // pChar is not found in the list
+        {
+            p->pBufferCur = pChar;
+            return;
+        }
+    }
+    // the file is finished or the last part continued 
+    // through VER_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return;
+    }
+    printf( "Ver_StreamSkipSymbol() failed to parse the file \"%s\".\n", p->pFileName );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips all symbols until encountering one from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop )
+{
+    char * pChar, * pTemp;
+    assert( !p->fStop );
+    assert( pCharsToStop != NULL );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // skip the symbols
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // skip symbols as long as they are NOT in the list
+        for ( pTemp = pCharsToStop; *pTemp; pTemp++ )
+            if ( *pChar == *pTemp )
+                break;
+        if ( *pTemp == 0 ) // pChar is not found in the list
+            continue;
+        // the symbol is found - move position and return
+        p->pBufferCur = pChar;
+        return;
+    }
+    // the file is finished or the last part continued 
+    // through VER_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return;
+    }
+    printf( "Ver_StreamSkipToSymbol() failed to parse the file \"%s\".\n", p->pFileName );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current word delimited by the set of symbols.]
+
+  Description [Modifies the stream by inserting 0 at the first encounter
+  of one of the symbols in the list.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop )
+{
+    char * pChar, * pTemp;
+    if ( p->fStop )
+        return NULL;
+    assert( pCharsToStop != NULL );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // skip the symbols
+    p->nChars = 0;
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // skip symbols as long as they are NOT in the list
+        for ( pTemp = pCharsToStop; *pTemp; pTemp++ )
+            if ( *pChar == *pTemp )
+                break;
+        if ( *pTemp == 0 ) // pChar is not found in the list
+        {
+            p->pChars[p->nChars++] = *pChar;
+            if ( p->nChars == VER_WORD_SIZE )
+                return NULL;
+            continue;
+        }
+        // the symbol is found - move the position, set the word end, return the word
+        p->pBufferCur = pChar;
+        p->pChars[p->nChars] = 0;
+        return p->pChars;
+    }
+    // the file is finished or the last part continued 
+    // through VER_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        p->pChars[p->nChars] = 0;
+        return p->pChars;
+    }
+    printf( "Ver_StreamGetWord() failed to parse the file \"%s\".\n", p->pFileName );
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ver/verWords.c b/src/temp/ver/verWords.c
new file mode 100644
index 00000000..f9d27010
--- /dev/null
+++ b/src/temp/ver/verWords.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [verWords.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Handles keywords that are currently supported.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verWords.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ver/ver_.c b/src/temp/ver/ver_.c
new file mode 100644
index 00000000..76599dac
--- /dev/null
+++ b/src/temp/ver/ver_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [ver_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of structural Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: ver_.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+