luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding symbolic fault representation in &fftest.

This commit is contained in:
Alan Mishchenko 2014-05-22 15:59:01 +09:00
parent 292cbfcf90
commit 824ee5b4f3
2 changed files with 34 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/base/abci/abc.c
View File

@ -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;
}

43
src/sat/bmc/bmcFault.c
View File

@ -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 );