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

Adding CEC command &splitprove.

This commit is contained in:
Alan Mishchenko 2014-06-04 12:00:37 -07:00
parent 97bd9d8f1b
commit f2818ddb83
2 changed files with 31 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -32876,10 +32876,10 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose );
int c, nTimeOut = 1, nIterMax = 0, fVerbose = 0;
extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose );
int c, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "TIvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "TILvh" ) ) != EOF )
{
switch ( c )
{
@ -32905,6 +32905,20 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nIterMax < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
LookAhead = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( LookAhead <= 0 || LookAhead > 100 )
{
Abc_Print( -1, "Look-ahead value (\"-L <num>\") should be between 1 and 100.\n", LookAhead );
goto usage;
}
break;
case 'v':
fVerbose ^= 1;
break;
@ -32924,14 +32938,15 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" );
return 1;
}
Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, fVerbose );
Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, LookAhead, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &splitprove [-TI num] [-vh]\n" );
Abc_Print( -2, "usage: &splitprove [-TIL num] [-vh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
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-h : print the command usage\n");
return 1;

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

@ -204,12 +204,14 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int Gia_SplitCofVar2( Gia_Man_t * p )
int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead )
{
abctime clk = Abc_Clock();
Gia_Man_t * pPart;
int * pOrder = Gia_PermuteSpecialOrder( p );
int Cost0, Cost1, CostBest = ABC_INFINITY;
int i, iBest = -1, LookAhead = 10;
int i, iBest = -1;
LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
for ( i = 0; i < LookAhead; i++ )
{
pPart = Gia_ManDupCofactor( p, pOrder[i], 0 );
@ -222,9 +224,14 @@ int Gia_SplitCofVar2( Gia_Man_t * p )
if ( CostBest > Cost0 + Cost1 )
CostBest = Cost0 + Cost1, iBest = pOrder[i];
// printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n",
// i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
// Cost0, Cost1, Cost0+Cost1 );
}
ABC_FREE( pOrder );
assert( iBest >= 0 );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return iBest;
}
@ -359,7 +366,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose )
int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
{
abctime clk, clkTotal = Abc_Clock();
Gia_Man_t * pPart0, * pPart1, * pLast;
@ -387,7 +394,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose )
pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
// determine cofactoring variable
Depth = Vec_IntSize(pLast->vCofVars);
iVar = Gia_SplitCofVar2( pLast );
iVar = Gia_SplitCofVar2( pLast, LookAhead );
// cofactor
pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
// create variable