From f30160f4be31006c768e2fca9935fb0bfb41ebf3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 May 2014 21:10:19 +0900 Subject: Adding symbolic fault representation in &fftest. --- src/base/abci/abc.c | 21 ++++++++++++--------- src/sat/bmc/bmcFault.c | 42 +++++++++++++++++------------------------- 2 files changed, 29 insertions(+), 34 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 79409b49..fde1a59b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19457,7 +19457,7 @@ int Abc_CommandCubeEnum( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: 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-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" ); @@ -33250,7 +33250,7 @@ usage: Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] [-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\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 2: traditional stuck-at testing\n" ); Abc_Print( -2, "\t 3: complement fault testing\n" ); @@ -33266,15 +33266,18 @@ usage: Abc_Print( -2, "\t : (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 The following notations are used:\n"); - Abc_Print( -2, "\t Functional variables: {a} or {a,b}\n"); - Abc_Print( -2, "\t Parameter variables: {p,q,r,s,...}\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,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 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 ((a&~p)|q) stuck-at-0/1 model\n"); - Abc_Print( -2, "\t (a^p) complement model\n"); - Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functional observability fault model\n"); - Abc_Print( -2, "\t (p^((q^a)&(r^b)) complement at the inputs/output\n"); + 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&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"); return 1; } diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 7d400d03..263a611f 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -394,10 +394,10 @@ int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars ) return 1; } } - if ( *pnVars < 1 && *pnVars > FFTEST_MAX_VARS ) - { printf( "Illigal number of primary inputs (%d)\n", *pnVars ); return 1; } + if ( *pnVars != FFTEST_MAX_VARS ) + { printf( "The number of primary inputs (%d) should be 2\n", *pnVars ); return 1; } 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; } @@ -430,17 +430,17 @@ char * Gia_ManFormulaEndToken( char * pForm ) assert( 0 ); 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; char * pEndNew; 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[0] >= 'a' && pBeg[0] <= 'b' ) 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']; assert( 0 ); return -1; @@ -452,17 +452,17 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p { assert( pBeg[0] == '(' ); 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 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]; // get second part pBeg = pEndNew + 1; 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 if ( Oper == '&' ) 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 assert( pEndNew[0] == ':' ); pBeg = pEndNew + 1; 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] ); } -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 ) { @@ -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 nVars, nPars; Gia_FormStrCount( pForm, &nVars, &nPars ); + assert( nVars == 2 ); pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); @@ -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 ); if ( fUseFaults ) { - if ( nVars == 1 ) - { - iFans[0] = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - 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 ); + iFans[0] = Gia_ObjFanin0Copy(pObj); + iFans[1] = Gia_ObjFanin1Copy(pObj); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, nPars ); } else 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 ) printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" ); else { - printf( "Unregnized algorithm (%d).\n", pPars->Algo ); + printf( "Unrecognized algorithm (%d).\n", pPars->Algo ); return; } -- cgit v1.2.3