Adding symbolic fault representation in &fftest.

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