Adding symbolic fault representation in &fftest.

1 files changed, 264 insertions, 47 deletions

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