Adding symbolic fault representation in &fftest.

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] <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\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<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         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;
     }