diff options
Diffstat (limited to 'src/aig/ssw/sswBmc.c')
| -rw-r--r-- | src/aig/ssw/sswBmc.c | 224 |
1 files changed, 0 insertions, 224 deletions
diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c deleted file mode 100644 index d565d5d3..00000000 --- a/src/aig/ssw/sswBmc.c +++ /dev/null @@ -1,224 +0,0 @@ -/**CFile**************************************************************** - - FileName [sswBmc.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Inductive prover with constraints.] - - Synopsis [Bounded model checker using dynamic unrolling.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - September 1, 2008.] - - Revision [$Id: sswBmc.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "sswInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Incrementally unroll the timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) -{ - Aig_Obj_t * pRes, * pRes0, * pRes1; - if ( (pRes = Ssw_ObjFrame_(pFrm, pObj, f)) ) - return pRes; - if ( Aig_ObjIsConst1(pObj) ) - pRes = Aig_ManConst1( pFrm->pFrames ); - else if ( Saig_ObjIsPi(pFrm->pAig, pObj) ) - pRes = Aig_ObjCreatePi( pFrm->pFrames ); - else if ( Aig_ObjIsPo(pObj) ) - { - Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); - pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f ); - } - else if ( Saig_ObjIsLo(pFrm->pAig, pObj) ) - { - if ( f == 0 ) - pRes = Aig_ManConst0( pFrm->pFrames ); - else - pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 ); - } - else - { - assert( Aig_ObjIsNode(pObj) ); - Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); - Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin1(pObj), f ); - pRes0 = Ssw_ObjChild0Fra_( pFrm, pObj, f ); - pRes1 = Ssw_ObjChild1Fra_( pFrm, pObj, f ); - pRes = Aig_And( pFrm->pFrames, pRes0, pRes1 ); - } - Ssw_ObjSetFrame_( pFrm, pObj, f, pRes ); - return pRes; -} - -/**Function************************************************************* - - Synopsis [Derives counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame ) -{ - Abc_Cex_t * pCex; - Aig_Obj_t * pObj, * pObjFrames; - int f, i, nShift; - assert( Saig_ManRegNum(pFrm->pAig) > 0 ); - // allocate the counter example - pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - // create data-bits - nShift = Saig_ManRegNum(pFrm->pAig); - for ( f = 0; f <= iFrame; f++, nShift += Saig_ManPiNum(pFrm->pAig) ) - Saig_ManForEachPi( pFrm->pAig, pObj, i ) - { - pObjFrames = Ssw_ObjFrame_(pFrm, pObj, f); - if ( pObjFrames == NULL ) - continue; - if ( Ssw_CnfGetNodeValue( pSat, pObjFrames ) ) - Aig_InfoSetBit( pCex->pData, nShift + i ); - } - return pCex; -} - - -/**Function************************************************************* - - Synopsis [Performs BMC for the given AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ) -{ - Ssw_Frm_t * pFrm; - Ssw_Sat_t * pSat; - Aig_Obj_t * pObj, * pObjFrame; - int status, clkPart, Lit, i, f, RetValue; - - // start managers - assert( Saig_ManRegNum(pAig) > 0 ); - Aig_ManSetPioNumbers( pAig ); - pSat = Ssw_SatStart( 0 ); - pFrm = Ssw_FrmStart( pAig ); - pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 ); - // report statistics - if ( fVerbose ) - { - printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", - Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), - Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); - fflush( stdout ); - } - // perform dynamic unrolling - RetValue = -1; - for ( f = 0; f < nFramesMax; f++ ) - { - clkPart = clock(); - Saig_ManForEachPo( pAig, pObj, i ) - { - // unroll the circuit for this output - Ssw_BmcUnroll_rec( pFrm, pObj, f ); - pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f ); - Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) ); - status = sat_solver_simplify(pSat->pSat); - assert( status ); - // solve - Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) ); - if ( fVerbose ) - { - printf( "Solving output %2d of frame %3d ... \r", - i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); - } - status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( status == l_False ) - { -/* - Lit = lit_neg( Lit ); - RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 ); - assert( RetValue ); - if ( pSat->pSat->qtail != pSat->pSat->qhead ) - { - RetValue = sat_solver_simplify(pSat->pSat); - assert( RetValue ); - } -*/ - RetValue = 1; - continue; - } - else if ( status == l_True ) - { - pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f ); - if ( piFrame ) - *piFrame = f; - RetValue = 0; - break; - } - else - { - if ( piFrame ) - *piFrame = f; - RetValue = -1; - break; - } - } - if ( fVerbose ) - { - printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f ); - printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ", - (double)pSat->pSat->stats.conflicts, - pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) ); - ABC_PRT( "T", clock() - clkPart ); - clkPart = clock(); - fflush( stdout ); - } - if ( RetValue != 1 ) - break; - } - - Ssw_SatStop( pSat ); - Ssw_FrmStop( pFrm ); - return RetValue; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |