diff options
| -rw-r--r-- | src/base/abci/abc.c | 15 | ||||
| -rw-r--r-- | src/sat/bmc/bmcFault.c | 43 |
2 files changed, 34 insertions, 24 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1b0ffbc3..5002905d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -33275,12 +33275,12 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <file> [-S str]\n" ); Abc_Print( -2, "\t performs functional fault test generation\n" ); - Abc_Print( -2, "\t-A num : selects test generation algorithm [default = %d]\n", pPars->Algo ); - Abc_Print( -2, "\t 0: algorithm is not selected (use -S str)\n" ); + Abc_Print( -2, "\t-A num : selects fault model for all gates [default = %d]\n", pPars->Algo ); + Abc_Print( -2, "\t 0: fault model is not selected (use -S str)\n" ); Abc_Print( -2, "\t 1: delay fault testing for sequential circuits\n" ); - Abc_Print( -2, "\t 2: traditional stuck-at testing\n" ); - Abc_Print( -2, "\t 3: complement fault testing\n" ); - Abc_Print( -2, "\t 4: functionally observable fault testing\n" ); + Abc_Print( -2, "\t 2: traditional stuck-at fault: -S (((a&b)&~p)|q)\n" ); + Abc_Print( -2, "\t 3: complement fault: -S ((a&b)^p)\n" ); + Abc_Print( -2, "\t 4: functionally observable fault\n" ); Abc_Print( -2, "\t-T num : specifies approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-c : toggles complementing control variables [default = %s]\n", pPars->fComplVars? "active-high": "active-low" ); Abc_Print( -2, "\t-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", pPars->fStartPats? "yes": "no" ); @@ -33301,9 +33301,10 @@ usage: Abc_Print( -2, "\t (((a&b)&~p)|q) stuck-at-0/1 at the output\n"); Abc_Print( -2, "\t (((a&~p)|q)&b) stuck-at-0/1 at input a\n"); Abc_Print( -2, "\t (((a|p)&(b|q))&~r) stuck-at-1 at the inputs and stuck-at-0 at the output\n"); + Abc_Print( -2, "\t (((a&~p)&(b&~q))|r) stuck-at-0 at the inputs and stuck-at-1 at the output\n"); Abc_Print( -2, "\t ((a&b)^p) complement at the output\n"); - Abc_Print( -2, "\t (((a^p)&(b^q))^r) complement at the inputs/output\n"); - Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functional observability fault at the output\n"); + Abc_Print( -2, "\t (((a^p)&(b^q))^r) complement at the inputs and at the output\n"); + Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functionally observable fault at the output\n"); Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n"); return 1; } diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 9d24f9a6..c52b5033 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -345,8 +345,6 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 4 * Gia_ManAndNum(p) ); -// if ( fUseFaults ) -// Gia_AigerWrite( pNew, "newfault.aig", 0, 0 ); return pNew; } @@ -418,6 +416,23 @@ int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars ) { printf( "The number of parameters should be between 1 and %d\n", *pnPars ); return 1; } return 0; } +void Gia_FormStrTransform( char * pStr, char * pForm ) +{ + int i, k; + for ( k = i = 0; pForm[i]; i++ ) + { + if ( pForm[i] == '~' ) + { + i++; + assert( pForm[i] >= 'a' && pForm[i] <= 'z' ); + pStr[k++] = 'A' + pForm[i] - 'a'; + } + else + pStr[k++] = pForm[i]; + } + pStr[k] = 0; +} + /**Function************************************************************* @@ -497,31 +512,21 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars ); return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] ); } -int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pForm, int nPars ) +int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr, int nPars ) { - char pStr[100]; int i, k; - for ( k = i = 0; pForm[i]; i++ ) - { - if ( pForm[i] == '~' ) - { - i++; - assert( pForm[i] >= 'a' && pForm[i] <= 'z' ); - pStr[k++] = 'A' + pForm[i] - 'a'; - } - else - pStr[k++] = pForm[i]; - } - pStr[k] = 0; return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars ); } Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm ) { + char pStr[100]; Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS]; int nVars, nPars; + assert( strlen(pForm) < 100 ); Gia_FormStrCount( pForm, &nVars, &nPars ); assert( nVars == 2 ); + Gia_FormStrTransform( pStr, pForm ); pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); @@ -536,7 +541,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, { iFans[0] = Gia_ObjFanin0Copy(pObj); iFans[1] = Gia_ObjFanin1Copy(pObj); - pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, nPars ); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars ); } else pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -660,6 +665,8 @@ void Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Ve int i, Lit; // derive the cofactor pC = Gia_ManFaultCofactor( pM, vLits ); +//Gia_AigerWrite( pC, "fftest_cof.aig", 0, 0 ); +//printf( "Dumped cofactor circuit into file \"%s\".\n", "fftest_cof.aig" ); // derive new CNF pCnf2 = Cnf_DeriveGiaRemapped( pC ); Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) ); @@ -877,6 +884,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) p0 = Gia_ManFOFUnfold( p, 0, pPars->fComplVars ); p1 = Gia_ManFOFUnfold( p, 1, pPars->fComplVars ); } +// Gia_AigerWrite( p1, "newfault.aig", 0, 0 ); +// printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" ); // create miter pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 ); |