summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/cec/cec.h1
-rw-r--r--src/aig/cec/cecCorr.c41
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaMan.c2
-rw-r--r--src/base/abci/abc.c28
-rw-r--r--src/base/abci/abcDar.c44
-rw-r--r--src/base/abci/abcMap.c7
-rw-r--r--src/base/main/main.c2
-rw-r--r--src/map/super/superGate.c12
-rw-r--r--src/misc/nm/nmApi.c3
-rw-r--r--src/misc/vec/vecPtr.h21
-rw-r--r--src/opt/mfs/mfsCore.c4
-rw-r--r--src/opt/mfs/mfsResub.c13
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-28 15:58:33 +0000