diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-09 12:11:49 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-09 12:11:49 -0700 |
commit | cc6c8b2f2af0337495a6efe71cc00b486e199640 (patch) | |
tree | 77652cddb36a02fe48389b8a7d1293f9093f154c /src/sat/bmc | |
parent | e5d552138a9765167b2a9933067d4f72ba710267 (diff) | |
download | abc-cc6c8b2f2af0337495a6efe71cc00b486e199640.tar.gz abc-cc6c8b2f2af0337495a6efe71cc00b486e199640.tar.bz2 abc-cc6c8b2f2af0337495a6efe71cc00b486e199640.zip |
Experiments with stuck-at fault testing.
Diffstat (limited to 'src/sat/bmc')
-rw-r--r-- | src/sat/bmc/bmcFault.c | 58 |
1 files changed, 51 insertions, 7 deletions
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 49ed63d6..d5615a75 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -88,7 +88,7 @@ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPl SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes ) +Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; @@ -113,7 +113,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManForEachAnd( p, pObj, i ) { - iCtrl = Gia_ManAppendCi( pNew ); + iCtrl = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( fUseMuxes ) pObj->Value = Gia_ManHashMux( pNew, iCtrl, iThis, pObj->Value ); @@ -139,6 +139,47 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes ) SeeAlso [] ***********************************************************************/ +Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iCtrl0, iCtrl1; + pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); + iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); + if ( fUseFaults ) + { + pObj->Value = Gia_ManHashAnd( pNew, iCtrl0, pObj->Value ); + pObj->Value = Gia_ManHashOr( pNew, Abc_LitNot(iCtrl1), pObj->Value ); + } + } + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 2 * Gia_ManAndNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues ) { Gia_Man_t * pNew, * pTemp; @@ -229,18 +270,19 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c SeeAlso [] ***********************************************************************/ -void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose ) +void Gia_ManFaultTest( Gia_Man_t * p, int fStuckAt, int fComplVars, int nTimeOut, int fDump, int fVerbose ) { int nIterMax = 1000000; int i, Iter, status; abctime clkTotal = Abc_Clock(); abctime clkSat = 0; + int nFuncVars = fStuckAt ? Gia_ManCiNum(p) : Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p); Vec_Int_t * vLits, * vTests; sat_solver * pSat; Gia_Obj_t * pObj; Gia_Man_t * pC; - Gia_Man_t * p0 = Gia_ManFaultUnfold( p, 0 ); - Gia_Man_t * p1 = Gia_ManFaultUnfold( p, 1 ); + Gia_Man_t * p0 = fStuckAt ? Gia_ManStuckAtUnfold(p, 0, fComplVars) : Gia_ManFaultUnfold(p, 0, fComplVars); + Gia_Man_t * p1 = fStuckAt ? Gia_ManStuckAtUnfold(p, 1, fComplVars) : Gia_ManFaultUnfold(p, 1, fComplVars); Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 ); Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM ), * pCnf2; Gia_ManStop( p0 ); @@ -296,7 +338,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose ) // collect SAT assignment Vec_IntClear( vLits ); Gia_ManForEachPi( pM, pObj, i ) - if ( i < Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p) ) + if ( i < nFuncVars ) Vec_IntPush( vLits, sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) ); Vec_IntAppend( vTests, vLits ); // derive the cofactor @@ -317,7 +359,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose ) } // add connection clauses Gia_ManForEachPi( pM, pObj, i ) - if ( i >= Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p) ) + if ( i >= nFuncVars ) sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 ); Cnf_DataFree( pCnf2 ); Gia_ManStop( pC ); @@ -337,6 +379,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose ) Vec_IntFree( vTests ); } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |