Version abc90807

committer: Baruch Sterin <baruchs@gmail.com>

4 files changed, 73 insertions, 8 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b73fdf9a..f251cdcc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -609,7 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
-
+ 
     Cmd_CommandAdd( pAbc, "AIG",          "&get",          Abc_CommandAbc9Get,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&put",          Abc_CommandAbc9Put,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&r",            Abc_CommandAbc9Read,         0 );
@@ -22299,14 +22299,20 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
     extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
+    extern Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk );
+    extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
     Gia_Man_t * pAig;
     Aig_Man_t * pMan;
     int c, fVerbose = 0;
+    int fNames = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fNames ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -22343,11 +22349,17 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pAig )
         Gia_ManStop( pAbc->pAig );
     pAbc->pAig = pAig;
+    if ( fNames )
+    {
+        pAig->vNamesIn  = Abc_NtkCollectCiNames( pAbc->pNtkCur );
+        pAig->vNamesOut = Abc_NtkCollectCoNames( pAbc->pNtkCur );
+    }
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &get [-vh] <file>\n" );
-    fprintf( stdout, "\t         transfer the current network from the old ABC\n" );
+    fprintf( stdout, "usage: &get [-nvh] <file>\n" );
+    fprintf( stdout, "\t         converts the network into an AIG and moves to the new ABC\n" );
+    fprintf( stdout, "\t-n     : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
     fprintf( stdout, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     fprintf( stdout, "\t<file> : the file name\n");
@@ -24058,7 +24070,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Cec_ManCorSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -24104,6 +24116,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fUseCSat ^= 1;
             break;
+        case 'w':
+            pPars->fVerboseFlops ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -24127,7 +24142,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &scorr [-FCP num] [-recvh]\n" );
+    fprintf( stdout, "usage: &scorr [-FCP num] [-recwvh]\n" );
     fprintf( stdout, "\t         performs signal correpondence computation\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@@ -24135,6 +24150,7 @@ usage:
     fprintf( stdout, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
     fprintf( stdout, "\t-e     : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
+    fprintf( stdout, "\t-w     : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index e30c6a93..790a9028 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -587,6 +587,50 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects CI of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_Ptr_t * vNames;
+    vNames = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
+    return vNames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects CO of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_Ptr_t * vNames;
+    vNames = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
+    return vNames;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collect latch values.]
 
   Description []
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index c4a68cc7..0b0294d5 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -263,7 +263,12 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int
 
     // check the case of constant node
     if ( Map_NodeIsConst(pNodeMap) )
-        return fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
+    {
+        pNodeNew = fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
+        if ( pNodeNew->pData == NULL )
+            printf( "Error creating mapped network: Library does not have a constant %d gate.\n", fPhase );
+        return pNodeNew;
+    }
 
     // check if the phase is already implemented
     pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase );
diff --git a/src/base/main/main.c b/src/base/main/main.c
index f74fb21a..ebe7c755 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -17,7 +17,7 @@
   Revision    [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
-
+ 
 #include "mainInt.h"
 
 // this line should be included in the library project