From 583bc4d71a403028d60fd676ce72c3c6d1e2e7fe Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 11 Sep 2011 20:31:25 -0500 Subject: Added limit on the number of flops to add in one iteration of &abs_cba. --- src/aig/gia/giaAbs.c | 17 ++++++++- src/aig/saig/saig.h | 2 ++ src/aig/saig/saigAbsCba.c | 87 ++++++++++++++++++++++++++++++++++++++++++++++- src/base/abci/abc.c | 16 +++++++-- 4 files changed, 118 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 37f5e315..2b5414e7 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -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 ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 36b41daf..0914c993 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -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 ); diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 4d9cef57..32b9c129 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -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; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 951c91bb..9da96731 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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"); -- cgit v1.2.3