Version abc60820

19 files changed, 3032 insertions, 111 deletions

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                                ///
+////////////////////////////////////////////////////////////////////////
+
+