/**CFile**************************************************************** FileName [fraBmc.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [New FRAIG package.] Synopsis [Bounded model checking.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 30, 2007.] Revision [$Id: fraBmc.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] ***********************************************************************/ #include "fra.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// // simulation manager struct Fra_Bmc_t_ { // parameters int nPref; // the size of the prefix int nDepth; // the depth of the frames int nFramesAll; // the total number of timeframes // implications to be filtered Vec_Int_t * vImps; // AIG managers Aig_Man_t * pAig; // the original AIG manager Aig_Man_t * pAigFrames; // initialized timeframes Aig_Man_t * pAigFraig; // the fraiged initialized timeframes // mapping of nodes Aig_Obj_t ** pObjToFrames; // mapping of the original node into frames Aig_Obj_t ** pObjToFraig; // mapping of the frames node into fraig }; static inline Aig_Obj_t * Bmc_ObjFrames( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i]; } static inline void Bmc_ObjSetFrames( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; } static inline Aig_Obj_t * Bmc_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id]; } static inline void Bmc_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; } static inline Aig_Obj_t * Bmc_ObjChild0Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Returns 1 if the nodes are equivalent.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { Fra_Man_t * p = (Fra_Man_t *)pObj0->pData; Aig_Obj_t * pObjFrames0, * pObjFrames1; Aig_Obj_t * pObjFraig0, * pObjFraig1; int i; for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ ) { pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) ); pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) ); if ( pObjFrames0 == pObjFrames1 ) continue; pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) ); pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) ); if ( pObjFraig0 != pObjFraig1 ) return 0; } return 1; } /**Function************************************************************* Synopsis [Returns 1 if the node is costant.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ) { Fra_Man_t * p = (Fra_Man_t *)pObj->pData; return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) ); } /**Function************************************************************* Synopsis [Refines implications using BMC.] Description [The input is the combinational FRAIG manager, which is used to FRAIG the timeframes. ] SideEffects [] SeeAlso [] ***********************************************************************/ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc ) { Aig_Obj_t * pLeft, * pRight; Aig_Obj_t * pLeftT, * pRightT; Aig_Obj_t * pLeftF, * pRightF; int i, f, Imp, Left, Right; int fComplL, fComplR; assert( p->nFramesAll == 1 ); assert( p->pManAig == pBmc->pAigFrames ); Vec_IntForEachEntry( pBmc->vImps, Imp, i ) { if ( Imp == 0 ) continue; Left = Fra_ImpLeft(Imp); Right = Fra_ImpRight(Imp); // get the corresponding nodes pLeft = Aig_ManObj( pBmc->pAig, Left ); pRight = Aig_ManObj( pBmc->pAig, Right ); // iterate through the timeframes for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ ) { // get timeframe nodes pLeftT = Bmc_ObjFrames( pLeft, f ); pRightT = Bmc_ObjFrames( pRight, f ); // get the corresponding FRAIG nodes pLeftF = Fra_ObjFraig( Aig_Regular(pLeftT), 0 ); pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 ); // get the complemented attributes fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT); fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT); // check equality if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) { if ( fComplL == fComplR ) // x => x - always true continue; assert( fComplL != fComplR ); // consider 4 possibilities: // NOT(1) => 1 or 0 => 1 - always true // 1 => NOT(1) or 1 => 0 - never true // NOT(x) => x or x - not always true // x => NOT(x) or NOT(x) - not always true if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication continue; // disproved implication Vec_IntWriteEntry( pBmc->vImps, i, 0 ); break; } // check the implication if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 ) { Vec_IntWriteEntry( pBmc->vImps, i, 0 ); break; } } } Fra_ImpCompactArray( pBmc->vImps ); } /**Function************************************************************* Synopsis [Starts the BMC manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth ) { Fra_Bmc_t * p; p = ABC_ALLOC( Fra_Bmc_t, 1 ); memset( p, 0, sizeof(Fra_Bmc_t) ); p->pAig = pAig; p->nPref = nPref; p->nDepth = nDepth; p->nFramesAll = nPref + nDepth; p->pObjToFrames = ABC_ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) ); memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) ); return p; } /**Function************************************************************* Synopsis [Stops the BMC manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Fra_BmcStop( Fra_Bmc_t * p ) { Aig_ManStop( p->pAigFrames ); if ( p->pAigFraig ) Aig_ManStop( p->pAigFraig ); ABC_FREE( p->pObjToFrames ); ABC_FREE( p->pObjToFraig ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Constructs initialized timeframes of the AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos ) { Aig_Man_t * pAigFrames; Aig_Obj_t * pObj, * pObjNew; Aig_Obj_t ** pLatches; int i, k, f; // start the fraig package pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll ); pAigFrames->pName = Abc_UtilStrsav( p->pAig->pName ); pAigFrames->pSpec = Abc_UtilStrsav( p->pAig->pSpec ); // create PI nodes for the frames for ( f = 0; f < p->nFramesAll; f++ ) Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) ); for ( f = 0; f < p->nFramesAll; f++ ) Aig_ManForEachPiSeq( p->pAig, pObj, i ) Bmc_ObjSetFrames( pObj, f, Aig_ObjCreateCi(pAigFrames) ); // set initial state for the latches Aig_ManForEachLoSeq( p->pAig, pObj, i ) Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) ); // add timeframes pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); for ( f = 0; f < p->nFramesAll; f++ ) { // add internal nodes of this frame Aig_ManForEachNode( p->pAig, pObj, i ) { pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) ); Bmc_ObjSetFrames( pObj, f, pObjNew ); } if ( f == p->nFramesAll - 1 ) break; // save the latch input values k = 0; Aig_ManForEachLiSeq( p->pAig, pObj, i ) pLatches[k++] = Bmc_ObjChild0Frames(pObj,f); assert( k == Aig_ManRegNum(p->pAig) ); // insert them to the latch output values k = 0; Aig_ManForEachLoSeq( p->pAig, pObj, i ) Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] ); assert( k == Aig_ManRegNum(p->pAig) ); } ABC_FREE( pLatches ); if ( fKeepPos ) { for ( f = 0; f < p->nFramesAll; f++ ) Aig_ManForEachPoSeq( p->pAig, pObj, i ) Aig_ObjCreateCo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) ); Aig_ManCleanup( pAigFrames ); } else { // add POs to all the dangling nodes Aig_ManForEachObj( pAigFrames, pObjNew, i ) if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 ) Aig_ObjCreateCo( pAigFrames, pObjNew ); } // return the new manager return pAigFrames; } /**Function************************************************************* Synopsis [Performs BMC for the given AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) { Aig_Obj_t * pObj; int i, nImpsOld = 0; abctime clk = Abc_Clock(); assert( p->pBmc == NULL ); // derive and fraig the frames p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth ); p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 ); // if implications are present, configure the AIG manager to check them if ( p->pCla->vImps ) { p->pBmc->pAigFrames->pImpFunc = (void (*) (void*, void*))Fra_BmcFilterImplications; p->pBmc->pAigFrames->pImpData = p->pBmc; p->pBmc->vImps = p->pCla->vImps; nImpsOld = Vec_IntSize(p->pCla->vImps); } p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 ); p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies; p->pBmc->pAigFrames->pObjCopies = NULL; // annotate frames nodes with pointers to the manager Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i ) pObj->pData = p; // report the results if ( p->pPars->fVerbose ) { printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d. ", Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) ); ABC_PRT( "Time", Abc_Clock() - clk ); printf( "Before BMC: " ); // Fra_ClassesPrint( p->pCla, 0 ); printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); if ( p->pCla->vImps ) printf( "Imp = %5d. ", nImpsOld ); printf( "\n" ); } // refine the classes p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst; p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual; Fra_ClassesRefine( p->pCla ); Fra_ClassesRefine1( p->pCla, 1, NULL ); p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst; p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; // report the results if ( p->pPars->fVerbose ) { printf( "After BMC: " ); // Fra_ClassesPrint( p->pCla, 0 ); printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); if ( p->pCla->vImps ) printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) ); printf( "\n" ); } // free the BMC manager Fra_BmcStop( p->pBmc ); p->pBmc = NULL; } /**Function************************************************************* Synopsis [Performs BMC for the given AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose ) { extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig ); Fra_Man_t * pTemp; Fra_Bmc_t * pBmc; Aig_Man_t * pAigTemp; abctime clk; int iOutput; // derive and fraig the frames clk = Abc_Clock(); pBmc = Fra_BmcStart( pAig, 0, nFrames ); pTemp = Fra_LcrAigPrepare( pAig ); pTemp->pBmc = pBmc; pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 ); if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) ); ABC_PRT( "Time", Abc_Clock() - clk ); } if ( fRewrite ) { clk = Abc_Clock(); pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 ); Aig_ManStop( pAigTemp ); if ( fVerbose ) { printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) ); ABC_PRT( "Time", Abc_Clock() - clk ); } } clk = Abc_Clock(); iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames ); if ( iOutput >= 0 ) pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); else { pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 ); iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig ); if ( pBmc->pAigFraig->pData ) { pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData ); ABC_FREE( pBmc->pAigFraig->pData ); } else if ( iOutput >= 0 ) pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); } if ( fVerbose ) { printf( "Fraiged init frames: Node = %6d. Lev = %5d. ", pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1, pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 ); ABC_PRT( "Time", Abc_Clock() - clk ); } Fra_BmcStop( pBmc ); ABC_FREE( pTemp ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END