diff options
Diffstat (limited to 'src/aig/saig/saigAbs2.c')
| -rw-r--r-- | src/aig/saig/saigAbs2.c | 237 |
1 files changed, 237 insertions, 0 deletions
diff --git a/src/aig/saig/saigAbs2.c b/src/aig/saig/saigAbs2.c new file mode 100644 index 00000000..a4d0f973 --- /dev/null +++ b/src/aig/saig/saigAbs2.c @@ -0,0 +1,237 @@ +/**CFile**************************************************************** + + FileName [saigAbs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Counter-example-based abstraction with constraints.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "ssw.h" +#include "fra.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Saig_ManFindFirstFlop( Aig_Man_t * p ); +extern Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, + int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, + int * piRetValue, int * pnFrames ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the array of constraint numbers that are violated.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManFindViolatedConstrs( Aig_Man_t * p, Abc_Cex_t * pCexAbs ) +{ + Vec_Int_t * vFailed; + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int * pPoMap, i, k, iBit; + pPoMap = ABC_CALLOC( int, Saig_ManPoNum(p) ); + Aig_ManCleanMarkA(p); + Saig_ManForEachLo( p, pObj, i ) + pObj->fMarkA = 0; + assert( pCexAbs->nBits == pCexAbs->nRegs + (pCexAbs->iFrame + 1) * pCexAbs->nPis ); + for ( i = 0; i <= pCexAbs->iFrame; i++ ) + { + iBit = pCexAbs->nRegs + i * pCexAbs->nPis; + Saig_ManForEachPi( p, pObj, k ) + pObj->fMarkA = Aig_InfoHasBit(pCexAbs->pData, iBit++); + Aig_ManForEachNode( p, pObj, k ) + pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( p, pObj, k ) + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj); + Saig_ManForEachPo( p, pObj, k ) + pPoMap[k] |= pObj->fMarkA; + Saig_ManForEachLiLo( p, pObjRi, pObjRo, k ) + pObjRo->fMarkA = pObjRi->fMarkA; + } + Aig_ManCleanMarkA(p); + // collect numbers of failed constraints + vFailed = Vec_IntAlloc( Saig_ManPoNum(p) ); + Saig_ManForEachPo( p, pObj, k ) + if ( pPoMap[k] ) + Vec_IntPush( vFailed, k ); + ABC_FREE( pPoMap ); + return vFailed; +} + +/**Function************************************************************* + + Synopsis [Computes the flops to remain after abstraction.] + + Description [Updates the set of included constraints.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManConCexAbstractionFlops( Aig_Man_t * pInit, Gia_ParAbs_t * pPars, Vec_Int_t * vConstrs ) +{ + int nUseStart = 0; + Aig_Man_t * pCur, * pAbs, * pTemp; + Vec_Int_t * vFlops, * vFlopsCopy, * vConstrsToAdd; + int i, Entry, iFlop, Iter, clk = clock(), clk2 = clock(); + assert( Aig_ManRegNum(pInit) > 0 ); + if ( pPars->fVerbose ) + printf( "Performing counter-example-based refinement with constraints.\n" ); +// Aig_ManSetPioNumbers( p ); + // create constrained AIG + pCur = Saig_ManDupFoldConstrs( pInit, vConstrs ); + assert( Saig_ManPoNum(pCur) == 1 ); + printf( "cur>>> " ); Aig_ManPrintStats( pCur ); + // start the flop map + iFlop = Saig_ManFindFirstFlop( pCur ); + assert( iFlop >= 0 ); +// vFlops = Vec_IntStartNatural( 1 ); + vFlops = Vec_IntAlloc( 1 ); + Vec_IntPush( vFlops, iFlop ); + // create the abstraction + pAbs = Saig_ManDeriveAbstraction( pCur, vFlops ); + printf( "abs>>> " ); Aig_ManPrintStats( pAbs ); + if ( !pPars->fVerbose ) + { + printf( "Init : " ); + Aig_ManPrintStats( pAbs ); + } + printf( "Refining abstraction...\n" ); + for ( Iter = 0; ; Iter++ ) + { + while ( 1 ) + { + vFlopsCopy = Vec_IntDup( vFlops ); + pTemp = Saig_ManCexRefine( pCur, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone ); + if ( pTemp == NULL ) + { + Vec_IntFree( vFlopsCopy ); + break; + } + vConstrsToAdd = Saig_ManFindViolatedConstrs( pInit, pAbs->pSeqModel ); + if ( Vec_IntSize(vConstrsToAdd) == 0 ) + { + Vec_IntFree( vConstrsToAdd ); + Vec_IntFree( vFlopsCopy ); + break; + } + // add the constraints to the base set + Vec_IntForEachEntry( vConstrsToAdd, Entry, i ) + { +// assert( Vec_IntFind(vConstrs, Entry) == -1 ); + Vec_IntPushUnique( vConstrs, Entry ); + } + printf( "Adding %3d constraints. The total is %3d (out of %3d).\n", + Vec_IntSize(vConstrsToAdd), Vec_IntSize(vConstrs), Saig_ManPoNum(pInit)-1 ); + Vec_IntFree( vConstrsToAdd ); + // update the current one + Aig_ManStop( pCur ); + pCur = Saig_ManDupFoldConstrs( pInit, vConstrs ); + printf( "cur>>> " ); Aig_ManPrintStats( pCur ); + // update the flop map + Vec_IntFree( vFlops ); + vFlops = vFlopsCopy; +// Vec_IntFree( vFlopsCopy ); +// vFlops = vFlops; + // update abstraction + Aig_ManStop( pAbs ); + pAbs = Saig_ManDeriveAbstraction( pCur, vFlops ); + printf( "abs>>> " ); Aig_ManPrintStats( pAbs ); + } + Aig_ManStop( pAbs ); + if ( pTemp == NULL ) + break; + pAbs = pTemp; + printf( "ITER %4d : ", Iter ); + if ( !pPars->fVerbose ) + Aig_ManPrintStats( pAbs ); + // output the intermediate result of abstraction + Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); +// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); + // check if the ratio is reached + if ( 100.0*(Aig_ManRegNum(pCur)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(pCur) < 1.0*pPars->nRatio ) + { + printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); + Aig_ManStop( pAbs ); + pAbs = NULL; + Vec_IntFree( vFlops ); + vFlops = NULL; + break; + } + } + ABC_FREE( pInit->pSeqModel ); + pInit->pSeqModel = pCur->pSeqModel; + pCur->pSeqModel = NULL; + Aig_ManStop( pCur ); + return vFlops; +} + +/**Function************************************************************* + + Synopsis [Performs counter-example-based abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManConCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +{ + Vec_Int_t * vFlops, * vConstrs; + Aig_Man_t * pCur, * pAbs = NULL; + assert( Saig_ManPoNum(p) > 1 ); // should contain constraint outputs + // start included constraints + vConstrs = Vec_IntAlloc( 100 ); + // perform refinement + vFlops = Saig_ManConCexAbstractionFlops( p, pPars, vConstrs ); + // write the final result + if ( vFlops ) + { + pCur = Saig_ManDupFoldConstrs( p, vConstrs ); + pAbs = Saig_ManDeriveAbstraction( pCur, vFlops ); + Aig_ManStop( pCur ); + + Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); + printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); + Vec_IntFree( vFlops ); + } + Vec_IntFree( vConstrs ); + return pAbs; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |