Version abc50910

16 files changed, 474 insertions, 53 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f29859b9..0e296d64 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -430,11 +430,13 @@ extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern bool               Abc_NtkIsDfsOrdered( 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 );
 extern int                Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
 /*=== abcFanio.c ==========================================================*/
 extern void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
 extern void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 43235139..356a4eba 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -101,7 +101,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     }
     if ( Abc_NtkHasMapping(pNtk) )
     {
-        if ( pNtk->pManFunc != Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+        if ( pNtk->pManFunc != Abc_FrameReadLibGen() )
         {
             fprintf( stdout, "NetworkCheck: The library of the mapped network is not the global library.\n" );
             return 0;
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 31a6e8b9..097ee92d 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -206,6 +206,37 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     Vec_PtrPush( vNodes, pNode );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the ordering of nodes is DFS.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // mark the CIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Abc_NodeSetTravIdCurrent( pNode );
+    // go through the nodes
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) )
+            return 0;
+        if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
+            return 0;
+        Abc_NodeSetTravIdCurrent( pNode );
+    }
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -573,6 +604,123 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Analyses choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeSetChoiceLevel_rec( Abc_Obj_t * pNode, int fMaximum )
+{
+    Abc_Obj_t * pTemp;
+    int Level1, Level2, Level, LevelE;
+    // skip the visited node
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return (int)pNode->pCopy;
+    Abc_NodeSetTravIdCurrent( pNode );
+    // compute levels of the children nodes
+    Level1 = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin0(pNode), fMaximum );
+    Level2 = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin1(pNode), fMaximum );
+    Level  = 1 + ABC_MAX( Level1, Level2 );
+    if ( pNode->pData )
+    {
+        LevelE = Abc_NodeSetChoiceLevel_rec( pNode->pData, fMaximum );
+        if ( fMaximum )
+            Level = ABC_MAX( Level, LevelE );
+        else
+            Level = ABC_MIN( Level, LevelE );
+        // set the level of all equivalent nodes to be the same minimum
+        for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
+            pTemp->pCopy = (void *)Level;
+    }
+    pNode->pCopy = (void *)Level;
+    return Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets the levels of the nodes in the choice graph.]
+
+  Description [Makes the level of the choice nodes to be equal to the
+  maximum of the level of the nodes in the equivalence class. This way
+  sorting by level leads to the reverse topological order, which is
+  needed for the required time computation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_AigSetChoiceLevels( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, LevelMax, LevelCur;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // set the new travid counter
+    Abc_NtkIncrementTravId( pNtk );
+    // set levels of the CI and constant
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        Abc_NodeSetTravIdCurrent( pObj );
+        pObj->pCopy = NULL;
+    }
+    pObj = Abc_AigConst1( pNtk->pManFunc );
+    Abc_NodeSetTravIdCurrent( pObj );
+    pObj->pCopy = NULL;
+    // set levels of all other nodes
+    LevelMax = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        LevelCur = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin0(pObj), 1 );
+        LevelMax = ABC_MAX( LevelMax, LevelCur );
+    }
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns nodes by level from the smallest to the largest.]
+
+  Description [Correctly handles the case of choice nodes, by first
+  spreading them out across several levels and then collecting.]
+               
+  SideEffects [What happens with dangling nodes???]
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis )
+{
+    Vec_Ptr_t * vNodes, * vLevels;
+    Abc_Obj_t * pNode, ** ppHead;
+    int LevelMax, i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // set the correct levels
+    Abc_NtkCleanCopy( pNtk );
+    LevelMax = Abc_AigSetChoiceLevels( pNtk );
+    // relink nodes by level
+    vLevels = Vec_PtrStart( LevelMax + 1 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        ppHead = ((Abc_Obj_t **)vLevels->pArray) + (int)pNode->pCopy;
+        pNode->pCopy = *ppHead;
+        *ppHead = pNode;
+    }
+    // recollect nodes
+    vNodes = Vec_PtrStart( Abc_NtkNodeNum(pNtk) );
+    Vec_PtrForEachEntryStart( vLevels, pNode, i, !fCollectCis )
+        for ( ; pNode; pNode = pNode->pCopy )
+            Vec_PtrPush( vNodes, pNode );
+    Vec_PtrFree( vLevels );
+    return vNodes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index b21d16fc..dc4dd9e2 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -74,7 +74,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     else if ( Abc_NtkHasAig(pNtk) )
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+        pNtk->pManFunc = Abc_FrameReadLibGen();
     else
         assert( 0 );
     return pNtk;
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index d5c18d2e..53ba3568 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -518,7 +518,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -546,7 +546,7 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -574,7 +574,7 @@ Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_Not(Cudd_bddIthVar(pNtk->pManFunc,0)), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadInv(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadInv(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -602,7 +602,7 @@ Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIthVar(pNtk->pManFunc,0), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadBuf(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadBuf(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -781,7 +781,7 @@ bool Abc_NodeIsConst0( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return Abc_ObjNot(pNode) == Abc_AigConst1(pNode->pNtk->pManFunc);
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadConst0(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadConst0(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
@@ -809,7 +809,7 @@ bool Abc_NodeIsConst1( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return pNode == Abc_AigConst1(pNode->pNtk->pManFunc);
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadConst1(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadConst1(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
@@ -838,7 +838,7 @@ bool Abc_NodeIsBuf( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return 0;
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadBuf(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadBuf(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
@@ -867,7 +867,7 @@ bool Abc_NodeIsInv( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return 0;
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadInv(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadInv(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dfe3ccc8..c4feb7a2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22,6 +22,8 @@
 #include "mainInt.h"
 #include "fraig.h"
 #include "fxu.h"
+#include "fpga.h"
+#include "pga.h"
 #include "cut.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -80,6 +82,7 @@ static int Abc_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -156,6 +159,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Abc_CommandSuperChoice,      1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
@@ -2720,14 +2724,13 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
-    pParams->fTruth    = 1;     // compute truth tables
-    pParams->fHash     = 0;     // hash cuts to detect unique
-    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fSeq      = 0;     // compute sequential cuts
     pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "KMtrfsdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "KMtfsdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2756,9 +2759,6 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pParams->fTruth ^= 1;
             break;
-        case 'r':
-            pParams->fHash ^= 1;
-            break;
         case 'f':
             pParams->fFilter ^= 1;
             break;
@@ -2794,16 +2794,15 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-trfsdvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfsdvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
-    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",    pParams->nVarsMax );
-    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",     pParams->nKeepMax );
-    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",          pParams->fTruth? "yes": "no" );
-    fprintf( pErr, "\t-r     : toggle reduction by hashing [default = %s]\n",             pParams->fHash? "yes": "no" );
-    fprintf( pErr, "\t-f     : toggle filtering by dominance [default = %s]\n",           pParams->fFilter? "yes": "no" );
-    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",       pParams->fSeq? "yes": "no" );
-    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",   pParams->fDrop? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",     pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
+    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",        pParams->fSeq? "yes": "no" );
+    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -3771,6 +3770,123 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Pga_Params_t Params, * pParams = &Params;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    memset( pParams, 0, sizeof(Pga_Params_t) );
+    pParams->pNtk       = pNtk;
+    pParams->pLutLib    = Abc_FrameReadLibLut();
+    pParams->fAreaFlow  = 1;
+    pParams->fArea      = 1;
+    pParams->fSwitching = 0;
+    pParams->fDropCuts  = 0;
+    pParams->fVerbose   = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "fapdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'f':
+            pParams->fAreaFlow ^= 1;
+            break;
+        case 'a':
+            pParams->fArea ^= 1;
+            break;
+        case 'p':
+            pParams->fSwitching ^= 1;
+            break;
+        case 'd':
+            pParams->fDropCuts ^= 1;
+            break;
+        case 'v':
+            pParams->fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        // strash and balance the network
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
+        // get the new network
+        pNtkRes = Abc_NtkPga( pParams );
+        if ( pNtkRes == NULL )
+        {
+            Abc_NtkDelete( pNtk );
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+        Abc_NtkDelete( pNtk );
+    }
+    else
+    {
+        // get the new network
+        pNtkRes = Abc_NtkPga( pParams );
+        if ( pNtkRes == NULL )
+        {
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: pga [-fapdvh]\n" );
+    fprintf( pErr, "\t        performs FPGA mapping of the current network\n" );
+    fprintf( pErr, "\t-f    : toggles area flow recovery [default = %s]\n", pParams->fAreaFlow? "yes": "no" );
+    fprintf( pErr, "\t-a    : toggles area recovery [default = %s]\n", pParams->fArea? "yes": "no" );
+    fprintf( pErr, "\t-p    : optimizes power by minimizing switching activity [default = %s]\n", pParams->fSwitching? "yes": "no" );
+    fprintf( pErr, "\t-d    : toggles dropping cuts to save memory [default = %s]\n", pParams->fDropCuts? "yes": "no" );
+    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h    : prints the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index 6ee1fb90..02fe7284 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -66,7 +66,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsSopLogic(pNtk) );
 
     // check that the library is available
-    pGenlib = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+    pGenlib = Abc_FrameReadLibGen();
     if ( pGenlib == NULL )
     {
         printf( "The current library is not available.\n" );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index f487bd1b..e7309a59 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -105,7 +105,6 @@ PRT( "Total", clock() - clk );
         if ( Abc_NodeIsTravIdCurrent(pDriver) )
             continue;
         Abc_NodeSetTravIdCurrent(pDriver);
-        Cut_NodeSetComputedAsNew( p, pDriver->Id );
     }
     // compute as long as new cuts appear
 
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 3f860585..7a8eed5d 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -556,7 +556,7 @@ void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
     int i, k;
     // check that the PO functions are correct
     nPoFinal = Abc_NtkPoNum(pFraig);
-    nStored  = Abc_FrameReadNtkStoreSize(Abc_FrameGetGlobalFrame());
+    nStored  = Abc_FrameReadNtkStoreSize();
     assert( nPoFinal % nStored == 0 );
     nPoOrig  = nPoFinal / nStored;
     for ( i = 0; i < nPoOrig; i++ )
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index ec5352cb..44f5aa94 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -66,18 +66,18 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
-    if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
+    if ( Abc_FrameReadLibGen() == NULL )
     {
         printf( "The current library is not available.\n" );
         return 0;
     }
 
     // derive the supergate library
-    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL && Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
     {
         printf( "A simple supergate library is derived from gate library \"%s\".\n", 
-            Mio_LibraryReadName(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) );
-        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
     }
 
     // print a warning about choice nodes
@@ -410,7 +410,7 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsMappedLogic(pNtk) );
     // update the functionality manager
-    assert( pNtk->pManFunc == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+    assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
     pNtk->pManFunc = Extra_MmFlexStart();
     pNtk->ntkFunc  = ABC_FUNC_SOP;
     // update the nodes
@@ -446,18 +446,18 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
-    if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
+    if ( Abc_FrameReadLibGen() == NULL )
     {
         printf( "The current library is not available.\n" );
         return 0;
     }
 
     // derive the supergate library
-    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL && Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
     {
         printf( "A simple supergate library is derived from gate library \"%s\".\n", 
-            Mio_LibraryReadName(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) );
-        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
     }
 
     // print a warning about choice nodes
diff --git a/src/base/abci/abcPga.c b/src/base/abci/abcPga.c
new file mode 100644
index 00000000..0562ddb2
--- /dev/null
+++ b/src/base/abci/abcPga.c
@@ -0,0 +1,155 @@
+/**CFile****************************************************************
+
+  FileName    [abcPga.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcPga.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+#include "fpga.h"
+#include "pga.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts );
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams )
+{
+    Abc_Ntk_t * pNtkNew, * pNtk = pParams->pNtk;
+    Pga_Man_t * pMan;
+    Vec_Ptr_t * vNodeCuts;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // print a warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Performing FPGA mapping with choices.\n" );
+
+    // start the mapping manager
+    pMan = Pga_ManStart( pParams );    
+    if ( pMan == NULL )
+        return NULL;
+
+    // perform mapping
+    vNodeCuts = Pga_DoMapping( pMan );
+
+    // transform the result of mapping into a BDD logic network
+    pNtkNew = Abc_NtkFromPga( pNtk, vNodeCuts );
+    if ( pNtkNew == NULL )
+        return NULL;
+    Pga_ManStop( pMan );
+    Vec_PtrFree( vNodeCuts );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkPga: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts )
+{
+    ProgressBar * pProgress;
+    DdManager * dd;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pFanin, * pNodeNew;
+    Cut_Cut_t * pCut;
+    Vec_Ptr_t * vLeaves, * vVisited;
+    int i, k, nDupGates;
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
+    dd = pNtkNew->pManFunc;
+    // set the constant node
+    pNode = Abc_AigConst1(pNtk->pManFunc);
+    if ( Abc_ObjFanoutNum(pNode) > 0 )
+        pNode->pCopy = Abc_NodeCreateConst1(pNtkNew);
+    // add new nodes in topologic order
+    vLeaves  = Vec_PtrAlloc( 6 );
+    vVisited = Vec_PtrAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodeCuts) );
+    Vec_PtrForEachEntry( vNodeCuts, pCut, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // create the new node
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Vec_PtrClear( vLeaves );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+        {
+            // add the node representing the old fanin in the new network
+            pFanin = Abc_NtkObj( pNtk, pCut->pLeaves[k] );
+            Vec_PtrPush( vLeaves, pFanin );
+            Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
+        }
+        // set the new node at the old node
+        pNode = Abc_NtkObj( pNtk, pCut->uSign );  // pCut->uSign contains the ID of the root node
+        pNode->pCopy = pNodeNew;
+        // create the function of the new node
+        pNodeNew->pData = Abc_NodeConeBdd( dd, dd->vars, pNode, vLeaves, vVisited );   Cudd_Ref( pNodeNew->pData );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vVisited );
+    Vec_PtrFree( vLeaves );
+    // finalize the new network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 81d97028..91a99a57 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -32,7 +32,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop );
+static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk );
 static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
@@ -52,7 +52,6 @@ static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
 ***********************************************************************/
 int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose )
 {
-    int fDrop = 0;
     ProgressBar * pProgress;
     Cut_Man_t * pManCut;
     Rwr_Man_t * pManRwr;
@@ -72,7 +71,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
         Abc_NtkStartReverseLevels( pNtk );
     // start the cut manager
 clk = clock();
-    pManCut = Abc_NtkStartCutManForRewrite( pNtk, fDrop );
+    pManCut = Abc_NtkStartCutManForRewrite( pNtk );
 Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
     pNtk->pManCut = pManCut;
 
@@ -142,7 +141,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
+Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk )
 {
     static Cut_Params_t Params, * pParams = &Params;
     Cut_Man_t * pManCut;
@@ -153,10 +152,9 @@ Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
     pParams->nVarsMax  = 4;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
     pParams->fTruth    = 1;     // compute truth tables
-    pParams->fHash     = 1;     // hash cuts to detect unique
-    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fSeq      = 0;     // compute sequential cuts
-    pParams->fDrop     = fDrop; // drop cuts on the fly
+    pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fVerbose  = 0;     // the verbosiness flag
     pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
     pManCut = Cut_ManStart( pParams );
@@ -182,13 +180,15 @@ Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
 ***********************************************************************/
 void Abc_NodePrintCuts( Abc_Obj_t * pNode )
 {
+    Vec_Ptr_t * vCuts;
     Cut_Cut_t * pCut;
-    unsigned uTruth;
+    int k;
+
     printf( "\nNode %s\n", Abc_ObjName(pNode) );
-    for ( pCut = (Cut_Cut_t *)pNode->pCopy; pCut; pCut = pCut->pNext )
+    vCuts = (Vec_Ptr_t *)pNode->pCopy;
+    Vec_PtrForEachEntry( vCuts, pCut, k )
     {
-        uTruth = pCut->uTruth;
-        Extra_PrintBinary( stdout, &uTruth, 16 ); 
+        Extra_PrintBinary( stdout, (unsigned *)&pCut->uSign, 16 ); 
         printf( "   " );
         Cut_CutPrint( pCut );   
         printf( "\n" );
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index b8524bd5..445978b3 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -470,9 +470,9 @@ void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtkOld )
     int i;
     if ( pNtkOld->pManTime == NULL )
         return;
-    if ( Mio_LibraryReadNand2(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) == NULL )
+    if ( Mio_LibraryReadNand2(Abc_FrameReadLibGen()) == NULL )
         return;
-    tAndDelay = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+    tAndDelay = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen());
     Abc_NtkForEachPi( pNtkOld, pNodeOld, i )
     {
         pNodeNew = pNodeOld->pCopy;
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index d7c0add2..0123e213 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -10,6 +10,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/abcPga.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 946de42b..7adec714 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -550,7 +550,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     int i, nNames;
 
     // check that the library is available
-    pGenlib = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+    pGenlib = Abc_FrameReadLibGen();
     if ( pGenlib == NULL )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
diff --git a/src/base/main/main.c b/src/base/main/main.c
index d44dade9..43ad6956 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -21,7 +21,7 @@
 #include "mainInt.h"
 
 // this line should be included in the library project
-#define _LIB
+//#define _LIB
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///