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

Added limit on the number of flops to add in one iteration of &abs_cba.

This commit is contained in:
Alan Mishchenko 2011-09-11 20:31:25 -05:00
parent a7acb2f104
commit 583bc4d71a
4 changed files with 118 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/aig/gia/giaAbs.c
View File

@ -273,7 +273,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
Vec_Int_t * vAbsFfsToAdd;
Vec_Int_t * vAbsFfsToAdd, * vAbsFfsToAddBest;
// check if flop classes are given
if ( pGia->vFlopClasses == NULL )
{
@ -298,6 +298,21 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
Aig_ManStop( pAig );
return 0;
}
// select the most useful flops among those to be added
if ( p->nFfToAddMax > 0 && Vec_IntSize(vAbsFfsToAdd) > p->nFfToAddMax )
{
// compute new flops
Aig_Man_t * pAigBig = Gia_ManToAigSimple( pGia );
vAbsFfsToAddBest = Saig_ManCbaFilterFlops( pAigBig, pAig->pSeqModel, pGia->vFlopClasses, vAbsFfsToAdd, p->nFfToAddMax );
Aig_ManStop( pAigBig );
assert( Vec_IntSize(vAbsFfsToAddBest) == p->nFfToAddMax );
if ( p->fVerbose )
printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vAbsFfsToAdd), Vec_IntSize(vAbsFfsToAddBest) );
// update
Vec_IntFree( vAbsFfsToAdd );
vAbsFfsToAdd = vAbsFfsToAddBest;
}
Aig_ManStop( pAig );
// update flop classes
Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );

2
src/aig/saig/saig.h
View File

@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
int nPisAbstract; // the number of PIs to abstract
int fSolveAll; // does not stop at the first SAT output
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fVerbose; // verbose
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
@ -131,6 +132,7 @@ extern Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses );
extern Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops );
extern Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs );
/*=== sswAbsCba.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose );
extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );

87
src/aig/saig/saigAbsCba.c
View File

@ -49,6 +49,90 @@ struct Saig_ManCba_t_
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Selects the best flops from the given array.]
Description [Selects the best 'nFfsToSelect' flops among the array
'vAbsFfsToAdd' of flops that should be added to the abstraction.
To this end, this procedure simulates the original AIG (pAig) using
the given CEX (pAbsCex), which was detected for the abstraction.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
int i, k, f, Entry, iBit, * pPerm;
assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
// map previously abstracted flops into their original numbers
vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry == 0 )
Vec_IntPush( vMapEntries, i );
// simulate one frame at a time
assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
// initialize the flops
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = 0;
for ( f = 0; f < pAbsCex->iFrame; f++ )
{
// override the flop values according to the cex
iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
Vec_IntForEachEntry( vMapEntries, Entry, k )
Saig_ManLo(pAig, Entry)->fMarkB = Aig_InfoHasBit(pAbsCex->pData, iBit + k);
// simulate
Aig_ManForEachNode( pAig, pObj, k )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachPo( pAig, pObj, k )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
// transfer
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
pObjRo->fMarkB = pObjRi->fMarkB;
// compare
iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
Vec_IntForEachEntry( vMapEntries, Entry, k )
if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Aig_InfoHasBit(pAbsCex->pData, iBit + k) )
Vec_IntAddToEntry( vFlopCosts, k, 1 );
}
// Vec_IntForEachEntry( vFlopCosts, Entry, i )
// printf( "%d ", Entry );
// printf( "\n" );
// remap the cost
vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
// sort the flops
pPerm = Abc_SortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
// shrink the array
vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
for ( i = 0; i < nFfsToSelect; i++ )
{
// printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
}
// printf( "\n" );
// cleanup
ABC_FREE( pPerm );
Vec_IntFree( vMapEntries );
Vec_IntFree( vFlopCosts );
Vec_IntFree( vFlopAddCosts );
Aig_ManCleanMarkB(pAig);
// return the computed flops
return vFfsToAddBest;
}
/**Function*************************************************************
Synopsis [Duplicate with literals.]
@ -637,7 +721,8 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
}
if ( pPars->fVerbose )
{
printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
printf( "Adding %d registers to the abstraction (total = %d). ",
Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return vAbsFfsToAdd;

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

@ -28597,7 +28597,7 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = pPars->nStart + 10;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
{
switch ( c )
{
@ -28634,6 +28634,17 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nConfLimit < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFfToAddMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFfToAddMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
@ -28671,11 +28682,12 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted flop map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
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");