luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding print-out to &splitprove to see impact of cof variable on AIG size.

This commit is contained in:
Alan Mishchenko 2014-06-07 13:14:23 -07:00
parent 2d38fc1608
commit 3c6def2915
2 changed files with 14 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/base/abci/abc.c
View File

@ -32892,10 +32892,10 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose );
int c, nProcs = 1, nTimeOut = 10, nIterMax = 0, LookAhead = 1, fVerbose = 0;
extern int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose );
int c, nProcs = 1, nTimeOut = 10, nIterMax = 0, LookAhead = 1, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PTILvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PTILvwh" ) ) != EOF )
{
switch ( c )
{
@ -32949,6 +32949,9 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -32965,18 +32968,19 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" );
return 1;
}
pAbc->Status = Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
pAbc->Status = Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose );
pAbc->pCex = pAbc->pGia->pCexComb; pAbc->pGia->pCexComb = NULL;
return 0;
usage:
Abc_Print( -2, "usage: &splitprove [-PTIL num] [-vh]\n" );
Abc_Print( -2, "usage: &splitprove [-PTIL num] [-vwh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs );
Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIterMax );
Abc_Print( -2, "\t-L num : maximum look-ahead during cofactoring [default = %d]\n", LookAhead );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

10
src/proof/cec/cecSplit.c
View File

@ -397,7 +397,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose )
{
abctime clkTotal = Abc_Clock();
Vec_Ptr_t * vStack;
@ -438,7 +438,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
if ( pLast->vCofVars == NULL )
pLast->vCofVars = Vec_IntAlloc( 100 );
// print results
if ( fVerbose )
if ( fVeryVerbose )
{
// Cec_GiaSplitPrintRefs( pLast );
printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
@ -558,7 +558,7 @@ void * Cec_GiaSplitWorkerThread( void * pArg )
assert( 0 );
return NULL;
}
int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose )
{
abctime clkTotal = Abc_Clock();
Par_ThData_t ThData[PAR_THR_MAX];
@ -575,7 +575,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
fflush( stdout );
if ( nProcs == 1 )
return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
@ -650,7 +650,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
Vec_PtrPush( vStack, pPart );
// print results
if ( fVerbose )
if ( fVeryVerbose )
{
// Cec_GiaSplitPrintRefs( pLast );
printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",