/**CFile**************************************************************** FileName [giaAbs.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [Counter-example-guided abstraction refinement.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" #include "giaAig.h" #include "aig/saig/saig.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [This procedure sets default parameters.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p ) { memset( p, 0, sizeof(Gia_ParAbs_t) ); p->Algo = 0; // algorithm: CBA p->nFramesMax = 10; // timeframes for PBA p->nConfMax = 10000; // conflicts for PBA p->fDynamic = 1; // dynamic unfolding for PBA p->fConstr = 0; // use constraints p->nFramesBmc = 250; // timeframes for BMC p->nConfMaxBmc = 5000; // conflicts for BMC p->nStableMax = 1000000; // the number of stable frames to quit p->nRatio = 10; // ratio of flops to quit p->nBobPar = 1000000; // the number of frames before trying to quit p->fUseBdds = 0; // use BDDs to refine abstraction p->fUseDprove = 0; // use 'dprove' to refine abstraction p->fUseStart = 1; // use starting frame p->fVerbose = 0; // verbose output p->fVeryVerbose= 0; // printing additional information p->Status = -1; // the problem status p->nFramesDone = -1; // the number of rames covered } /**Function************************************************************* Synopsis [Transform flop list into flop map.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops ) { Vec_Int_t * vFlopClasses; int i, Entry; vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); Vec_IntForEachEntry( vFlops, Entry, i ) Vec_IntWriteEntry( vFlopClasses, Entry, 1 ); return vFlopClasses; } /**Function************************************************************* Synopsis [Transform flop map into flop list.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses ) { Vec_Int_t * vFlops; int i, Entry; vFlops = Vec_IntAlloc( 100 ); Vec_IntForEachEntry( vFlopClasses, Entry, i ) if ( Entry ) Vec_IntPush( vFlops, i ); return vFlops; } /**Function************************************************************* Synopsis [Starts abstraction by computing latch map.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) { Vec_Int_t * vFlops; Aig_Man_t * pNew; if ( pGia->vFlopClasses != NULL ) { printf( "Gia_ManCexAbstractionStart(): Abstraction latch map is present but will be rederived.\n" ); Vec_IntFreeP( &pGia->vFlopClasses ); } pNew = Gia_ManToAig( pGia, 0 ); vFlops = Saig_ManCexAbstractionFlops( pNew, pPars ); pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; Aig_ManStop( pNew ); if ( vFlops ) { pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); Vec_IntFree( vFlops ); } } /**Function************************************************************* Synopsis [Refines abstraction using the latch map.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ) { Aig_Man_t * pNew; Vec_Int_t * vFlops; if ( pGia->vFlopClasses == NULL ) { printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" ); return -1; } pNew = Gia_ManToAig( pGia, 0 ); vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) ) { pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; Vec_IntFree( vFlops ); Aig_ManStop( pNew ); return 0; } Vec_IntFree( pGia->vFlopClasses ); pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); Vec_IntFree( vFlops ); Aig_ManStop( pNew ); return -1; } /**Function************************************************************* Synopsis [Transform flop list into flop map.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew ) { Vec_Int_t * vSelected; int i, Entry; vSelected = Vec_IntAlloc( Vec_IntSize(vFlopsNew) ); Vec_IntForEachEntry( vFlopsNew, Entry, i ) Vec_IntPush( vSelected, Vec_IntEntry(vFlops, Entry) ); return vSelected; } /**Function************************************************************* Synopsis [Adds flops that should be present in the abstraction.] Description [The second argument (vAbsFfsToAdd) is the array of numbers of previously abstrated flops (flops replaced by PIs in the abstracted model) that should be present in the abstraction as real flops.] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManFlopsAddToClasses( Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd ) { Vec_Int_t * vMapEntries; int i, Entry, iFlopNum; // 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 ); // add these flops as real flops Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i ) { iFlopNum = Vec_IntEntry( vMapEntries, Entry ); assert( Vec_IntEntry( vFlopClasses, iFlopNum ) == 0 ); Vec_IntWriteEntry( vFlopClasses, iFlopNum, 1 ); } Vec_IntFree( vMapEntries ); } /**Function************************************************************* Synopsis [Derive unrolled timeframes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ 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, * vAbsFfsToAddBest; // check if flop classes are given if ( pGia->vFlopClasses == NULL ) { Abc_Print( 0, "Initial flop map is not given. Trivial abstraction is assumed.\n" ); pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); } // derive abstraction pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses ); pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); // refine abstraction using CBA vAbsFfsToAdd = Saig_ManCbaPerform( pAig, Gia_ManPiNum(pGia), p ); if ( vAbsFfsToAdd == NULL ) // found true CEX { assert( pAig->pSeqModel != NULL ); printf( "Refinement did not happen. Discovered a true counter-example.\n" ); printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAig), Gia_ManPiNum(pGia) ); // derive new counter-example pOrig = Gia_ManToAigSimple( pGia ); pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel ); Aig_ManStop( pOrig ); 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 ); Vec_IntFree( vAbsFfsToAdd ); if ( p->fVerbose ) Gia_ManPrintStats( pGia, 0, 0 ); return -1; } /**Function************************************************************* Synopsis [Derive unrolled timeframes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ) { Gia_Man_t * pAbs; Aig_Man_t * pAig, * pOrig; Vec_Int_t * vFlops, * vFlopsNew, * vSelected; int RetValue; if ( pGia->vFlopClasses == NULL ) { printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" ); return 0; } // derive abstraction pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses ); // refine abstraction using PBA pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, nTimeLimit, fVerbose, piFrame ); // derive new classes if ( pAig->pSeqModel == NULL ) { // check if there is no timeout if ( vFlopsNew != NULL ) { // the problem is UNSAT vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew ); Vec_IntFree( pGia->vFlopClasses ); pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); Vec_IntFree( vSelected ); Vec_IntFree( vFlopsNew ); Vec_IntFree( vFlops ); } RetValue = -1; } else if ( vFlopsNew == NULL ) { // found real counter-example assert( pAig->pSeqModel != NULL ); printf( "Refinement did not happen. Discovered a true counter-example.\n" ); printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAig), Gia_ManPiNum(pGia) ); // derive new counter-example pOrig = Gia_ManToAigSimple( pGia ); pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel ); Aig_ManStop( pOrig ); RetValue = 0; } else { // found counter-eample for the abstracted model // update flop classes Vec_Int_t * vAbsFfsToAdd = vFlopsNew; Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); Vec_IntFree( vAbsFfsToAdd ); RetValue = -1; } Aig_ManStop( pAig ); if ( fVerbose ) Gia_ManPrintStats( pGia, 0, 0 ); return RetValue; } /**Function************************************************************* Synopsis [Derive unrolled timeframes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) { extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses, * vGateClassesOld = NULL; Aig_Man_t * pAig; // check if flop classes are given if ( pGia->vGateClasses == NULL ) Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" ); else { Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" ); vGateClassesOld = pGia->vGateClasses; pGia->vGateClasses = NULL; fNaiveCnf = 1; } // perform abstraction p->iFrame = -1; pAig = Gia_ManToAigSimple( pGia ); assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) ); vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose, &p->iFrame ); Aig_ManStop( pAig ); // update the map Vec_IntFreeP( &vGateClassesOld ); pGia->vGateClasses = vGateClasses; if ( p->fVerbose ) Gia_ManPrintStats( pGia, 0, 0 ); return 1; } /**Function************************************************************* Synopsis [Derive unrolled timeframes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ) { extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); extern Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses; Gia_Man_t * pGiaAbs; Aig_Man_t * pAig; // check if flop classes are given if ( pGia->vGateClasses == NULL ) { Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" ); pAig = Gia_ManToAigSimple( pGia ); } else { Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" ); pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); pAig = Gia_ManToAigSimple( pGiaAbs ); Gia_ManStop( pGiaAbs ); } // perform abstraction if ( fNewSolver ) vGateClasses = Aig_Gla3ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); else vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); Aig_ManStop( pAig ); // update the BMC depth if ( vGateClasses ) p->iFrame = p->nFramesMax; // update the abstraction map (hint: AIG and GIA have one-to-one obj ID match) if ( pGia->vGateClasses && vGateClasses ) { Gia_Obj_t * pObj; int i, Counter = 0; Gia_ManForEachObj1( pGia, pObj, i ) { if ( !~pObj->Value ) continue; if ( !Vec_IntEntry(pGia->vGateClasses, i) ) continue; // this obj was abstracted before assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) ); // if corresponding AIG object is not abstracted, remove abstraction if ( !Vec_IntEntry(vGateClasses, Abc_Lit2Var(pObj->Value)) ) { Vec_IntWriteEntry( pGia->vGateClasses, i, 0 ); Counter++; } } Vec_IntFree( vGateClasses ); if ( p->fVerbose ) Abc_Print( 1, "Repetition of abstraction removed %d entries from the old abstraction map.\n", Counter ); } else { Vec_IntFreeP( &pGia->vGateClasses ); pGia->vGateClasses = vGateClasses; } // clean up the abstraction map if ( pGia->vGateClasses ) { pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); Gia_ManStop( pGiaAbs ); } if ( p->fVerbose ) Gia_ManPrintStats( pGia, 0, 0 ); return 1; } /**Function************************************************************* Synopsis [Converting VTA vector to GLA vector.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ) { Gia_Obj_t * pObj; Vec_Int_t * vGla; int nObjMask, nObjs = Gia_ManObjNum(p); int i, Entry, nFrames = Vec_IntEntry( vVta, 0 ); assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); // get the bitmask nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; assert( nObjs <= nObjMask ); // go through objects vGla = Vec_IntStart( nObjs ); Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 ) { pObj = Gia_ManObj( p, (Entry & nObjMask) ); assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) ); Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 ); } Vec_IntWriteEntry( vGla, 0, nFrames ); return vGla; } /**Function************************************************************* Synopsis [Converting GLA vector to VTA vector.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ) { Vec_Int_t * vVta; int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p); int i, k, j, Entry, Counter, nGlaSize; //. get the GLA size nGlaSize = Vec_IntSum(vGla); // get the bitmask nObjBits = Abc_Base2Log(nObjs); nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; assert( nObjs <= nObjMask ); // go through objects vVta = Vec_IntAlloc( 1000 ); Vec_IntPush( vVta, nFrames ); Counter = nFrames + 2; for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize ) Vec_IntPush( vVta, Counter ); for ( i = 0; i < nFrames; i++ ) for ( k = 0; k <= i; k++ ) Vec_IntForEachEntry( vGla, Entry, j ) if ( Entry ) Vec_IntPush( vVta, (k << nObjBits) | j ); Counter = Vec_IntEntry(vVta, nFrames+1); assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); return vVta; } /**Function************************************************************* Synopsis [Converting GLA vector to FLA vector.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; Gia_ObjSetTravIdCurrent(p, pObj); Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 ); if ( Gia_ObjIsRo(p, pObj) ) return; assert( Gia_ObjIsAnd(pObj) ); Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla ); } /**Function************************************************************* Synopsis [Converting FLA vector to GLA vector.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ) { Vec_Int_t * vGla; Gia_Obj_t * pObj; int i; // mark const0 and relevant CI objects Gia_ManIncrementTravId( p ); Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p)); Gia_ManForEachPi( p, pObj, i ) Gia_ObjSetTravIdCurrent(p, pObj); Gia_ManForEachRo( p, pObj, i ) if ( !Vec_IntEntry(vFla, i) ) Gia_ObjSetTravIdCurrent(p, pObj); // label all objects reachable from the PO and selected flops vGla = Vec_IntStart( Gia_ManObjNum(p) ); Vec_IntWriteEntry( vGla, 0, 1 ); Gia_ManForEachPo( p, pObj, i ) Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); Gia_ManForEachRi( p, pObj, i ) if ( Vec_IntEntry(vFla, i) ) Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); return vGla; } /**Function************************************************************* Synopsis [Converting GLA vector to FLA vector.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ) { Vec_Int_t * vFla; Gia_Obj_t * pObj; int i; vFla = Vec_IntStart( Gia_ManRegNum(p) ); Gia_ManForEachRo( p, pObj, i ) if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) Vec_IntWriteEntry( vFla, i, 1 ); return vFla; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose ) { int i, Entry, CountUpTo, CountAll, CountRem, * pCounts; int nFrames = Vec_IntEntry( p->vGateClasses, 0 ); if ( nFrames < 2 ) { printf( "Gate-level abstraction is missing object count information.\n" ); return; } // collect info CountAll = 0; pCounts = ABC_CALLOC( int, nFrames + 1 ); assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) { Entry = Vec_IntEntry( p->vGateClasses, i ); assert( Entry >= 0 && Entry <= nFrames ); if ( Entry == 0 ) continue; CountAll++; pCounts[Entry]++; } // print entries CountUpTo = 0; for ( i = 0; i <= nFrames; i++ ) printf( "%d=%d(%d) ", i, pCounts[i], CountUpTo += pCounts[i] ); printf( "\n" ); // removing entries appearing only ones CountRem = 0; for ( i = 0; i < Gia_ManObjNum(p); i++ ) { if ( Vec_IntEntry( p->vGateClasses, i ) == 0 ) continue; if ( Vec_IntEntry( p->vGateClasses, i ) <= nPurifyRatio ) { CountRem++; Vec_IntWriteEntry( p->vGateClasses, i, 0 ); } } printf( "Removed %d entries appearing less or equal than %d times (out of %d).\n", CountRem, nPurifyRatio, CountAll ); ABC_FREE( pCounts ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END