Adding symbolic fault representation in &fftest.

3 files changed, 341 insertions, 76 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index de32646c..79409b49 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -33144,11 +33144,13 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fBasic, int fDump, int fDumpUntest, int fVerbose );
-    int c, Algo = 0, fComplVars = 0, fStartPats = 0, nTimeOut = 0, fBasic = 0, fDump = 0, fDumpUntest = 0, fVerbose = 0;
-    char * pFileName = NULL;
+    extern void Gia_ParFfSetDefault( Bmc_ParFf_t * p );
+    extern void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars );
+    Bmc_ParFf_t Pars, * pPars = &Pars;
+    int c;
+    Gia_ParFfSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ATcsbduvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ATScsbduvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -33158,9 +33160,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
                 goto usage;
             }
-            Algo = atoi(argv[globalUtilOptind]);
+            pPars->Algo = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( Algo < 1 || Algo > 4 )
+            if ( pPars->Algo < 0 || pPars->Algo > 4 )
                 goto usage;
             break;
         case 'T':
@@ -33169,28 +33171,37 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nTimeOut = atoi(argv[globalUtilOptind]);
+            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nTimeOut < 0 )
+            if ( pPars->nTimeOut < 0 )
                 goto usage;
             break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" );
+                goto usage;
+            }
+            pPars->pFormStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'c':
-            fComplVars ^= 1;
+            pPars->fComplVars ^= 1;
             break;
         case 's':
-            fStartPats ^= 1;
+            pPars->fStartPats ^= 1;
             break;
         case 'b':
-            fBasic ^= 1;
+            pPars->fBasic ^= 1;
             break;
         case 'd':
-            fDump ^= 1;
+            pPars->fDump ^= 1;
             break;
         case 'u':
-            fDumpUntest ^= 1;
+            pPars->fDumpUntest ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -33198,15 +33209,25 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( pPars->Algo == 0 && pPars->pFormStr == NULL )
+    {
+        Abc_Print( -1, "Formula string (-S <str>) should be selected when algorithm is 0 (-A 0).\n" );
+        return 0;
+    }
+    if ( pPars->Algo != 0 && pPars->pFormStr != NULL )
+    {
+        Abc_Print( -1, "Algorithm should be 0 (-A 0) when formula string is selected (-S <str>).\n" );
+        return 0;
+    }
     // get the file name
     if ( argc == globalUtilOptind + 1 )
     {
         FILE * pFile;
-        pFileName = argv[globalUtilOptind];
-        pFile = fopen( pFileName, "r" );
+        pPars->pFileName = argv[globalUtilOptind];
+        pFile = fopen( pPars->pFileName, "r" );
         if ( pFile == NULL )
         {
-            Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName );
+            Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pPars->pFileName );
             return 0;
         }
         fclose( pFile );
@@ -33217,32 +33238,44 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9FFTest(): There is no AIG.\n" );
         return 0;
     }
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 && Algo == 1 )
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 && pPars->Algo == 1 )
     {
         Abc_Print( -1, "Abc_CommandAbc9FFTest(): For delay testing, AIG should be sequential.\n" );
         return 0;
     }
-    Gia_ManFaultTest( pAbc->pGia, pFileName, Algo, fComplVars, fStartPats, nTimeOut, fBasic, fDump, fDumpUntest, fVerbose );
+    Gia_ManFaultTest( pAbc->pGia, pPars );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <file>\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-A num : selects test generation algorithm [default = %d]\n", 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               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-T num : specifies approximate runtime limit in seconds [default = %d]\n",        nTimeOut );
-    Abc_Print( -2, "\t-c     : toggles complementing control variables [default = %s]\n",               fComplVars?  "active-high": "active-low" );
-    Abc_Print( -2, "\t-s     : toggles starting with the all-0 and all-1 patterns [default = %s]\n",    fStartPats?  "yes": "no" );
-    Abc_Print( -2, "\t-b     : toggles testing for single faults only [default = %s]\n",                fBasic?      "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", fDump?       "yes": "no" );
-    Abc_Print( -2, "\t-u     : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", fDumpUntest? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",                  fVerbose?    "yes": "no" );
+    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" );
+    Abc_Print( -2, "\t-b     : toggles testing for single faults only [default = %s]\n",                pPars->fBasic?      "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", pPars->fDump?       "yes": "no" );
+    Abc_Print( -2, "\t-u     : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",                  pPars->fVerbose?    "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
-    Abc_Print( -2, "\t<file> : (optional) file name with input test patterns\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         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           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           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             (p?(a|b):(a&b))       replace AND by OR\n");    
     return 1;
 }
 
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 558b2d62..dd8d36eb 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -120,6 +120,21 @@ struct Bmc_MulPar_t_
     int         fVeryVerbose;
 };
 
+typedef struct Bmc_ParFf_t_ Bmc_ParFf_t;
+struct Bmc_ParFf_t_
+{
+    char *     pFileName;
+    char *     pFormStr;
+    int        Algo;
+    int        fComplVars;
+    int        fStartPats;
+    int        nTimeOut;
+    int        fBasic;
+    int        fDump;
+    int        fDumpUntest;
+    int        fVerbose;
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 6c1bf81b..7d400d03 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -30,12 +30,40 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define FFTEST_MAX_VARS 2
+#define FFTEST_MAX_PARS 8
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
+{
+    memset( p, 0, sizeof(Bmc_ParFf_t) );
+    p->pFileName     =  NULL; 
+    p->Algo          =     0; 
+    p->fComplVars    =     0; 
+    p->fStartPats    =     0; 
+    p->nTimeOut      =     0; 
+    p->fBasic        =     0; 
+    p->fDump         =     0; 
+    p->fDumpUntest   =     0; 
+    p->fVerbose      =     0; 
+}
+
+/**Function*************************************************************
+
   Synopsis    [Add constraint that no more than 1 variable is 1.]
 
   Description []
@@ -324,6 +352,183 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars )
+{
+    int i;
+    if ( pStr[0] != '(' )
+    {
+        printf( "The first symbol should be the opening paranthesis \"(\".\n" );
+        return 1;
+    }
+    if ( pStr[strlen(pStr)-1] != ')' )
+    {
+        printf( "The last symbol should be the closing paranthesis \")\".\n" );
+        return 1;
+    }
+    *pnVars = 0;
+    *pnPars = 0;
+    for ( i = 0; pStr[i]; i++ )
+    {
+        if ( pStr[i] >= 'a' && pStr[i] <= 'b' )
+            *pnVars = Abc_MaxInt( *pnVars, pStr[i] - 'a' + 1 );
+        else if ( pStr[i] >= 'p' && pStr[i] <= 's' )
+            *pnPars = Abc_MaxInt( *pnPars, pStr[i] - 'p' + 1 );
+        else if ( pStr[i] == '(' || pStr[i] == ')' )
+        {}
+        else if ( pStr[i] == '&' || pStr[i] == '|' || pStr[i] == '^' )
+        {}
+        else if ( pStr[i] == '?' || pStr[i] == ':' || pStr[i] == '~' )
+        {}
+        else 
+        {
+            printf( "Unknown symbol (%c) in the formula (%s)\n", pStr[i], pStr );
+            return 1;
+        }
+    }
+    if ( *pnVars < 1 && *pnVars > FFTEST_MAX_VARS )
+        { printf( "Illigal number of primary inputs (%d)\n", *pnVars ); return 1; }
+    if ( *pnPars < 1 && *pnPars > FFTEST_MAX_PARS )
+        { printf( "Illigal number of primary inputs (%d)\n", *pnPars ); return 1; }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements fault model formula using functional/parameter vars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Gia_ManFormulaEndToken( char * pForm )
+{
+    int Counter = 0;
+    char * pThis;
+    for ( pThis = pForm; *pThis; pThis++ )
+    {
+        if ( *pThis == '~' )
+            continue;
+        if ( *pThis == '(' )
+            Counter++;
+        else if ( *pThis == ')' )
+            Counter--;
+        if ( Counter == 0 )
+            return pThis + 1;
+    }
+    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 iFans[3], Oper = -1;
+    char * pEndNew;
+    if ( pBeg[0] == '~' )
+        return Abc_LitNot( Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd, nVars, nPars ) );
+    if ( pBeg + 1 == pEnd )
+    {
+        if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
+            return pVars[pBeg[0] - 'a'];
+        if ( pBeg[0] >= 'p' && pBeg[0] <= 's' )
+            return pPars[pBeg[0] - 'p'];
+        assert( 0 );
+        return -1;
+    }
+    if ( pBeg[0] == '(' )
+    {
+        pEndNew = Gia_ManFormulaEndToken( pBeg );
+        if ( pEndNew == pEnd )
+        {
+            assert( pBeg[0] == '(' );
+            assert( pBeg[pEnd-pBeg-1] == ')' );
+            return Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd - 1, nVars, nPars );
+        }
+    }
+    // get first part
+    pEndNew  = Gia_ManFormulaEndToken( pBeg );
+    iFans[0] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, 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 );
+    // derive the formula
+    if ( Oper == '&' )
+        return Gia_ManHashAnd( p, iFans[0], iFans[1] );
+    if ( Oper == '|' )
+        return Gia_ManHashOr( p, iFans[0], iFans[1] );
+    if ( Oper == '^' )
+        return Gia_ManHashXor( p, iFans[0], iFans[1] );
+    // get third part
+    assert( Oper == '?' );
+    assert( pEndNew[0] == ':' );
+    pBeg     = pEndNew + 1;
+    pEndNew  = Gia_ManFormulaEndToken( pBeg );
+    iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, 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 )
+{
+    return Gia_ManRealizeFormula_rec( p, pVars, pPars, pForm, pForm + strlen(pForm), nVars, nPars );
+}
+Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS];
+    int nVars, nPars;
+    Gia_FormStrCount( pForm, &nVars, &nPars );
+    pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        for ( k = 0; k < nPars; k++ )
+            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 );
+        }
+        else
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * Gia_ManAndNum(p) );
+//    if ( fUseFaults )
+//        Gia_AigerWrite( pNew, "newfault.aig", 0, 0 );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -564,9 +769,9 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fBasic, int fDump, int fDumpUntest, int fVerbose )
+void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
 {
-    int nIterMax = 1000000;
+    int nIterMax = 1000000, nVars, nPars;
     int i, Iter, LitRoot, status, nFuncVars = -1;
     abctime clkSat = 0, clkTotal = Abc_Clock();
     Vec_Int_t * vLits, * vTests;
@@ -575,34 +780,41 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
 
+    if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) )
+        return;
+
     // select algorithm
-    if ( Algo == 1 )
-        printf( "FFTEST is computing test patterns for %sdelay faults...\n", fBasic ? "single " : "" );
-    else if ( Algo == 2 )
-        printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", fBasic ? "single " : "" );
-    else if ( Algo == 3 )
-        printf( "FFTEST is computing test patterns for %scomplement faults...\n", fBasic ? "single " : "" );
-    else if ( Algo == 4 )
-        printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", fBasic ? "single " : "" );
+    if ( pPars->Algo == 0 )
+        printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr );
+    else if ( pPars->Algo == 1 )
+        printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" );
+    else if ( pPars->Algo == 2 )
+        printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" );
+    else if ( pPars->Algo == 3 )
+        printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" );
+    else if ( pPars->Algo == 4 )
+        printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" );
     else
     {
-        printf( "Unregnized algorithm (%d).\n", Algo );
+        printf( "Unregnized algorithm (%d).\n", pPars->Algo );
         return;
     }
 
     // select algorithm
-    if ( Algo == 1 )
+    if ( pPars->Algo == 0 )
+        nFuncVars = Gia_ManCiNum(p);
+    else if ( pPars->Algo == 1 )
         nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
-    else if ( Algo == 2 )
+    else if ( pPars->Algo == 2 )
         nFuncVars = Gia_ManCiNum(p);
-    else if ( Algo == 3 )
+    else if ( pPars->Algo == 3 )
         nFuncVars = Gia_ManCiNum(p);
-    else if ( Algo == 4 )
+    else if ( pPars->Algo == 4 )
         nFuncVars = Gia_ManCiNum(p);
 
     // collect test patterns from file
-    if ( pFileName )
-        vTests = Gia_ManGetTestPatterns( pFileName );
+    if ( pPars->pFileName )
+        vTests = Gia_ManGetTestPatterns( pPars->pFileName );
     else
         vTests = Vec_IntAlloc( 10000 );
     if ( vTests == NULL )
@@ -615,26 +827,31 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     }
 
     // select algorithm
-    if ( Algo == 1 )
+    if ( pPars->Algo == 0 )
+    {
+        p0 = Gia_ManFormulaUnfold( p, 0, pPars->fComplVars, pPars->pFormStr );
+        p1 = Gia_ManFormulaUnfold( p, 1, pPars->fComplVars, pPars->pFormStr );
+    }
+    else if ( pPars->Algo == 1 )
     {
         assert( Gia_ManRegNum(p) > 0 );
-        p0 = Gia_ManFaultUnfold( p, 0, fComplVars );
-        p1 = Gia_ManFaultUnfold( p, 1, fComplVars );
+        p0 = Gia_ManFaultUnfold( p, 0, pPars->fComplVars );
+        p1 = Gia_ManFaultUnfold( p, 1, pPars->fComplVars );
     }
-    else if ( Algo == 2 )
+    else if ( pPars->Algo == 2 )
     {
-        p0 = Gia_ManStuckAtUnfold( p, 0, fComplVars );
-        p1 = Gia_ManStuckAtUnfold( p, 1, fComplVars );
+        p0 = Gia_ManStuckAtUnfold( p, 0, pPars->fComplVars );
+        p1 = Gia_ManStuckAtUnfold( p, 1, pPars->fComplVars );
     }
-    else if ( Algo == 3 )
+    else if ( pPars->Algo == 3 )
     {
-        p0 = Gia_ManFlipUnfold( p, 0, fComplVars );
-        p1 = Gia_ManFlipUnfold( p, 1, fComplVars );
+        p0 = Gia_ManFlipUnfold( p, 0, pPars->fComplVars );
+        p1 = Gia_ManFlipUnfold( p, 1, pPars->fComplVars );
     }
-    else if ( Algo == 4 )
+    else if ( pPars->Algo == 4 )
     {
-        p0 = Gia_ManFOFUnfold( p, 0, fComplVars );
-        p1 = Gia_ManFOFUnfold( p, 1, fComplVars );
+        p0 = Gia_ManFOFUnfold( p, 0, pPars->fComplVars );
+        p1 = Gia_ManFOFUnfold( p, 1, pPars->fComplVars );
     }
 
     // create miter
@@ -645,9 +862,9 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
 
     // start the SAT solver
     pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, pCnf->nVars + (fDumpUntest ? 1 : 0) );
-    sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
-    LitRoot = fDumpUntest ? Abc_Var2Lit( pCnf->nVars, 1 ) : 0;
+    sat_solver_setnvars( pSat, pCnf->nVars + (pPars->fDumpUntest ? 1 : 0) );
+    sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+    LitRoot = pPars->fDumpUntest ? Abc_Var2Lit( pCnf->nVars, 1 ) : 0;
     // add timeframe clauses
     for ( i = 0; i < pCnf->nClauses; i++ )
         if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
@@ -662,7 +879,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
 
     // add cadinality constraint
-    if ( fBasic )
+    if ( pPars->fBasic )
     {
         Vec_IntClear( vLits );
         Gia_ManForEachPi( pM, pObj, i )
@@ -676,7 +893,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     {
         int nTests = Vec_IntSize(vTests) / nFuncVars;
         assert( Vec_IntSize(vTests) % nFuncVars == 0 );
-        printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
+        printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName );
         for ( Iter = 0; Iter < nTests; Iter++ )
         {
             abctime clk = Abc_Clock();
@@ -687,7 +904,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
             for ( i = 0; i < nFuncVars; i++ )
                 Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
             Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
-            if ( fVerbose )
+            if ( pPars->fVerbose )
             {
                 printf( "Iter%6d : ",       Iter );
                 printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
@@ -698,21 +915,21 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
             }
         }
     }
-    else if ( fStartPats )
+    else if ( pPars->fStartPats )
     {
         for ( Iter = 0; Iter < 2; Iter++ )
         {
             status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( status == l_Undef )
             {
-                if ( fVerbose )
+                if ( pPars->fVerbose )
                     printf( "\n" );
-                printf( "Timeout reached after %d seconds and %d iterations.  ", nTimeOut, Iter );
+                printf( "Timeout reached after %d seconds and %d iterations.  ", pPars->nTimeOut, Iter );
                 break;
             }
             if ( status == l_False )
             {
-                if ( fVerbose )
+                if ( pPars->fVerbose )
                     printf( "\n" );
                 printf( "The problem is UNSAT after %d iterations.  ", Iter );
                 break;
@@ -725,12 +942,12 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     }
 
     // iterate through the test vectors
-    for ( Iter = fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
+    for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
     {
         abctime clk = Abc_Clock();
         status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         clkSat += Abc_Clock() - clk;
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
             printf( "Iter%6d : ",       Iter );
             printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
@@ -741,14 +958,14 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
         }
         if ( status == l_Undef )
         {
-            if ( fVerbose )
+            if ( pPars->fVerbose )
                 printf( "\n" );
-            printf( "Timeout reached after %d seconds and %d iterations.  ", nTimeOut, Iter );
+            printf( "Timeout reached after %d seconds and %d iterations.  ", pPars->nTimeOut, Iter );
             break;
         }
         if ( status == l_False )
         {
-            if ( fVerbose )
+            if ( pPars->fVerbose )
                 printf( "\n" );
             printf( "The problem is UNSAT after %d iterations.  ", Iter );
             break;
@@ -769,11 +986,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     // cleanup
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
     // dump untestable faults
-    if ( fDumpUntest )
+    if ( pPars->fDumpUntest )
     {
         abctime clk = Abc_Clock();
         char * pFileName = "untest.txt";
-        int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, Abc_LitNot(LitRoot), pFileName, fVerbose );
+        int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, Abc_LitNot(LitRoot), pFileName, pPars->fVerbose );
         printf( "Dumping %d untestable multiple faults into file \"%s\".  ", nUntests, pFileName );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
@@ -782,7 +999,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
     Gia_ManStop( pM );
     sat_solver_delete( pSat );
     // dump the test suite
-    if ( fDump )
+    if ( pPars->fDump )
     {
         char * pFileName = "tests.txt";
         Gia_ManDumpTests( vTests, Iter, pFileName );