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

Variable timeframe abstraction.

This commit is contained in:
Alan Mishchenko 2012-01-27 00:57:42 -08:00
parent ce0e8caf79
commit 7a87f20c18
2 changed files with 15 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaAbsVta.c
View File

@ -151,7 +151,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
p->nConfLimit = 0; // conflict limit p->nConfLimit = 0; // conflict limit
p->nTimeOut = 60; // timeout in seconds p->nTimeOut = 60; // timeout in seconds
p->fUseTermVars = 0; // use terminal variables p->fUseTermVars = 0; // use terminal variables
p->fVerbose = 1; // verbose flag p->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered p->iFrame = -1; // the number of frames covered
} }

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

@ -26408,7 +26408,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Gia_VtaSetDefaultParams( pPars ); Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTtvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "SFPCTtvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -26434,6 +26434,17 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFramesMax < 0 ) if ( pPars->nFramesMax < 0 )
goto usage; goto usage;
break; break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesOver = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesOver < 0 )
goto usage;
break;
case 'C': case 'C':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
@ -26499,10 +26510,11 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &vta [-SFCT num] [-tvh]\n" ); Abc_Print( -2, "usage: &vta [-SFPCT num] [-tvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesOver );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" ); Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );