Version abc60820

22 files changed, 1003 insertions, 119 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 03f5a66f..8bd48874 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -462,6 +462,7 @@ extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
@@ -503,6 +504,7 @@ extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
+extern void               Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
@@ -519,6 +521,7 @@ extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkCreateBox( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 79669657..8448578e 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -256,6 +256,37 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    // go through the PO nodes and call for each of them
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_NtkNodeSupport_rec( Abc_ObjFanin0(pNode), vNodes );
+    // add unused CIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        if ( !Abc_NodeIsTravIdCurrent( pNode ) )
+            Vec_PtrPush( vNodes, pNode );
+    assert( Vec_PtrSize(vNodes) == Abc_NtkCiNum(pNtk) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of CI nodes in the support of the given nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
 {
     Vec_Ptr_t * vNodes;
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 7d4460bf..f9e529c7 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -54,10 +54,10 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     if ( pNtk->tName2Model )
         return Abc_NtkNetlistToLogicHie( pNtk );
     // start the network
-    if ( !Abc_NtkHasMapping(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
-    else
+    if ( Abc_NtkHasMapping(pNtk) )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
+    else
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc );
     // duplicate the nodes 
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index b8c0462d..1a07ebf2 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     }
     else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen();
-    else
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     // allocate constant node
     if ( !Abc_NtkIsNetlist(pNtk) )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index d993ca65..337ba428 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -409,6 +409,29 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the net with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet;
+    int ObjId;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL );
+    if ( ObjId == -1 )
+        return NULL;
+    pNet = Abc_NtkObj( pNtk, ObjId );
+    return pNet;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finds or creates the net.]
 
   Description []
@@ -568,7 +591,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen());
-    else
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     return pNode;
 }
@@ -596,7 +619,7 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen());
-    else
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     return pNode;
 }
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index ed76f396..bb0606f7 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -30,7 +30,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Abc_ShowFile( char * FileNameDot );
+extern void Abc_ShowFile( char * FileNameDot );
 static void Abc_ShowGetFileName( char * pName, char * pBuffer );
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index afa91c45..f756ef89 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -251,7 +251,12 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk )
     TotalArea = 0.0;
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        assert( pNode->pData );
+//        assert( pNode->pData );
+        if ( pNode->pData == NULL )
+        {
+            printf( "Node without mapping is encountered.\n" );
+            continue;
+        }
         TotalArea += Mio_GateReadArea( pNode->pData );
     }
     return TotalArea;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f3dbe357..c1327f43 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -74,6 +74,7 @@ static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReorder        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrder          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOneOutput      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -192,6 +193,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "reorder",       Abc_CommandReorder,          0 );
+    Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandOneOutput,        1 );
@@ -1627,6 +1629,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
+    int fVerbose;
     int fBddSizeMax;
     int fDualRail;
     int fReorder;
@@ -1637,11 +1640,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fVerbose = 1;
     fReorder = 1;
     fDualRail = 0;
-    fBddSizeMax = 1000000;
+    fBddSizeMax = 50000000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Brdh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Brdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1659,6 +1663,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDualRail ^= 1;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'r':
             fReorder ^= 1;
             break;
@@ -1683,11 +1690,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0 );
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -1700,11 +1707,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: collapse [-B num] [-rdh]\n" );
+    fprintf( pErr, "usage: collapse [-B num] [-rdvh]\n" );
     fprintf( pErr, "\t          collapses the network by constructing global BDDs\n" );
     fprintf( pErr, "\t-B num  : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
     fprintf( pErr, "\t-r      : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
     fprintf( pErr, "\t-d      : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
+    fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
 }
@@ -3462,6 +3470,93 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int c;
+    int fReverse;
+    int fVerbose;
+    extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
+    extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fReverse = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'r':
+            fReverse ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+//    if ( Abc_NtkLatchNum(pNtk) > 0 )
+//    {
+//        printf( "Currently this procedure does not work for sequential networks.\n" );
+//        return 1;
+//    }
+
+    // if the var order file is given, implement this order
+    pFileName = NULL;
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pFileName = argv[globalUtilOptind];
+        pFile = fopen( pFileName, "r" );
+        if ( pFile == NULL )
+        {
+            fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
+            return 1;
+        }
+        fclose( pFile );
+    }
+    if ( pFileName )
+        Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
+    else
+        Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: order [-rvh] <file>\n" );
+    fprintf( pErr, "\t         computes a good static CI variable order\n" );
+    fprintf( pErr, "\t-r     : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );  
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4583,7 +4678,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // run the command
 //    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+//    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5105,21 +5201,36 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUpdateLevel, fVerbose;
-    extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose );
+    int c, fUseZeroCost, fVerbose, nIters;
+    extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUpdateLevel = 1;
+    nIters       = 3;
+    fUseZeroCost = 1;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "zvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIters < 0 ) 
+                goto usage;
+            break;
+        case 'z':
+            fUseZeroCost ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5140,7 +5251,7 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyHaig( pNtk, fVerbose );
+    pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5151,9 +5262,10 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: haig [-vh]\n" );
-    fprintf( pErr, "\t         prints HAIG stats after one round of sequential rewriting\n" );
-//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "usage: haig [-Izvh]\n" );
+    fprintf( pErr, "\t         prints HAIG stats after sequential rewriting\n" );
+    fprintf( pErr, "\t-I num : the number of rewriting iterations [default = %d]\n", nIters );
+    fprintf( pErr, "\t-z     : toggle zero-cost replacements [default = %s]\n", fUseZeroCost? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index eed18e1b..1de087e8 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -46,14 +46,17 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
 Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
+    int clk = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
-
     // compute the global BDDs
     if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+    {
+        printf( "The shared BDD size is %d nodes.  ", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+        PRT( "BDD construction time", clock() - clk );
+    }
 
     // create the new network
     if ( fDualRail )
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 7d5ed6ec..42d5173a 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
-static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
 static Ivy_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
 
 static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
@@ -120,17 +120,17 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq )
+Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig )
 {
     Abc_Ntk_t * pNtkAig;
     int nNodes, fCleanup = 1;
     // convert from the AIG manager
     if ( fSeq )
-        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
+        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig );
     else
         pNtkAig = Abc_NtkFromAig( pNtk, pMan );
     // report the cleanup results
-    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+    if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
         printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
@@ -163,11 +163,11 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
     pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
     if ( pMan == NULL )
         return NULL;
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
@@ -179,21 +179,28 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
+    int i;
+
     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
     if ( pMan == NULL )
         return NULL;
 
-    Ivy_ManHaigStart( pMan );
-    Ivy_ManRewriteSeq( pMan, 0, fVerbose );
-    Ivy_ManHaigPrintStats( pMan );
-    Ivy_ManHaigStop( pMan );
+    Ivy_ManHaigStart( pMan, fVerbose );
+    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    for ( i = 1; i < nIters; i++ )
+        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+    Ivy_ManHaigPostprocess( pMan, fVerbose );
+
+    // write working AIG into the current network
+//    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 
+    // write HAIG into the current network
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
 
-//    pNtkAig = Abc_NtkIvyAfterHaig( pNtk, pMan, 1 );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    Ivy_ManHaigStop( pMan );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -239,7 +246,7 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
     if ( pMan == NULL )
         return NULL;
     Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -263,7 +270,9 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
     if ( pMan == NULL )
         return NULL;
     Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+//    Ivy_ManRewriteSeq( pMan, 1, 0 );
+//    Ivy_ManRewriteSeq( pMan, 1, 0 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -288,7 +297,7 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
         return NULL;
     pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
     Ivy_ManStop( pTemp );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -474,14 +483,14 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
 {
     Vec_Int_t * vNodes, * vLatches;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
-    Ivy_Obj_t * pNode;
+    Ivy_Obj_t * pNode, * pTemp;
     int i;
-    assert( Ivy_ManLatchNum(pMan) > 0 );
+//    assert( Ivy_ManLatchNum(pMan) > 0 );
     // perform strashing
     pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
@@ -493,7 +502,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
     {
         pObjNew = Abc_NtkCreateLatch( pNtk );
-        if ( Ivy_ObjInit(pNode) == IVY_INIT_DC )
+        if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
             Abc_LatchSetInitDc( pObjNew );
         else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
             Abc_LatchSetInit1( pObjNew );
@@ -505,14 +514,14 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     // rebuild the AIG
     Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
     {
-        // add the first fanins
+        // add the first fanin
         pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
         if ( Ivy_ObjIsBuf(pNode) )
         {
             pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
             continue;
         }
-        // add the first second
+        // add the second fanin
         pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
         // create the new node
         if ( Ivy_ObjIsExor(pNode) )
@@ -520,6 +529,22 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
         else
             pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
         pNode->TravId = Abc_EdgeFromNode( pObjNew );
+        // process the choice nodes
+        if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
+        {
+            pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
+            pFaninNew->fPhase = 0;
+            assert( !Ivy_IsComplement(pNode->pEquiv) );
+            for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
+            {
+                pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
+                pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
+                pFaninNew->pData = pFaninNew1;
+                pFaninNew = pFaninNew1;
+            }
+            pFaninNew->pData = NULL;
+//            printf( "Writing choice node %d.\n", pNode->Id );
+        }
     }
     // connect the PO nodes
     Abc_NtkForEachPo( pNtkOld, pObj, i )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index ecd44017..ea1beb8c 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -27,7 +27,6 @@
 static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
-static void        Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 6cbab1a6..0976b652 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -246,35 +246,47 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 {
     ProgressBar * pProgress;
     Vec_Ptr_t * vFuncsGlob;
-    Abc_Obj_t * pNode;
+    Abc_Obj_t * pNode, * pFanin;
     DdNode * bFunc;
     DdManager * dd;
-    int i, Counter;
+    int i, k, Counter;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtk->pManFunc );
 
     // start the manager
     assert( pNtk->pManGlob == NULL );
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // set reordering
     if ( fReorder )
         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
 
-    // set the elementary variables
+    // clean storage for local BDDs
     Abc_NtkCleanCopy( pNtk );
+    // set the elementary variables
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
+        if ( Abc_ObjFanoutNum(pNode) > 0 )
+        {
+            pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
+            Cudd_Ref( dd->vars[i] );
+        }
     // assign the constant node BDD
     pNode = Abc_NtkConst1( pNtk );
-    pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
+    if ( Abc_ObjFanoutNum(pNode) > 0 )
+    {
+        pNode->pCopy = (Abc_Obj_t *)dd->one;   
+        Cudd_Ref( dd->one );
+    }
 
     // collect the global functions of the COs
-    vFuncsGlob = Vec_PtrAlloc( 100 );
     Counter = 0;
+    vFuncsGlob = Vec_PtrAlloc( 100 );
     if ( fLatchOnly )
     {
         // construct the BDDs
         pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachLatch( pNtk, pNode, i )
         {
-//            Extra_ProgressBarUpdate( pProgress, i, NULL );
             bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
@@ -295,7 +307,6 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
         pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
-//            Extra_ProgressBarUpdate( pProgress, i, NULL );
             bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
@@ -305,12 +316,12 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
                 Cudd_Quit( dd );
                 return NULL;
             }
-            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );   Cudd_Ref( bFunc );
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );  Cudd_Ref( bFunc ); 
             Vec_PtrPush( vFuncsGlob, bFunc );
         }
         Extra_ProgressBarStop( pProgress );
     }
-
+/*
     // derefence the intermediate BDDs
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( pNode->pCopy ) 
@@ -318,6 +329,22 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
             Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
             pNode->pCopy = NULL;
         }
+*/
+/*
+    // make sure all nodes are derefed
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        if ( pNode->pCopy != NULL )
+            printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pNode->Id );
+        if ( pNode->vFanouts.nSize > 0 )
+            printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pNode->Id );
+    }
+*/
+    // reset references
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            pFanin->vFanouts.nSize++;
+
     // reorder one more time
     if ( fReorder )
     {
@@ -326,6 +353,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
     }
     pNtk->pManGlob = dd;
     pNtk->vFuncsGlob = vFuncsGlob;
+//    Cudd_PrintInfo( dd, stdout );
     return dd;
 }
 
@@ -342,7 +370,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 ***********************************************************************/
 DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
 {
-    DdNode * bFunc, * bFunc0, * bFunc1;
+    DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
     assert( !Abc_ObjIsComplement(pNode) );
     if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
     {
@@ -353,29 +381,87 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
         return NULL;
     }
     // if the result is available return
-    if ( pNode->pCopy )
-        return (DdNode *)pNode->pCopy;
-    // compute the result for both branches
-    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
-    if ( bFunc0 == NULL )
-        return NULL;
-    Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
-    if ( bFunc1 == NULL )
-        return NULL;
-    Cudd_Ref( bFunc1 );
-    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
-    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
-    // get the final result
-    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( dd, bFunc0 );
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    // set the result
-    assert( pNode->pCopy == NULL );
-    pNode->pCopy = (Abc_Obj_t *)bFunc;
-    // increment the progress bar
-    if ( pProgress )
-        Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL );
+    if ( pNode->pCopy == NULL )
+    {
+        Abc_Obj_t * pNodeC, * pNode0, * pNode1;
+        pNode0 = Abc_ObjFanin0(pNode);
+        pNode1 = Abc_ObjFanin1(pNode);
+        // check for the special case when it is MUX/EXOR
+//        if ( 0 )
+        if ( pNode0->pCopy == NULL && pNode1->pCopy == NULL &&
+             Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 && 
+             Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 && 
+             Abc_NodeIsMuxType(pNode) )
+        {
+            // deref the fanins
+            pNode0->vFanouts.nSize--;
+            pNode1->vFanouts.nSize--;
+            // recognize the MUX
+            pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
+            assert( Abc_ObjFanoutNum(pNodeC) > 1 );
+            // dereference the control once (the second time it will be derefed when BDDs are computed)
+            pNodeC->vFanouts.nSize--;
+
+            // compute the result for all branches
+            bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFuncC == NULL )
+                return NULL;
+            Cudd_Ref( bFuncC );
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc0 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc0 );
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc1 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc1 );
+
+            // complement the branch BDDs
+            bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjIsComplement(pNode0) );
+            bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjIsComplement(pNode1) );
+            // get the final result
+            bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 );   Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc0 );
+            Cudd_RecursiveDeref( dd, bFunc1 );
+            Cudd_RecursiveDeref( dd, bFuncC );
+            // add the number of used nodes
+            (*pCounter) += 3;
+        }
+        else
+        {
+            // compute the result for both branches
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc0 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc0 );
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            if ( bFunc1 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc1 );
+            bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+            bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+            // get the final result
+            bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc0 );
+            Cudd_RecursiveDeref( dd, bFunc1 );
+            // add the number of used nodes
+            (*pCounter)++;
+        }
+        // set the result
+        assert( pNode->pCopy == NULL );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+        // increment the progress bar
+        if ( pProgress )
+            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
+    }
+    // prepare the return value
+    bFunc = (DdNode *)pNode->pCopy;
+    // dereference BDD at the node
+    if ( --pNode->vFanouts.nSize == 0 )
+    {
+        Cudd_Deref( bFunc );
+        pNode->pCopy = NULL;
+    }
     return bFunc;
 }
 
diff --git a/src/base/abci/abcOrder.c b/src/base/abci/abcOrder.c
new file mode 100644
index 00000000..c9ebdc12
--- /dev/null
+++ b/src/base/abci/abcOrder.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+  FileName    [abcOrder.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Exploring static BDD variable orders.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcOrder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Changes the order of primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose )
+{
+    Vec_Ptr_t * vSupp;
+    vSupp = Abc_NtkSupport( pNtk );
+    Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
+    Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given variable order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose )
+{
+    char Buffer[1000];
+    FILE * pFile;
+    Vec_Ptr_t * vSupp;
+    Abc_Obj_t * pObj;
+    pFile = fopen( pFileName, "r" );
+    vSupp = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
+    while ( fscanf( pFile, "%s", Buffer ) == 1 )
+    {
+        pObj = Abc_NtkFindTerm( pNtk, Buffer );
+        if ( pObj == NULL || !Abc_ObjIsCi(pObj) )
+        {
+            printf( "Name \"%s\" is not a PI name. Cannot use this order.\n", Buffer );
+            Vec_PtrFree( vSupp );
+            fclose( pFile );
+            return;
+        }
+        Vec_PtrPush( vSupp, pObj );
+    }
+    fclose( pFile );
+    if ( Vec_PtrSize(vSupp) != Abc_NtkCiNum(pNtk) )
+    {
+        printf( "The number of names in the order (%d) is not the same as the number of PIs (%d).\n", Vec_PtrSize(vSupp), Abc_NtkCiNum(pNtk) );
+        Vec_PtrFree( vSupp );
+        return;
+    }
+    Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
+    Vec_PtrFree( vSupp );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Changes the order of primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Vec_PtrSize(vSupp) == Abc_NtkCiNum(pNtk) );
+    // order CIs using the array
+    if ( fReverse )
+        Vec_PtrForEachEntry( vSupp, pObj, i )
+            Vec_PtrWriteEntry( pNtk->vCis, Vec_PtrSize(vSupp)-1-i, pObj );
+    else
+        Vec_PtrForEachEntry( vSupp, pObj, i )
+            Vec_PtrWriteEntry( pNtk->vCis, i, pObj );
+    // order PIs accordingly
+    Vec_PtrClear( pNtk->vPis );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjIsPi(pObj) )
+            Vec_PtrPush( pNtk->vPis, pObj );
+//    Abc_NtkForEachCi( pNtk, pObj, i )
+//        printf( "%s ", Abc_ObjName(pObj) );
+//    printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 5d35678d..2e338e48 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,6 +15,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
+    src/base/abci/abcOrder.c \
     src/base/abci/abcPga.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcProve.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 614fa812..6da1f4d8 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -32,6 +32,8 @@ static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadVer     ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadVerLib  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 
@@ -45,6 +47,7 @@ static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
@@ -71,6 +74,8 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_ver",      IoCommandReadVer,      1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_verlib",   IoCommandReadVerLib,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
 
@@ -84,6 +89,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_verlib",  IoCommandWriteVerLib,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
 }
 
@@ -659,6 +665,209 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    st_table * tDesign;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+    extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    tDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck );
+    if ( tDesign == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
+        return 1;
+    }
+
+    if ( st_count(tDesign) == 1 )
+    {
+        st_generator * gen;
+        char * pName;
+        // find the network
+        st_foreach_item( tDesign, gen, (char**)&pName, (char**)&pNtk )
+        {
+            st_free_gen(gen);
+            break;
+        }
+        st_free_table( tDesign );
+
+        // convert it into a logic network
+        pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+        if ( pNtk == NULL )
+        {
+            fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+            return 1;
+        }
+        // replace the current network
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    }
+    else
+    {
+        printf( "The design includes more than one module and is currently not used.\n" );
+    }
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_ver [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read a network in structural verilog (using current library)\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    st_table * tDesign;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+    extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
+    extern void Ver_ParseFreeLibrary( st_table * pLibVer );
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    tDesign = Ver_ParseFile( FileName, NULL, fCheck );
+    if ( tDesign == NULL )
+    {
+        fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
+        return 1;
+    }
+    printf( "The library contains %d gates.\n", st_count(tDesign) );
+
+    // convert gates into AIGs
+    {
+        st_table * tLibrary;
+        st_generator * gen;
+        char * pName;
+        // transform the gates into the library AIGs
+        tLibrary  = st_init_table( strcmp, st_strhash );
+        st_foreach_item( tDesign, gen, (char**)&pName, (char**)&pNtk )
+        {
+            // convert the netlist into SOP logic network
+            pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+            Abc_NtkDelete( pTemp );
+            // perform structural hashing
+            pNtk = Abc_NtkStrash( pTemp = pNtk, 0, 1 );
+            Abc_NtkDelete( pTemp );
+            // insert the new network into the new library
+            st_insert( tLibrary, pNtk->pName, (char *)pNtk );
+        }
+        st_free_table( tDesign );
+
+        // free old library
+        if ( Abc_FrameReadLibVer() )
+            Ver_ParseFreeLibrary( Abc_FrameReadLibVer() );
+        // read new library
+        Abc_FrameSetLibVer( tLibrary );
+    }
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_verlib [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read a gate library in structural verilog\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pTemp;
@@ -1472,6 +1681,61 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    st_table * tLibrary;
+    char * FileName;
+    int c;
+    extern void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName );
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+
+    // derive the netlist
+    tLibrary = Abc_FrameReadLibVer();
+    if ( tLibrary == NULL )
+    {
+        fprintf( pAbc->Out, "Verilog library is not specified.\n" );
+        return 0;
+    }
+    Io_WriteVerilogLibrary( tLibrary, FileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_verlib [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the current verilog library\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 11dd2db1..ade9051f 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -43,6 +43,7 @@ struct Io_ReadBlif_t_
     // the error message
     FILE *               Output;       // the output stream
     char                 sError[1000]; // the error string generated during parsing
+    int                  fError;       // set to 1 when error occurs
 };
 
 static Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName );
@@ -182,7 +183,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
             return NULL;
         }
     }
-    else
+    else if ( !p->fError )
         Abc_NtkFinalizeRead( pNtkMaster );
     // return the master network
     return pNtkMaster;
@@ -273,7 +274,11 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         if ( p->vTokens == NULL ) // some files do not have ".end" in the end
             break;
         if ( fStatus == 1 )
+        {
+            Extra_ProgressBarStop( pProgress );
+            Abc_NtkDelete( pNtk );
             return NULL;
+        }
     }
     if ( p->pNtkMaster == NULL )
     Extra_ProgressBarStop( pProgress );
@@ -487,6 +492,16 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
     // set the pointer to the functionality of the node
     Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, p->vCubes->pArray) );
 
+    // check the size
+    if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum(Abc_ObjData(pNode)) )
+    {
+        p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+        sprintf( p->sError, "The number of fanins (%d) of node %s is different from SOP size (%d).", 
+            Abc_ObjFaninNum(pNode), Abc_ObjName(Abc_ObjFanout(pNode,0)), Abc_SopGetVarNum(Abc_ObjData(pNode)) );
+        Io_ReadBlifPrintErrorMessage( p );
+        return 1;
+    }
+
     // return the last array of tokens
     *pvTokens = vTokens;
     return 0;
@@ -735,6 +750,7 @@ int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vToken
 ***********************************************************************/
 void Io_ReadBlifPrintErrorMessage( Io_ReadBlif_t * p )
 {
+    p->fError = 1;
     if ( p->LineCur == 0 ) // the line number is not given
         fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
     else // print the error message with the line number
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
index 902219aa..594bf4eb 100644
--- a/src/base/io/ioWriteVer.c
+++ b/src/base/io/ioWriteVer.c
@@ -36,6 +36,7 @@ static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -73,6 +74,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     }
 
     // write the equations for the network
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     Io_WriteVerilogInt( pFile, pNtk );
     fprintf( pFile, "\n" );
     fclose( pFile );
@@ -80,6 +82,49 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
 
 /**Function*************************************************************
 
+  Synopsis    [Write verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
+{
+    FILE * pFile;
+    st_generator * gen;
+    Abc_Ntk_t * pNtk, * pNetlist;
+    char * pName;
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteVerilogLibrary(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    fprintf( pFile, "// Verilog library \"%s\" written by ABC on %s\n", pFileName, Extra_TimeStamp() );
+    fprintf( pFile, "\n" );
+    // write modules
+    st_foreach_item( tLibrary, gen, (char**)&pName, (char**)&pNtk )
+    {
+        // create netlist
+        pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+        // write the equations for the network
+        Io_WriteVerilogInt( pFile, pNetlist );
+        fprintf( pFile, "\n" );
+        // delete the netlist
+        Abc_NtkDelete( pNetlist );
+    }
+
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes verilog.]
 
   Description []
@@ -92,7 +137,6 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
 void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     // write inputs and outputs
-    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
     Io_WriteVerilogPis( pFile, pNtk, 3 );
     fprintf( pFile, ",\n   " );
@@ -111,9 +155,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
     Io_WriteVerilogRegs( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
     }
+    if ( Io_WriteVerilogWiresCount(pNtk) > 0 )
+    {
     fprintf( pFile, "  wire" );
     Io_WriteVerilogWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
+    }
     // write the nodes
     if ( Abc_NtkHasMapping(pNtk) )
         Io_WriteVerilogGates( pFile, pNtk );
@@ -205,7 +252,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the wires.]
+  Synopsis    [Counts the number of wires.]
 
   Description []
                
@@ -214,15 +261,10 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pTerm, * pNet;
-    int LineLength;
-    int AddedLength;
-    int NameCounter;
-    int i, Counter, nNodes;
-
-    // count the number of wires
+    int i, nNodes;
     nNodes = Abc_NtkLatchNum(pNtk);
     Abc_NtkForEachNode( pNtk, pTerm, i )
     {
@@ -233,6 +275,30 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             continue;
         nNodes++;
     }
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of wires
+    nNodes = Io_WriteVerilogWiresCount( pNtk );
 
     // write the wires
     Counter = 0;
diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c
index feb7a47e..cdfd98b8 100644
--- a/src/base/main/libSupport.c
+++ b/src/base/main/libSupport.c
@@ -44,42 +44,71 @@ void open_libs() {
 #else
     DIR* dirp;
     struct dirent* dp;
+    char *env, *init_p, *p;
+    int done;
+
+    env = getenv ("ABC_LIB_PATH");
+    if (env == NULL) {
+      printf("Warning: ABC_LIB_PATH not defined. Looking into the current directory.\n");
+      init_p = malloc (2*sizeof(char));
+      init_p[0]='.'; init_p[1] = 0;
+    } else {
+      init_p = malloc ((strlen(env)+1)*sizeof(char));
+      strcpy (init_p, env);
+    }
 
-    dirp = opendir(".");
-    while ((dp = readdir(dirp)) != NULL) {
+    // Extract directories and read libraries
+    done = 0;
+    p = init_p;
+    while (!done) {
+      char *endp = strchr (p,':');
+      if (endp == NULL) done = 1; // last directory in the list
+      else *endp = 0; // end of string
+
+      dirp = opendir(p);
+      if (dirp == NULL) {
+        printf("Warning: directory in ABC_LIB_PATH does not exist (%s).\n", p);
+        continue;
+      }
+
+      while ((dp = readdir(dirp)) != NULL) {
         if ((strncmp("libabc_", dp->d_name, 7) == 0) &&
             (strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) {
 
-            // make sure we don't overflow the handle array
-            if (curr_lib >= MAX_LIBS) {
-                printf("Warning: maximum number of ABC libraries (%d) exceeded.  Not loading %s.\n",
-                       MAX_LIBS,
-                       dp->d_name);
-            }
-
-            // attempt to load it
-            else {
-                char* szPrefixed = malloc((strlen(dp->d_name) + 3) * sizeof(char));
-                strcpy(szPrefixed, "./");
-                strcat(szPrefixed, dp->d_name);
-
-                libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
-
-                // did the load succeed?
-                if (libHandles[curr_lib] != 0) {
-                    printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
-                    curr_lib++;
-                } else {
-                    printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
-                }
-
-                free(szPrefixed);
+          // make sure we don't overflow the handle array
+          if (curr_lib >= MAX_LIBS) {
+            printf("Warning: maximum number of ABC libraries (%d) exceeded.  Not loading %s.\n",
+                   MAX_LIBS,
+                   dp->d_name);
+          }
+          
+          // attempt to load it
+          else {
+            char* szPrefixed = malloc((strlen(dp->d_name) + strlen(p) + 2) * 
+                                      sizeof(char));
+            sprintf(szPrefixed, "%s/", p);
+            strcat(szPrefixed, dp->d_name);
+            libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
+            
+            // did the load succeed?
+            if (libHandles[curr_lib] != 0) {
+              printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
+              curr_lib++;
+            } else {
+              printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
             }
+            
+            free(szPrefixed);
+          }
         }
+      }
+      closedir(dirp);
+      p = endp+1;
     }
-    closedir(dirp);
-#endif
 
+    free(init_p);
+#endif
+    
     // null terminate the list of handles
     libHandles[curr_lib] = 0;    
 }
diff --git a/src/base/main/main.h b/src/base/main/main.h
index fe511314..80238a05 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -97,6 +97,7 @@ extern int             Abc_FrameReadNtkStoreSize();
 extern void *          Abc_FrameReadLibLut();                    
 extern void *          Abc_FrameReadLibGen();                    
 extern void *          Abc_FrameReadLibSuper();                  
+extern void *          Abc_FrameReadLibVer();                  
 extern void *          Abc_FrameReadManDd();                     
 extern void *          Abc_FrameReadManDec();                    
 extern char *          Abc_FrameReadFlag( char * pFlag ); 
@@ -107,6 +108,7 @@ extern void            Abc_FrameSetNtkStoreSize( int nStored );
 extern void            Abc_FrameSetLibLut( void * pLib );        
 extern void            Abc_FrameSetLibGen( void * pLib );        
 extern void            Abc_FrameSetLibSuper( void * pLib );      
+extern void            Abc_FrameSetLibVer( void * pLib );      
 extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
 #ifdef __cplusplus
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index a1011a36..068a8bfb 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -48,6 +48,7 @@ int         Abc_FrameReadNtkStoreSize()              { return s_GlobalFrame->nSt
 void *      Abc_FrameReadLibLut()                    { return s_GlobalFrame->pLibLut;      } 
 void *      Abc_FrameReadLibGen()                    { return s_GlobalFrame->pLibGen;      } 
 void *      Abc_FrameReadLibSuper()                  { return s_GlobalFrame->pLibSuper;    } 
+void *      Abc_FrameReadLibVer()                    { return s_GlobalFrame->pLibVer;      } 
 void *      Abc_FrameReadManDd()                     { if ( s_GlobalFrame->dd == NULL )      s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );  return s_GlobalFrame->dd;      } 
 void *      Abc_FrameReadManDec()                    { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart();                                        return s_GlobalFrame->pManDec; } 
 char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
@@ -57,6 +58,7 @@ void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored  =
 void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
 void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
 void        Abc_FrameSetLibSuper( void * pLib )      { s_GlobalFrame->pLibSuper = pLib;    } 
+void        Abc_FrameSetLibVer( void * pLib )        { s_GlobalFrame->pLibVer   = pLib;    } 
 void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );  } 
 
 /**Function*************************************************************
@@ -135,11 +137,13 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void Rwt_ManGlobalStop();
     extern void undefine_cube_size();
+    extern void Ver_ParseFreeLibrary( st_table * pLibVer );
 //    extern void Ivy_TruthManStop();
 //    Abc_HManStop();
     undefine_cube_size();
     Rwt_ManGlobalStop();
 //    Ivy_TruthManStop();
+    if ( p->pLibVer ) Ver_ParseFreeLibrary( p->pLibVer );
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index d2bca1ab..13c71759 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -72,6 +72,7 @@ struct Abc_Frame_t_
     void *          pLibLut;     // the current LUT library
     void *          pLibGen;     // the current genlib
     void *          pLibSuper;   // the current supergate library
+    void *          pLibVer;     // the current Verilog library
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/temp.c b/src/base/temp.c
new file mode 100644
index 00000000..55709247
--- /dev/null
+++ b/src/base/temp.c
@@ -0,0 +1,83 @@
+
+/**Function*************************************************************
+
+  Synopsis    [Command procedure to allow for static BDD variable ordering.]
+
+  Description [This procedure should be integrated in "abc\src\base\abci\abc.c"
+  similar to how procedure Abc_CommandReorder() is currently integrated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int c;
+    int fReverse;
+    int fVerbose;
+    extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
+    extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fReverse = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'r':
+            fReverse ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    // if the var order file is given, implement this order
+    pFileName = NULL;
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pFileName = argv[globalUtilOptind];
+        pFile = fopen( pFileName, "r" );
+        if ( pFile == NULL )
+        {
+            fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
+            return 1;
+        }
+        fclose( pFile );
+    }
+    if ( pFileName )
+        Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
+    else
+        Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: order [-rvh] <file>\n" );
+    fprintf( pErr, "\t         computes a good static CI variable order\n" );
+    fprintf( pErr, "\t-r     : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );  
+    return 1;
+}