Version abc90807

committer: Baruch Sterin <baruchs@gmail.com>

13 files changed, 157 insertions, 23 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 7f445970..199d6939 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -135,6 +135,7 @@ struct Cec_ParCor_t_
     int              fUseCSat;      // use circuit-based solver
 //    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
+    int              fVerboseFlops; // verbose stats
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 96c45907..27a7dd36 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -990,6 +990,39 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints flop equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPrintFlopEquivs( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pRepr;
+    int i;
+    assert( p->vNamesIn != NULL );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
+            printf( "Flop \"%s\" is equivalent to constant 0.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
+        else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+        {
+            if ( Gia_ObjIsCi(pRepr) )
+                printf( "Flop \"%s\" is equivalent to flop \"%s\".\n", 
+                    Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj)  ), 
+                    Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
+            else
+                printf( "Flop \"%s\" is equivalent to internal node %d.\n", 
+                    Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
+        }
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Top-level procedure for register correspondence.]
 
   Description []
@@ -1060,6 +1093,14 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     }
     if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
         printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
+    // print verbose info about equivalences
+    if ( pPars->fVerboseFlops )
+    {
+        if ( pAig->vNamesIn == NULL )
+            printf( "Flop output names are not available. Use command \"&get -n\".\n" );
+        else
+            Cec_ManPrintFlopEquivs( pAig );
+    }
     return pNew;
 }
 
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 9dad2742..f8c1fe91 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -136,6 +136,8 @@ struct Gia_Man_t_
     unsigned char* pSwitching;    // switching activity for each object
     Gia_Plc_t *    pPlacement;    // placement of the objects
     int *          pTravIds;      // separate traversal ID representation
+    Vec_Ptr_t *    vNamesIn;      // the input names 
+    Vec_Ptr_t *    vNamesOut;     // the output names
 };
 
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 37afde13..4547e61c 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -66,6 +66,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
 ***********************************************************************/
 void Gia_ManStop( Gia_Man_t * p )  
 {
+    Vec_PtrFreeFree( p->vNamesIn );
+    Vec_PtrFreeFree( p->vNamesOut );
     if ( p->vFlopClasses )
     Vec_IntFree( p->vFlopClasses );
     Vec_IntFree( p->vCis );
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
diff --git a/src/map/super/superGate.c b/src/map/super/superGate.c
index cb7d8d78..6ffab984 100644
--- a/src/map/super/superGate.c
+++ b/src/map/super/superGate.c
@@ -706,7 +706,7 @@ void Super_TranferGatesToArray( Super_Man_t * pMan )
 {
     stmm_generator * gen;
     Super_Gate_t * pGate, * pList;
-    unsigned Key;
+    ABC_PTRUINT_T Key;
 
     // put the gates fron the table into the array
     ABC_FREE( pMan->pGates );
@@ -734,10 +734,10 @@ void Super_TranferGatesToArray( Super_Man_t * pMan )
 void Super_AddGateToTable( Super_Man_t * pMan, Super_Gate_t * pGate )
 {
     Super_Gate_t ** ppList;
-    unsigned Key;
+    ABC_PTRUINT_T Key;
 //    Key = pGate->uTruth[0] + 2003 * pGate->uTruth[1];
     Key = pGate->uTruth[0] ^ pGate->uTruth[1];
-    if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)Key, (char ***)&ppList ) )
+    if ( !stmm_find_or_add( pMan->tTable, (char *)Key, (char ***)&ppList ) )
         *ppList = NULL;
     pGate->pNext = *ppList;
     *ppList = pGate;
@@ -761,7 +761,7 @@ bool Super_CompareGates( Super_Man_t * pMan, unsigned uTruth[], float Area, floa
 {
     Super_Gate_t ** ppList, * pPrev, * pGate, * pGate2;
     int i, fNewIsBetter, fGateIsBetter;
-    unsigned Key;
+    ABC_PTRUINT_T Key;
 
     // skip constant functions
     if ( pMan->nVarsMax < 6 )
@@ -778,7 +778,7 @@ bool Super_CompareGates( Super_Man_t * pMan, unsigned uTruth[], float Area, floa
     // get hold of the place where the entry is stored
 //    Key = uTruth[0] + 2003 * uTruth[1];
     Key = uTruth[0] ^ uTruth[1];
-    if ( !stmm_find( pMan->tTable, (char *)(ABC_PTRUINT_T)Key, (char ***)&ppList ) )
+    if ( !stmm_find( pMan->tTable, (char *)Key, (char ***)&ppList ) )
         return 1; 
     // the entry with this truth table is found
     pPrev = NULL;
@@ -918,7 +918,7 @@ void Super_Write( Super_Man_t * pMan )
     Super_Gate_t * pGateRoot, * pGate;
     stmm_generator * gen;
     int fZeroFound, clk, v;
-    unsigned Key;
+    ABC_PTRUINT_T Key;
 
     if ( pMan->nGates < 1 )
     {
diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c
index 7f7cbb97..0d79a84c 100644
--- a/src/misc/nm/nmApi.c
+++ b/src/misc/nm/nmApi.c
@@ -118,7 +118,8 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, int Type, char * pName, char
     }
     // create a new entry
     nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1;
-    nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
+//    nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
+    nEntrySize = (nEntrySize / 8 + ((nEntrySize % 8) > 0)) * 8;
     pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize );
     pEntry->pNextI2N = pEntry->pNextN2I = pEntry->pNameSake = NULL;
     pEntry->ObjId = ObjId;
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 3f958b6f..7b153d90 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -465,6 +465,27 @@ static inline void Vec_PtrClear( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Deallocates array of memory pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
+{
+    void * pTemp;
+    int i;
+    if ( p == NULL ) return;
+    Vec_PtrForEachEntry( p, pTemp, i )
+        ABC_FREE( pTemp );
+    Vec_PtrFree( p );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Copies the interger array.]
 
   Description []
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 78d45b14..8f40d2f7 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -266,7 +266,7 @@ clk = clock();
         return 1;
     }
 clk = clock();
-    Abc_NtkMfsConstructGia( p );
+//    Abc_NtkMfsConstructGia( p );
 p->timeGia += clock() - clk;
     // solve the SAT problem
     if ( p->pPars->fPower )
@@ -280,7 +280,7 @@ p->timeGia += clock() - clk;
             Abc_NtkMfsResubNode2( p, pNode );
     }
 p->timeSat += clock() - clk;
-    Abc_NtkMfsDeconstructGia( p );
+//    Abc_NtkMfsDeconstructGia( p );
     return 1;
 }
 
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 8cd70dbf..b28e782a 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -99,16 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 {
     unsigned * pData;
     int RetValue, iVar, i;
-    int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
-p->timeGia += clock() - clk;
+//    int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
+//p->timeGia += clock() - clk;
 
     p->nSatCalls++;
     RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 //    assert( RetValue == l_False || RetValue == l_True );
-    if ( RetValue != l_Undef && RetValue2 != -1 )
-    {
-        assert( (RetValue == l_False) == (RetValue2 == 1) );
-    }
+
+//    if ( RetValue != l_Undef && RetValue2 != -1 )
+//    {
+//        assert( (RetValue == l_False) == (RetValue2 == 1) );
+//    }
 
     if ( RetValue == l_False )
         return 1;