Version abc80517

5 files changed, 105 insertions, 56 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 0cafa314..8f0c7210 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -29,8 +29,6 @@ extern "C" {
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#pragma warning( disable : 4273 )
-
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -226,6 +224,8 @@ struct Abc_Lib_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+//#pragma warning( disable : 4273 )
+
 #ifdef WIN32
 #define DLLEXPORT __declspec(dllexport)
 #define DLLIMPORT __declspec(dllimport)
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9b5ebddb..8d27c0d2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2762,19 +2762,36 @@ usage:
 int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fCleanupPis;
+    int fCleanupPos;
+    int fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fCleanupPis = 1;
+    fCleanupPos = 1;
+    fVerbose    = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "iovh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'i':
+            fCleanupPis ^= 1;
+            break;
+        case 'o':
+            fCleanupPos ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2789,16 +2806,35 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
+        if ( !fCleanupPos && !fCleanupPos )
+        {
+            printf( "Cleanup for PIs and POs is not enabled.\n" );
+            pNtkRes = Abc_NtkDup( pNtk );
+        }
+        else
+            pNtkRes = Abc_NtkDarCleanupAig( pNtk, fCleanupPis, fCleanupPos, fVerbose );
+    }
+    else
+    {
+        Abc_NtkCleanup( pNtk, fVerbose );
+        pNtkRes = Abc_NtkDup( pNtk );
+    }
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Cleanup has failed.\n" );
         return 1;
     }
-    // modify the current network
-    Abc_NtkCleanup( pNtk, 1 );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cleanup [-h]\n" );
-    fprintf( pErr, "\t        removes dangling nodes\n" );
+    fprintf( pErr, "usage: cleanup [-iovh]\n" );
+    fprintf( pErr, "\t        for logic networks, removes dangling combinatinal logic\n" );
+    fprintf( pErr, "\t        for AIGs, removes PIs w/o fanout and POs driven by const-0\n" );
+    fprintf( pErr, "\t-i    : toggles removing PIs without fanout [default = %s]\n", fCleanupPis? "yes": "no" );
+    fprintf( pErr, "\t-o    : toggles removing POs with const-0 drivers [default = %s]\n", fCleanupPos? "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;
 }
@@ -7469,7 +7505,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 //    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-//    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
@@ -7661,7 +7697,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 //    Abc_NtkDarPartition( pNtk );
-Abc_NtkDarTest( pNtk );
+//Abc_NtkDarTest( pNtk );
+
+
+Abc_NtkDarHaigRecord( pNtk );
 return 0;
 
     pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ca54e4e1..f369918e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -94,16 +94,6 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     pMan->fCatchExor = fExors;
 
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
-    // save the number of registers
-    if ( fRegisters )
-    {
-        pMan->nRegs = Abc_NtkLatchNum(pNtk);
-        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
-//        pMan->vFlopNums = NULL;
-//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
-        if ( pNtk->vOnehots )
-            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
-    }
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
@@ -134,6 +124,16 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     if ( !fExors && nNodes )
         printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
 //Aig_ManDumpVerilog( pMan, "test.v" );
+    // save the number of registers
+    if ( fRegisters )
+    {
+        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
+        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
+//        pMan->vFlopNums = NULL;
+//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
+        if ( pNtk->vOnehots )
+            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
+    }
     if ( !Aig_ManCheck( pMan ) )
     {
         printf( "Abc_NtkToDar: AIG check has failed.\n" );
@@ -1220,8 +1220,6 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
         return RetValue;
     }
     assert( pMan->nRegs > 0 );
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
     // perform verification
     if ( fNewAlgo )
     {
@@ -1282,8 +1280,6 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
     RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
@@ -1593,9 +1589,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbo
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
     pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
     Aig_ManStop( pTemp );
 
@@ -1630,9 +1623,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwa
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
     pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
     Aig_ManStop( pTemp );
 
@@ -1664,11 +1654,8 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
     Aig_ManPrintStats(pMan);
-    Saig_ManRetimeSteps( pMan, 1, 0 );
+    Saig_ManRetimeSteps( pMan, 1000, 1 );
     Aig_ManPrintStats(pMan);
 
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@@ -1689,18 +1676,16 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
-/*
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
-//    Aig_ManReduceLachesCount( pMan );
     if ( pMan->vFlopNums )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
-    Aig_ManHaigRecord( pMan );
+
+    Saig_ManHaigRecord( pMan );
     Aig_ManStop( pMan );
-*/
 }
 
 /**Function*************************************************************
@@ -2006,8 +1991,6 @@ void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
     if ( pMan == NULL )
         return;
     assert( Aig_ManRegNum(pMan) > 0 );
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
     Saig_ManPrintCones( pMan );
     Aig_ManStop( pMan );
 }
@@ -2063,10 +2046,7 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
     Vec_Int_t * vInits;
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     vInits = Abc_NtkGetLatchValues(pNtk);
@@ -2097,10 +2077,7 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
@@ -2116,6 +2093,43 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI
 
 /**Function*************************************************************
 
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( fCleanupPis )
+    {
+        int Temp = Aig_ManPiCleanup( pMan );
+        if ( fVerbose )
+            printf( "Cleanup removed %d primary inputs without fanout.\n", Temp );                                                                     
+    }
+    if ( fCleanupPos )
+    {
+        int Temp = Aig_ManPoCleanup( pMan );
+        if ( fVerbose )
+            printf( "Cleanup removed %d primary outputs driven by const-0.\n", Temp );                                                                     
+    }
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs BDD-based reachability analysis.]
 
   Description []
@@ -2129,10 +2143,7 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
 {
     extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
     Aig_Man_t * pMan;
-    pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
     Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
@@ -2156,9 +2167,6 @@ void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
     Aig_Man_t * pMan;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
     if ( pMan == NULL )
         return;
 
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index a6ec6981..f74cbee8 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -523,6 +523,7 @@ void Abc_NtkRecAdd( Abc_Ntk_t * pNtk )
     pPars->nFlowIters  =  0;
     pPars->nAreaIters  =  0;
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  0;
     pPars->fArea       =  1;
     pPars->fFancy      =  0;
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 8e8e8719..f2861204 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -74,6 +74,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     pPars->nFlowIters  =  nFlowIters;
     pPars->nAreaIters  =  nAreaIters;
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  1;
     pPars->fArea       =  fArea;
     pPars->fFancy      =  0;