Skip to content

A
abc
Commit ea13085f by Alan Mishchenko
Options

Added printout of BMC tents in &ps.

parent c2b2e992
Showing with 46 additions and 28 deletions
src/aig/gia/gia.h
...@@ -742,7 +742,7 @@ extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pP ...@@ -742,7 +742,7 @@ extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pP
extern Gia_Man_t * Gia_ManStart( int nObjsMax ); extern Gia_Man_t * Gia_ManStart( int nObjsMax );
extern void Gia_ManStop( Gia_Man_t * p ); extern void Gia_ManStop( Gia_Man_t * p );
extern void Gia_ManStopP( Gia_Man_t ** p ); extern void Gia_ManStopP( Gia_Man_t ** p );
extern void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); extern void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch );
extern void Gia_ManPrintStatsShort( Gia_Man_t * p ); extern void Gia_ManPrintStatsShort( Gia_Man_t * p );
extern void Gia_ManPrintMiterStatus( Gia_Man_t * p ); extern void Gia_ManPrintMiterStatus( Gia_Man_t * p );
extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs ); extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
......
src/aig/gia/giaAbs.c
...@@ -292,7 +292,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ) ...@@ -292,7 +292,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
Vec_IntFree( vAbsFfsToAdd ); Vec_IntFree( vAbsFfsToAdd );
if ( p->fVerbose ) if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
return -1; return -1;
} }
...@@ -365,7 +365,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit ...@@ -365,7 +365,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
} }
Aig_ManStop( pAig ); Aig_ManStop( pAig );
if ( fVerbose ) if ( fVerbose )
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
return RetValue; return RetValue;
} }
...@@ -409,7 +409,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) ...@@ -409,7 +409,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
Vec_IntFreeP( &vGateClassesOld ); Vec_IntFreeP( &vGateClassesOld );
pGia->vGateClasses = vGateClasses; pGia->vGateClasses = vGateClasses;
if ( p->fVerbose ) if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
return 1; return 1;
} }
...@@ -494,7 +494,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ) ...@@ -494,7 +494,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
Gia_ManStop( pGiaAbs ); Gia_ManStop( pGiaAbs );
} }
if ( p->fVerbose ) if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
return 1; return 1;
} }
......
src/aig/gia/giaCof.c
...@@ -862,7 +862,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose ...@@ -862,7 +862,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) ); printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) );
Gia_ManPrintStats( p, 0 ); Gia_ManPrintStats( p, 0, 0 );
} }
if ( Vec_IntSize( vSigs ) > 200 ) if ( Vec_IntSize( vSigs ) > 200 )
{ {
...@@ -888,7 +888,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose ...@@ -888,7 +888,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
if ( fVerbose ) if ( fVerbose )
printf( "Cofactored variable %d.\n", iVar ); printf( "Cofactored variable %d.\n", iVar );
if ( fVerbose ) if ( fVerbose )
Gia_ManPrintStats( pAig, 0 ); Gia_ManPrintStats( pAig, 0, 0 );
} }
Vec_IntFree( vSigsNew ); Vec_IntFree( vSigsNew );
return pAig; return pAig;
......
src/aig/gia/giaEquiv.c
...@@ -1686,7 +1686,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f ...@@ -1686,7 +1686,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
} }
// (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
Gia_ManCleanMark0( pGia ); Gia_ManCleanMark0( pGia );
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
for ( nIter = 0; ; nIter++ ) for ( nIter = 0; ; nIter++ )
{ {
if ( Gia_ManHasNoEquivs(pGia) ) if ( Gia_ManHasNoEquivs(pGia) )
......
src/aig/gia/giaMan.c
...@@ -363,7 +363,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p ) ...@@ -363,7 +363,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
{ {
if ( p->pName ) if ( p->pName )
printf( "%-8s : ", p->pName ); printf( "%-8s : ", p->pName );
...@@ -399,6 +399,19 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) ...@@ -399,6 +399,19 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
Gia_ManPrintFlopClasses( p ); Gia_ManPrintFlopClasses( p );
Gia_ManPrintGateClasses( p ); Gia_ManPrintGateClasses( p );
Gia_ManPrintObjClasses( p ); Gia_ManPrintObjClasses( p );
if ( fTents )
{
int k, Entry, Prev = 1;
Vec_Int_t * vLimit = Vec_IntAlloc( 1000 );
Gia_Man_t * pNew = Gia_ManUnrollDup( p, vLimit );
printf( "Tents: " );
Vec_IntForEachEntryStart( vLimit, Entry, k, 1 )
printf( "%d = %d ", k, Entry-Prev ), Prev = Entry;
printf( " Unused = %d.", Gia_ManObjNum(p) - Gia_ManObjNum(pNew) );
printf( "\n" );
Vec_IntFree( vLimit );
Gia_ManStop( pNew );
}
} }
/**Function************************************************************* /**Function*************************************************************
......
src/aig/gia/giaReparam.c
...@@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) ...@@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Original AIG:\n" ); printf( "Original AIG:\n" );
Gia_ManPrintStats( p, 0 ); Gia_ManPrintStats( p, 0, 0 );
} }
// perform input trimming // perform input trimming
...@@ -155,7 +155,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) ...@@ -155,7 +155,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
{ {
printf( "After PI trimming:\n" ); printf( "After PI trimming:\n" );
Gia_ManPrintStats( pNew, 0 ); Gia_ManPrintStats( pNew, 0, 0 );
} }
// transform GIA // transform GIA
pNew = Gia_ManDupIn2Ff( pTmp = pNew ); pNew = Gia_ManDupIn2Ff( pTmp = pNew );
...@@ -163,7 +163,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) ...@@ -163,7 +163,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
{ {
printf( "After PI-2-FF transformation:\n" ); printf( "After PI-2-FF transformation:\n" );
Gia_ManPrintStats( pNew, 0 ); Gia_ManPrintStats( pNew, 0, 0 );
} }
// derive AIG // derive AIG
...@@ -178,7 +178,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) ...@@ -178,7 +178,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
{ {
printf( "After min-area retiming:\n" ); printf( "After min-area retiming:\n" );
Gia_ManPrintStats( pNew, 0 ); Gia_ManPrintStats( pNew, 0, 0 );
} }
// transform back // transform back
...@@ -187,7 +187,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) ...@@ -187,7 +187,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
{ {
printf( "After FF-2-PI tranformation:\n" ); printf( "After FF-2-PI tranformation:\n" );
Gia_ManPrintStats( pNew, 0 ); Gia_ManPrintStats( pNew, 0, 0 );
} }
return pNew; return pNew;
} }
......
src/base/abc/abcHieCec.c
...@@ -402,7 +402,7 @@ Gia_Man_t * Abc_NtkDeriveFlatGia2Derive( Abc_Ntk_t * pNtk, Vec_Ptr_t * vOrder ) ...@@ -402,7 +402,7 @@ Gia_Man_t * Abc_NtkDeriveFlatGia2Derive( Abc_Ntk_t * pNtk, Vec_Ptr_t * vOrder )
Gia_ManStop( pGiaBox ); Gia_ManStop( pGiaBox );
printf( "%8d -> ", Abc_NtkCountAndNodes(vOrder) ); printf( "%8d -> ", Abc_NtkCountAndNodes(vOrder) );
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
return pGia; return pGia;
} }
/* /*
...@@ -721,7 +721,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose ) ...@@ -721,7 +721,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
clk = clock(); clk = clock();
pGia = Abc_NtkDeriveFlatGia2( pNtk, vOrder ); pGia = Abc_NtkDeriveFlatGia2( pNtk, vOrder );
Abc_PrintTime( 1, "Deriving GIA", clock() - clk ); Abc_PrintTime( 1, "Deriving GIA", clock() - clk );
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
// Gia_ManStop( pGia ); // Gia_ManStop( pGia );
Vec_PtrFree( vOrder ); Vec_PtrFree( vOrder );
...@@ -737,7 +737,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose ) ...@@ -737,7 +737,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
clk = clock(); clk = clock();
pGia = Abc_NtkDeriveFlatGia( pNtk ); pGia = Abc_NtkDeriveFlatGia( pNtk );
Abc_PrintTime( 1, "Deriving GIA", clock() - clk ); Abc_PrintTime( 1, "Deriving GIA", clock() - clk );
Gia_ManPrintStats( pGia, 0 ); Gia_ManPrintStats( pGia, 0, 0 );
// clean nodes/boxes of all nodes // clean nodes/boxes of all nodes
Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i ) Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i )
......
src/base/abci/abc.c
...@@ -22031,11 +22031,15 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22031,11 +22031,15 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
int c; int c;
int fSwitch = 0; int fSwitch = 0;
int fTents = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "tph" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 't':
fTents ^= 1;
break;
case 'p': case 'p':
fSwitch ^= 1; fSwitch ^= 1;
break; break;
...@@ -22050,12 +22054,13 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22050,12 +22054,13 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" );
return 1; return 1;
} }
Gia_ManPrintStats( pAbc->pGia, fSwitch ); Gia_ManPrintStats( pAbc->pGia, fTents, fSwitch );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &ps [-ph]\n" ); Abc_Print( -2, "usage: &ps [-tph]\n" );
Abc_Print( -2, "\t prints stats of the current AIG\n" ); Abc_Print( -2, "\t prints stats of the current AIG\n" );
Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", fTents? "yes": "no" );
Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", fSwitch? "yes": "no" ); Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", fSwitch? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
......
src/misc/util/utilSort.c
...@@ -509,7 +509,7 @@ void Abc_QuickSort1( word * pData, int nSize, int fDecrease ) ...@@ -509,7 +509,7 @@ void Abc_QuickSort1( word * pData, int nSize, int fDecrease )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Iso_SelectSortInc( word * pData, int nSize ) static inline void Abc_SelectSortInc( word * pData, int nSize )
{ {
int i, j, best_i; int i, j, best_i;
for ( i = 0; i < nSize-1; i++ ) for ( i = 0; i < nSize-1; i++ )
...@@ -521,7 +521,7 @@ static inline void Iso_SelectSortInc( word * pData, int nSize ) ...@@ -521,7 +521,7 @@ static inline void Iso_SelectSortInc( word * pData, int nSize )
ABC_SWAP( word, pData[i], pData[best_i] ); ABC_SWAP( word, pData[i], pData[best_i] );
} }
} }
static inline void Iso_SelectSortDec( word * pData, int nSize ) static inline void Abc_SelectSortDec( word * pData, int nSize )
{ {
int i, j, best_i; int i, j, best_i;
for ( i = 0; i < nSize-1; i++ ) for ( i = 0; i < nSize-1; i++ )
...@@ -543,7 +543,7 @@ void Abc_QuickSort2Inc_rec( word * pData, int l, int r ) ...@@ -543,7 +543,7 @@ void Abc_QuickSort2Inc_rec( word * pData, int l, int r )
assert( l < r ); assert( l < r );
if ( r - l < 10 ) if ( r - l < 10 )
{ {
Iso_SelectSortInc( pData + l, r - l + 1 ); Abc_SelectSortInc( pData + l, r - l + 1 );
return; return;
} }
while ( 1 ) while ( 1 )
...@@ -569,7 +569,7 @@ void Abc_QuickSort2Dec_rec( word * pData, int l, int r ) ...@@ -569,7 +569,7 @@ void Abc_QuickSort2Dec_rec( word * pData, int l, int r )
assert( l < r ); assert( l < r );
if ( r - l < 10 ) if ( r - l < 10 )
{ {
Iso_SelectSortDec( pData + l, r - l + 1 ); Abc_SelectSortDec( pData + l, r - l + 1 );
return; return;
} }
while ( 1 ) while ( 1 )
...@@ -596,7 +596,7 @@ void Abc_QuickSort3Inc_rec( word * pData, int l, int r ) ...@@ -596,7 +596,7 @@ void Abc_QuickSort3Inc_rec( word * pData, int l, int r )
assert( l < r ); assert( l < r );
if ( r - l < 10 ) if ( r - l < 10 )
{ {
Iso_SelectSortInc( pData + l, r - l + 1 ); Abc_SelectSortInc( pData + l, r - l + 1 );
return; return;
} }
while ( 1 ) while ( 1 )
...@@ -631,7 +631,7 @@ void Abc_QuickSort3Dec_rec( word * pData, int l, int r ) ...@@ -631,7 +631,7 @@ void Abc_QuickSort3Dec_rec( word * pData, int l, int r )
assert( l < r ); assert( l < r );
if ( r - l < 10 ) if ( r - l < 10 )
{ {
Iso_SelectSortDec( pData + l, r - l + 1 ); Abc_SelectSortDec( pData + l, r - l + 1 );
return; return;
} }
while ( 1 ) while ( 1 )
...@@ -678,7 +678,7 @@ void Abc_QuickSort2( word * pData, int nSize, int fDecrease ) ...@@ -678,7 +678,7 @@ void Abc_QuickSort2( word * pData, int nSize, int fDecrease )
} }
void Abc_QuickSort3( word * pData, int nSize, int fDecrease ) void Abc_QuickSort3( word * pData, int nSize, int fDecrease )
{ {
int i, fVerify = 0; int i, fVerify = 1;
if ( fDecrease ) if ( fDecrease )
{ {
Abc_QuickSort2Dec_rec( pData, 0, nSize - 1 ); Abc_QuickSort2Dec_rec( pData, 0, nSize - 1 );
......
src/proof/cec/cecCore.c
...@@ -400,7 +400,7 @@ p->timeSim += clock() - clk; ...@@ -400,7 +400,7 @@ p->timeSim += clock() - clk;
// Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 ); // Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
if ( pPars->fVeryVerbose ) if ( pPars->fVeryVerbose )
Gia_ManPrintStats( pSrm, 0 ); Gia_ManPrintStats( pSrm, 0, 0 );
if ( Gia_ManCoNum(pSrm) == 0 ) if ( Gia_ManCoNum(pSrm) == 0 )
{ {
Gia_ManStop( pSrm ); Gia_ManStop( pSrm );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment