Skip to content

A
abc
Commit f30160f4 by Alan Mishchenko
Options

Adding symbolic fault representation in &fftest.

parent 911b801f
Showing with 29 additions and 34 deletions
src/base/abci/abc.c
...@@ -19457,7 +19457,7 @@ int Abc_CommandCubeEnum( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19457,7 +19457,7 @@ int Abc_CommandCubeEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
Abc_Print( -2, "usage: cubeenum [-vh]\n" ); Abc_Print( -2, "usage: cubeenum [-vh]\n" );
Abc_Print( -2, "\t enumerates reachable states of 2x2x2x cube\n" ); Abc_Print( -2, "\t enumerates reachable states of 2x2x2 cube\n" );
Abc_Print( -2, "\t (http://en.wikipedia.org/wiki/Pocket_Cube)\n" ); Abc_Print( -2, "\t (http://en.wikipedia.org/wiki/Pocket_Cube)\n" );
Abc_Print( -2, "\t-z : toggle using ZDD-based algorithm [default = %s]\n", fZddAlgo? "yes": "no" ); Abc_Print( -2, "\t-z : toggle using ZDD-based algorithm [default = %s]\n", fZddAlgo? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
...@@ -33250,7 +33250,7 @@ usage: ...@@ -33250,7 +33250,7 @@ usage:
Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <file> [-S str]\n" ); 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 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-A num : selects test generation algorithm [default = %d]\n", pPars->Algo );
Abc_Print( -2, "\t 0: algorithm is not selected\n" ); Abc_Print( -2, "\t 0: algorithm is not selected (use -S str)\n" );
Abc_Print( -2, "\t 1: delay fault testing for sequential circuits\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 2: traditional stuck-at testing\n" );
Abc_Print( -2, "\t 3: complement fault testing\n" ); Abc_Print( -2, "\t 3: complement fault testing\n" );
...@@ -33266,15 +33266,18 @@ usage: ...@@ -33266,15 +33266,18 @@ usage:
Abc_Print( -2, "\t<file> : (optional) file name with input test patterns\n\n"); Abc_Print( -2, "\t<file> : (optional) file name with input test patterns\n\n");
Abc_Print( -2, "\t-S str : (optional) string representing the fault model\n"); Abc_Print( -2, "\t-S str : (optional) string representing the fault model\n");
Abc_Print( -2, "\t The following notations are used:\n"); Abc_Print( -2, "\t The following notations are used:\n");
Abc_Print( -2, "\t Functional variables: {a} or {a,b}\n"); Abc_Print( -2, "\t Functional variables: {a,b} (both a and b are always present)\n");
Abc_Print( -2, "\t Parameter variables: {p,q,r,s,...}\n"); Abc_Print( -2, "\t Parameter variables: {p,q,r,s,t,u,v,w} (any number from 1 to 8)\n");
Abc_Print( -2, "\t Boolean operators: AND(&), OR(|), XOR(^), MUX(?:), NOT(~)\n"); Abc_Print( -2, "\t Boolean operators: AND(&), OR(|), XOR(^), MUX(?:), NOT(~)\n");
Abc_Print( -2, "\t Parantheses should be used around each operator. Spaces are not allowed.\n"); Abc_Print( -2, "\t Parantheses should be used around each operator. Spaces not allowed.\n");
Abc_Print( -2, "\t Complement (~) is only allowed before variables (use DeMorgan law).\n");
Abc_Print( -2, "\t Examples:\n"); Abc_Print( -2, "\t Examples:\n");
Abc_Print( -2, "\t ((a&~p)|q) stuck-at-0/1 model\n"); Abc_Print( -2, "\t (((a&b)&~p)|q) stuck-at-0/1 at the output\n");
Abc_Print( -2, "\t (a^p) complement model\n"); Abc_Print( -2, "\t (((a&~p)|q)&b) stuck-at-0/1 at input a\n");
Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functional observability fault model\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 (p^((q^a)&(r^b)) complement at the inputs/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 (p?(a|b):(a&b)) replace AND by OR\n"); Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n");
return 1; return 1;
} }
src/sat/bmc/bmcFault.c
...@@ -394,10 +394,10 @@ int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars ) ...@@ -394,10 +394,10 @@ int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars )
return 1; return 1;
} }
} }
if ( *pnVars < 1 && *pnVars > FFTEST_MAX_VARS ) if ( *pnVars != FFTEST_MAX_VARS )
{ printf( "Illigal number of primary inputs (%d)\n", *pnVars ); return 1; } { printf( "The number of primary inputs (%d) should be 2\n", *pnVars ); return 1; }
if ( *pnPars < 1 && *pnPars > FFTEST_MAX_PARS ) if ( *pnPars < 1 && *pnPars > FFTEST_MAX_PARS )
{ printf( "Illigal number of primary inputs (%d)\n", *pnPars ); return 1; } { printf( "The number of parameters should be between 1 and %d\n", *pnPars ); return 1; }
return 0; return 0;
} }
...@@ -430,17 +430,17 @@ char * Gia_ManFormulaEndToken( char * pForm ) ...@@ -430,17 +430,17 @@ char * Gia_ManFormulaEndToken( char * pForm )
assert( 0 ); assert( 0 );
return NULL; return NULL;
} }
int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nVars, int nPars ) int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nPars )
{ {
int iFans[3], Oper = -1; int iFans[3], Oper = -1;
char * pEndNew; char * pEndNew;
if ( pBeg[0] == '~' ) if ( pBeg[0] == '~' )
return Abc_LitNot( Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd, nVars, nPars ) ); return Abc_LitNot( Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd, nPars ) );
if ( pBeg + 1 == pEnd ) if ( pBeg + 1 == pEnd )
{ {
if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' ) if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
return pVars[pBeg[0] - 'a']; return pVars[pBeg[0] - 'a'];
if ( pBeg[0] >= 'p' && pBeg[0] <= 's' ) if ( pBeg[0] >= 'p' && pBeg[0] <= 'w' ) // pqrstuvw
return pPars[pBeg[0] - 'p']; return pPars[pBeg[0] - 'p'];
assert( 0 ); assert( 0 );
return -1; return -1;
...@@ -452,17 +452,17 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p ...@@ -452,17 +452,17 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p
{ {
assert( pBeg[0] == '(' ); assert( pBeg[0] == '(' );
assert( pBeg[pEnd-pBeg-1] == ')' ); assert( pBeg[pEnd-pBeg-1] == ')' );
return Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd - 1, nVars, nPars ); return Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd - 1, nPars );
} }
} }
// get first part // get first part
pEndNew = Gia_ManFormulaEndToken( pBeg ); pEndNew = Gia_ManFormulaEndToken( pBeg );
iFans[0] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, nPars ); iFans[0] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
Oper = pEndNew[0]; Oper = pEndNew[0];
// get second part // get second part
pBeg = pEndNew + 1; pBeg = pEndNew + 1;
pEndNew = Gia_ManFormulaEndToken( pBeg ); pEndNew = Gia_ManFormulaEndToken( pBeg );
iFans[1] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, nPars ); iFans[1] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
// derive the formula // derive the formula
if ( Oper == '&' ) if ( Oper == '&' )
return Gia_ManHashAnd( p, iFans[0], iFans[1] ); return Gia_ManHashAnd( p, iFans[0], iFans[1] );
...@@ -475,12 +475,12 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p ...@@ -475,12 +475,12 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p
assert( pEndNew[0] == ':' ); assert( pEndNew[0] == ':' );
pBeg = pEndNew + 1; pBeg = pEndNew + 1;
pEndNew = Gia_ManFormulaEndToken( pBeg ); pEndNew = Gia_ManFormulaEndToken( pBeg );
iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, nPars ); iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] ); return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] );
} }
int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pForm, int nVars, int nPars ) int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pForm, int nPars )
{ {
return Gia_ManRealizeFormula_rec( p, pVars, pPars, pForm, pForm + strlen(pForm), nVars, nPars ); return Gia_ManRealizeFormula_rec( p, pVars, pPars, pForm, pForm + strlen(pForm), nPars );
} }
Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm ) Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm )
{ {
...@@ -489,6 +489,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, ...@@ -489,6 +489,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars,
int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS]; int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS];
int nVars, nPars; int nVars, nPars;
Gia_FormStrCount( pForm, &nVars, &nPars ); Gia_FormStrCount( pForm, &nVars, &nPars );
assert( nVars == 2 );
pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) ); pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew ); Gia_ManHashAlloc( pNew );
...@@ -501,18 +502,9 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, ...@@ -501,18 +502,9 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars,
iCtrl[k] = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); iCtrl[k] = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
if ( fUseFaults ) if ( fUseFaults )
{ {
if ( nVars == 1 ) iFans[0] = Gia_ObjFanin0Copy(pObj);
{ iFans[1] = Gia_ObjFanin1Copy(pObj);
iFans[0] = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, nPars );
pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, 1, nPars );
}
else if ( nVars == 2 )
{
iFans[0] = Gia_ObjFanin0Copy(pObj);
iFans[1] = Gia_ObjFanin1Copy(pObj);
pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, 2, nPars );
}
else assert( 0 );
} }
else else
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
...@@ -796,7 +788,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) ...@@ -796,7 +788,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" ); printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" );
else else
{ {
printf( "Unregnized algorithm (%d).\n", pPars->Algo ); printf( "Unrecognized algorithm (%d).\n", pPars->Algo );
return; return;
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment