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

Added dumping abstracted model in &vta.

This commit is contained in:
Alan Mishchenko 2012-04-07 12:43:17 -07:00
parent c3d3ccf349
commit 48b47300e3
3 changed files with 43 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -210,6 +210,7 @@ struct Gia_ParVta_t_
int nRatioMin; // stop when less than this % of object is abstracted
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fDumpVabs; // dumps the abstracted model
int fVerbose; // verbose flag
int iFrame; // the number of frames covered
};

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

@ -1428,6 +1428,39 @@ void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose )
Gia_ManToBridgeBadAbs( stdout );
}
/**Function*************************************************************
Synopsis [Send abstracted model or send cancel.]
Description [Counter-example will be sent automatically when &vta terminates.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
{
Gia_Man_t * pAbs;
if ( fVerbose )
Abc_Print( 1, "Dumping abstracted model into file \"vabs.aig\"...\n" );
if ( !Abc_FrameIsBridgeMode() )
return;
// create obj classes
Vec_IntFreeP( &p->pGia->vObjClasses );
p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
// create gate classes
Vec_IntFreeP( &p->pGia->vGateClasses );
p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
Vec_IntFreeP( &p->pGia->vObjClasses );
// create abstrated model
pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
Vec_IntFreeP( &p->pGia->vGateClasses );
// send it out
Gia_WriteAiger( pAbs, "vabs.aig", 0, 0 );
Gia_ManStop( pAbs );
}
/**Function*************************************************************
Synopsis [Collect nodes/flops involved in different timeframes.]
@ -1568,6 +1601,9 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// send new one
Gia_VtaSendAbsracted( p, pPars->fVerbose );
fOneIsSent = 1;
// dump the model
if ( p->pPars->fDumpVabs )
Gia_VtaDumpAbsracted( p, pPars->fVerbose );
}
// check if the number of objects is below limit
if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )

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

@ -27222,7 +27222,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRtrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRtrdvh" ) ) != EOF )
{
switch ( c )
{
@ -27309,6 +27309,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fUseRollback ^= 1;
break;
case 'd':
pPars->fDumpVabs ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -27354,7 +27357,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-trvh]\n" );
Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-trdvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
@ -27365,6 +27368,7 @@ usage:
Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into file \"vabs.aig\" [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;