/**CFile**************************************************************** FileName [saigAbsCba.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Sequential AIG package.] Synopsis [CEX-based abstraction.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: saigAbsCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "saig.h" #include "src/aig/gia/giaAig.h" #include "src/aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// // local manager typedef struct Saig_ManCba_t_ Saig_ManCba_t; struct Saig_ManCba_t_ { // user data Aig_Man_t * pAig; // user's AIG Abc_Cex_t * pCex; // user's CEX int nInputs; // the number of first inputs to skip int fVerbose; // verbose flag // unrolling Aig_Man_t * pFrames; // unrolled timeframes Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs // additional information Vec_Vec_t * vReg2Frame; // register to frame mapping Vec_Vec_t * vReg2Value; // register to value mapping }; //////////////////////////////////////////////////////////////////////// /// 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 = Abc_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)Abc_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.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Saig_ManDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value ) { Vec_Int_t * vLevel; Aig_Man_t * pAigNew; Aig_Obj_t * pObj, * pMiter; int i, k, Lit; assert( pAig->nConstrs == 0 ); // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) ); pAigNew->pName = Abc_UtilStrsav( pAig->pName ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); // create variables for PIs Aig_ManForEachPi( pAig, pObj, i ) pObj->pData = Aig_ObjCreatePi( pAigNew ); // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // create POs for cubes Vec_VecForEachLevelInt( vReg2Value, vLevel, i ) { pMiter = Aig_ManConst1( pAigNew ); Vec_IntForEachEntry( vLevel, Lit, k ) { pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) ); pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) ); } Aig_ObjCreatePo( pAigNew, pMiter ); } // transfer to register outputs Saig_ManForEachLi( pAig, pObj, i ) Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); // finalize Aig_ManCleanup( pAigNew ); Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); return pAigNew; } /**Function************************************************************* Synopsis [Maps array of frame PI IDs into array of additional PI IDs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Saig_ManCbaReason2Inputs( Saig_ManCba_t * p, Vec_Int_t * vReasons ) { Vec_Int_t * vOriginal, * vVisited; int i, Entry; vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) ); vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); Vec_IntForEachEntry( vReasons, Entry, i ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); assert( iInput >= p->nInputs && iInput < Aig_ManPiNum(p->pAig) ); if ( Vec_IntEntry(vVisited, iInput) == 0 ) Vec_IntPush( vOriginal, iInput - p->nInputs ); Vec_IntAddToEntry( vVisited, iInput, 1 ); } Vec_IntFree( vVisited ); return vOriginal; } /**Function************************************************************* Synopsis [Creates the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons ) { Abc_Cex_t * pCare; int i, Entry, iInput, iFrame; pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); Vec_IntForEachEntry( vReasons, Entry, i ) { assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); } /* for ( iFrame = 0; iFrame <= pCare->iFrame; iFrame++ ) { int Count = 0; for ( i = 0; i < pCare->nPis; i++ ) Count += Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i); printf( "%d ", Count ); } printf( "\n" ); */ return pCare; } /**Function************************************************************* Synopsis [Returns reasons for the property to fail.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons ) { if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return; Aig_ObjSetTravIdCurrent(p, pObj); if ( Aig_ObjIsConst1(pObj) ) return; if ( Aig_ObjIsPi(pObj) ) { Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); return; } assert( Aig_ObjIsNode(pObj) ); if ( pObj->fPhase ) { Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); } else { int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase; assert( !fPhase0 || !fPhase1 ); if ( !fPhase0 && fPhase1 ) Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); else if ( fPhase0 && !fPhase1 ) Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); else { int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); if ( iPrio0 <= iPrio1 ) Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); else Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); } } } /**Function************************************************************* Synopsis [Returns reasons for the property to fail.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p ) { Aig_Obj_t * pObj; Vec_Int_t * vPrios, * vReasons; int i; // set PI values according to CEX vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) ); Aig_ManConst1(p->pFrames)->fPhase = 1; Aig_ManForEachPi( p->pFrames, pObj, i ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); } // traverse and set the priority Aig_ManForEachNode( p->pFrames, pObj, i ) { int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase; int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); pObj->fPhase = fPhase0 && fPhase1; if ( fPhase0 && fPhase1 ) // both are one Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) ); else if ( !fPhase0 && fPhase1 ) Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 ); else if ( fPhase0 && !fPhase1 ) Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 ); else // both are zero Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) ); } // check the property output pObj = Aig_ManPo( p->pFrames, 0 ); pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; assert( !pObj->fPhase ); // select the reason vReasons = Vec_IntAlloc( 100 ); Aig_ManIncrementTravId( p->pFrames ); Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons ); Vec_IntFree( vPrios ); // assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) ); return vReasons; } /**Function************************************************************* Synopsis [Collect nodes in the unrolled timeframes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Saig_ManCbaUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots ) { if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); if ( Aig_ObjIsPo(pObj) ) Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); else if ( Aig_ObjIsNode(pObj) ) { Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots ); } if ( vRoots && Saig_ObjIsLo( pAig, pObj ) ) Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) ); Vec_IntPush( vObjs, Aig_ObjId(pObj) ); } /**Function************************************************************* Synopsis [Derive unrolled timeframes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A, Vec_Vec_t ** pvReg2Frame ) { Aig_Man_t * pFrames; // unrolled timeframes Vec_Vec_t * vFrameCos; // the list of COs per frame Vec_Vec_t * vFrameObjs; // the list of objects per frame Vec_Int_t * vRoots, * vObjs; Aig_Obj_t * pObj; int i, f; // sanity checks assert( Saig_ManPiNum(pAig) == pCex->nPis ); assert( Saig_ManRegNum(pAig) == pCex->nRegs ); assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) ); // map PIs of the unrolled frames into PIs of the original design *pvMapPiF2A = Vec_IntAlloc( 1000 ); // collect COs and Objs visited in each frame vFrameCos = Vec_VecStart( pCex->iFrame+1 ); vFrameObjs = Vec_VecStart( pCex->iFrame+1 ); // initialized the topmost frame pObj = Aig_ManPo( pAig, pCex->iPo ); Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) ); for ( f = pCex->iFrame; f >= 0; f-- ) { // collect nodes starting from the roots Aig_ManIncrementTravId( pAig ); vRoots = Vec_VecEntryInt( vFrameCos, f ); Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) Saig_ManCbaUnrollCollect_rec( pAig, pObj, Vec_VecEntryInt(vFrameObjs, f), (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) ); //printf( "%d ", Vec_VecLevelSize(vFrameCos, f) ); } //printf( "\n" ); // derive unrolled timeframes pFrames = Aig_ManStart( 10000 ); pFrames->pName = Abc_UtilStrsav( pAig->pName ); pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // initialize the flops Saig_ManForEachLo( pAig, pObj, i ) pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) ); // iterate through the frames for ( f = 0; f <= pCex->iFrame; f++ ) { // construct vObjs = Vec_VecEntryInt( vFrameObjs, f ); Aig_ManForEachObjVec( vObjs, pAig, pObj, i ) { if ( Aig_ObjIsNode(pObj) ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); else if ( Aig_ObjIsPo(pObj) ) pObj->pData = Aig_ObjChild0Copy(pObj); else if ( Aig_ObjIsConst1(pObj) ) pObj->pData = Aig_ManConst1(pFrames); else if ( Saig_ObjIsPi(pAig, pObj) ) { if ( Aig_ObjPioNum(pObj) < nInputs ) { int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); } else { pObj->pData = Aig_ObjCreatePi( pFrames ); Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) ); Vec_IntPush( *pvMapPiF2A, f ); } } } if ( f == pCex->iFrame ) break; // transfer vRoots = Vec_VecEntryInt( vFrameCos, f ); Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) { Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData; if ( *pvReg2Frame ) { Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjId(pObj) ); // record LO Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjToLit((Aig_Obj_t *)pObj->pData) ); // record its literal } } } // create output pObj = Aig_ManPo( pAig, pCex->iPo ); Aig_ObjCreatePo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) ); Aig_ManSetRegNum( pFrames, 0 ); // cleanup Vec_VecFree( vFrameCos ); Vec_VecFree( vFrameObjs ); // finallize Aig_ManCleanup( pFrames ); // return return pFrames; } /**Function************************************************************* Synopsis [Creates refinement manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Saig_ManCba_t * Saig_ManCbaStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ) { Saig_ManCba_t * p; p = ABC_CALLOC( Saig_ManCba_t, 1 ); p->pAig = pAig; p->pCex = pCex; p->nInputs = nInputs; p->fVerbose = fVerbose; return p; } /**Function************************************************************* Synopsis [Destroys refinement manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Saig_ManCbaStop( Saig_ManCba_t * p ) { Vec_VecFreeP( &p->vReg2Frame ); Vec_VecFreeP( &p->vReg2Value ); Aig_ManStopP( &p->pFrames ); Vec_IntFreeP( &p->vMapPiF2A ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Destroys refinement manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Saig_ManCbaShrink( Saig_ManCba_t * p ) { Aig_Man_t * pManNew; Aig_Obj_t * pObjLi, * pObjFrame; Vec_Int_t * vLevel, * vLevel2; int f, k, ObjId, Lit; // assuming that important objects are labeled in Saig_ManCbaFindReason() Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, f ) { Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k ) { pObjFrame = Aig_ManObj( p->pFrames, Abc_Lit2Var(Lit) ); if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) ) continue; pObjLi = Aig_ManObj( p->pAig, ObjId ); assert( Saig_ObjIsLi(p->pAig, pObjLi) ); Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjPioNum(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) ); } } // print statistics Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, k ) { vLevel2 = Vec_VecEntryInt( p->vReg2Value, k ); printf( "Level = %4d StateBits = %4d (%6.2f %%) CareBits = %4d (%6.2f %%)\n", k, Vec_IntSize(vLevel)/2, 100.0 * (Vec_IntSize(vLevel)/2) / Aig_ManRegNum(p->pAig), Vec_IntSize(vLevel2), 100.0 * Vec_IntSize(vLevel2) / Aig_ManRegNum(p->pAig) ); } // try reducing the frames pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value ); Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 ); Aig_ManStop( pManNew ); } /**Function************************************************************* Synopsis [SAT-based refinement of the counter-example.] Description [The first parameter (nInputs) indicates how many first primary inputs to skip without considering as care candidates.] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ) { Saig_ManCba_t * p; Vec_Int_t * vReasons; Abc_Cex_t * pCare; int clk = clock(); clk = clock(); p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose ); // p->vReg2Frame = Vec_VecStart( pCex->iFrame ); // p->vReg2Value = Vec_VecStart( pCex->iFrame ); p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame ); vReasons = Saig_ManCbaFindReason( p ); if ( p->vReg2Frame ) Saig_ManCbaShrink( p ); //if ( fVerbose ) //Aig_ManPrintStats( p->pFrames ); if ( fVerbose ) { Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons ); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); Vec_IntFree( vRes ); ABC_PRT( "Time", clock() - clk ); } pCare = Saig_ManCbaReason2Cex( p, vReasons ); Vec_IntFree( vReasons ); Saig_ManCbaStop( p ); if ( fVerbose ) { printf( "Real " ); Abc_CexPrintStats( pCex ); } if ( fVerbose ) { printf( "Care " ); Abc_CexPrintStats( pCare ); } return pCare; } /**Function************************************************************* Synopsis [Returns the array of PIs for flops that should not be absracted.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) { Saig_ManCba_t * p; Vec_Int_t * vRes, * vReasons; int clk; if ( Saig_ManPiNum(pAig) != pCex->nPis ) { printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n", Aig_ManPiNum(pAig), pCex->nPis ); return NULL; } clk = clock(); p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose ); p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame ); vReasons = Saig_ManCbaFindReason( p ); vRes = Saig_ManCbaReason2Inputs( p, vReasons ); if ( fVerbose ) { printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); } Vec_IntFree( vReasons ); Saig_ManCbaStop( p ); return vRes; } /**Function************************************************************* Synopsis [Checks the abstracted model for a counter-example.] Description [Returns the array of abstracted flops that should be added to the abstraction.] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars ) { Vec_Int_t * vAbsFfsToAdd; int RetValue, clk = clock(); // assert( pAbs->nRegs > 0 ); // perform BMC RetValue = Saig_ManBmcScalable( pAbs, pPars ); if ( RetValue == -1 ) // time out - nothing to add { printf( "Resource limit is reached during BMC.\n" ); assert( pAbs->pSeqModel == NULL ); return Vec_IntAlloc( 0 ); } if ( pAbs->pSeqModel == NULL ) { printf( "BMC did not detect a CEX with the given depth.\n" ); return Vec_IntAlloc( 0 ); } if ( pPars->fVerbose ) Abc_CexPrintStats( pAbs->pSeqModel ); // CEX is detected - refine the flops vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAbs, nInputs, pAbs->pSeqModel, pPars->fVerbose ); if ( Vec_IntSize(vAbsFfsToAdd) == 0 ) { Vec_IntFree( vAbsFfsToAdd ); return NULL; } if ( pPars->fVerbose ) { 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; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END