diff options
Diffstat (limited to 'src/aig/fra/fraBmc.c')
| -rw-r--r-- | src/aig/fra/fraBmc.c | 451 |
1 files changed, 0 insertions, 451 deletions
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c deleted file mode 100644 index 3907fcdd..00000000 --- a/src/aig/fra/fraBmc.c +++ /dev/null @@ -1,451 +0,0 @@ -/**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 = Aig_UtilStrsav( p->pAig->pName ); - pAigFrames->pSpec = Aig_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_ObjCreatePi(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_ObjCreatePo( 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_ObjCreatePo( 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, clk = 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", 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; - int clk, iOutput; - // derive and fraig the frames - clk = 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_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(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_ManPiNum(pBmc->pAigFrames), Aig_ManPoNum(pBmc->pAigFrames), - Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) ); - ABC_PRT( "Time", clock() - clk ); - } - if ( fRewrite ) - { - clk = 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", clock() - clk ); - } - } - clk = clock(); - iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames ); - if ( iOutput >= 0 ) - pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(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_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(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", clock() - clk ); - } - Fra_BmcStop( pBmc ); - ABC_FREE( pTemp ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |