diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcFault.c | 44 |
2 files changed, 36 insertions, 10 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 17e15335..de96b546 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36405,7 +36405,7 @@ usage: Abc_Print( -2, "\t-N num : specifies iteration to check for fixed parameters [default = %d]\n", pPars->nIterCheck ); Abc_Print( -2, "\t-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", pPars->fStartPats? "yes": "no" ); Abc_Print( -2, "\t-b : toggles testing for single faults only [default = %s]\n", pPars->fBasic? "yes": "no" ); - Abc_Print( -2, "\t-f : toggles using flop inputs only with \"-A 1\" [default = %s]\n", pPars->fFfOnly? "yes": "no" ); + Abc_Print( -2, "\t-f : toggles faults at flop inputs only with \"-A 1\" and \"-S str\" [default = %s]\n", pPars->fFfOnly? "yes": "no" ); Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", pPars->fDump? "yes": "no" ); Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index d0186d31..d07f9fba 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -557,9 +557,10 @@ int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr, { return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars ); } -Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm ) +Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly ) { char pStr[100]; + int Count = 0; Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS]; @@ -574,19 +575,44 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm ) Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachAnd( p, pObj, i ) + if ( fFfOnly ) + { + Gia_ManCleanMark0( p ); + Gia_ManForEachRi( p, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( pObj->fMark0 ) + { + for ( k = 0; k < nPars; k++ ) + iCtrl[k] = Gia_ManAppendCi(pNew); + iFans[0] = Gia_ObjFanin0Copy(pObj); + iFans[1] = Gia_ObjFanin1Copy(pObj); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars ); + Count++; + } + else + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + Gia_ManForEachRi( p, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 0; + } + else { - for ( k = 0; k < nPars; k++ ) - iCtrl[k] = Gia_ManAppendCi(pNew); - iFans[0] = Gia_ObjFanin0Copy(pObj); - iFans[1] = Gia_ObjFanin1Copy(pObj); - pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars ); + Gia_ManForEachAnd( p, pObj, i ) + { + for ( k = 0; k < nPars; k++ ) + iCtrl[k] = Gia_ManAppendCi(pNew); + iFans[0] = Gia_ObjFanin0Copy(pObj); + iFans[1] = Gia_ObjFanin1Copy(pObj); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars ); + } } 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) + nPars * Gia_ManAndNum(p) ); + assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * (fFfOnly ? Count : Gia_ManAndNum(p)) ); // if ( fUseFaults ) // Gia_AigerWrite( pNew, "newfault.aig", 0, 0 ); return pNew; @@ -939,7 +965,7 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int // select algorithm if ( pPars->Algo == 0 ) - p1 = Gia_ManFormulaUnfold( p, pPars->pFormStr ); + p1 = Gia_ManFormulaUnfold( p, pPars->pFormStr, pPars->fFfOnly ); else if ( pPars->Algo == 1 ) { assert( Gia_ManRegNum(p) > 0 ); |