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-02-11 22:30:04 -08:00
parent 95d7b478fd
commit 49c5beefd4
3 changed files with 24 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/gia/gia.h
View File

@ -201,9 +201,9 @@ struct Gia_ParSim_t_
typedef struct Gia_ParVta_t_ Gia_ParVta_t;
struct Gia_ParVta_t_
{
int nFramesStart; // starting frame
int nFramesMax; // maximum frames
int nFramesOver; // overlap frames
int nFramesStart; // starting frame
int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted

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

@ -145,13 +145,13 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesStart = 5; // starting frame
p->nFramesOver = 4; // overlap frames
p->nFramesMax = 0; // maximum frames
p->nFramesStart = 5; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
p->fUseTermVars = 0; // use terminal variables
p->fUseTermVars = 1; // use terminal variables
p->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered
}
@ -1409,7 +1409,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
printf( "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
printf( "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
p->pPars->nFramesStart, p->pPars->nFramesOver, p->pPars->nFramesMax,
p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax,
p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
printf( "Frame Abs Confl Cex Core F0 F1 F2 F3 ...\n" );
}
@ -1435,7 +1435,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
// load the time frame
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesOver, p->pPars->nFramesStart); i++ )
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, p->pPars->nFramesStart); i++ )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )

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

@ -26711,21 +26711,10 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFPCTRtvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCTRtvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesStart < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
@ -26737,15 +26726,26 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesStart < 0 )
goto usage;
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]);
pPars->nFramesPast = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesOver < 0 )
if ( pPars->nFramesPast < 0 )
goto usage;
break;
case 'C':
@ -26824,11 +26824,11 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &vta [-SFPCTR num] [-tvh]\n" );
Abc_Print( -2, "usage: &vta [-FSPCTR num] [-tvh]\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-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-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
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-R num : stop when less than this %% of object is abstracted (0<=num<=100) [default = %d]\n", pPars->nRatioMin );