Adding switch to handle only single faults.

7 files changed, 104 insertions, 24 deletions

diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c
index 71a6547d..19cdf9e6 100644
--- a/src/aig/gia/giaCCof.c
+++ b/src/aig/gia/giaCCof.c
@@ -128,7 +128,7 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
                 Gia_ObjFaninId0(pObj, i), 
                 Gia_ObjFaninId1(pObj, i), 
                 Gia_ObjFaninC0(pObj), 
-                Gia_ObjFaninC1(pObj) ); 
+                Gia_ObjFaninC1(pObj), 0 ); 
     }
     sat_solver_setnvars( p->pSat, Gia_ManObjNum(p->pFrames) );
 }
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c
index c7a5a638..c918559f 100644
--- a/src/aig/gia/giaFalse.c
+++ b/src/aig/gia/giaFalse.c
@@ -180,10 +180,10 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
             continue;
         sat_solver_add_and( pSat, pObj->Value + Shift[0], 
             Gia_ObjFanin0(pObj)->Value + Shift[0], Gia_ObjFanin1(pObj)->Value + Shift[0], 
-            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) ); 
+            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
         sat_solver_add_and( pSat, pObj->Value + Shift[1], 
             Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1], 
-            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) ); 
+            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
     }
     // call the SAT solver
     status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9c4c587..acdfb9f8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32880,11 +32880,11 @@ 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 fDump, int fDumpUntest, int fVerbose );
-    int c, Algo = 0, fComplVars = 0, fStartPats = 0, nTimeOut = 0, fDump = 0, fDumpUntest = 0, fVerbose = 0;
+    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;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ATcsduvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ATcsbduvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32916,6 +32916,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fStartPats ^= 1;
             break;
+        case 'b':
+            fBasic ^= 1;
+            break;
         case 'd':
             fDump ^= 1;
             break;
@@ -32955,11 +32958,11 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9FFTest(): For delay testing, AIG should be sequential.\n" );
         return 0;
     }
-    Gia_ManFaultTest( pAbc->pGia, pFileName, Algo, fComplVars, fStartPats, nTimeOut, fDump, fDumpUntest, fVerbose );
+    Gia_ManFaultTest( pAbc->pGia, pFileName, Algo, fComplVars, fStartPats, nTimeOut, fBasic, fDump, fDumpUntest, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fftest [-AT num] [-csduvh] <file>\n" );
+    Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <file>\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               0: algorithm is not selected\n" );
@@ -32970,6 +32973,7 @@ usage:
     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" );
diff --git a/src/map/if/ifSelect.c b/src/map/if/ifSelect.c
index 78557583..21e3be72 100644
--- a/src/map/if/ifSelect.c
+++ b/src/map/if/ifSelect.c
@@ -455,7 +455,7 @@ int If_ManNodeShapeSat( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape
         assert( Vec_IntSize(vFanins) > 0 );
         sat_solver_add_choice( pSat, If_ObjSatVar(pObj), vFanins ); // external
         assert( If_ObjSatVar(pObj) > 0 );
-//        sat_solver_add_and( pSat, If_ObjSatVar(pObj)+1, If_ObjSatVar(pObj->pFanin0), If_ObjSatVar(pObj->pFanin1), 0, 0 );
+//        sat_solver_add_and( pSat, If_ObjSatVar(pObj)+1, If_ObjSatVar(pObj->pFanin0), If_ObjSatVar(pObj->pFanin1), 0, 0, 0 );
         if ( If_ObjSatVar(pObj->pFanin0) > 0 && If_ObjSatVar(pObj->pFanin1) > 0 )
         {
             int Lits[2];
diff --git a/src/proof/int2/int2Bmc.c b/src/proof/int2/int2Bmc.c
index cd7f1a74..641bfb84 100644
--- a/src/proof/int2/int2Bmc.c
+++ b/src/proof/int2/int2Bmc.c
@@ -293,7 +293,7 @@ void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos )
                 if ( Entry < Gia_ManObjNum(pFrames) )
                 {
                     assert( !Abc_LitIsCompl(iLit) );
-                    sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); 
+                    sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 ); 
                 }
             }
             else
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index b4a540a4..8f7d8c9b 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -36,6 +36,67 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Add constraint that no more than 1 variable is 1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cnf_AddCardinConstr( sat_solver * p, Vec_Int_t * vVars )
+{
+    int i, k, pLits[2], iVar, nVars = sat_solver_nvars(p);
+    Vec_IntForEachEntry( vVars, iVar, i )
+        assert( iVar >= 0 && iVar < nVars );
+    iVar = nVars;
+    sat_solver_setnvars( p, nVars + Vec_IntSize(vVars) - 1 );
+    while ( Vec_IntSize(vVars) > 1 )
+    {
+        for ( k = i = 0; i < Vec_IntSize(vVars)/2; i++ )
+        {
+            pLits[0] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i), 1 );
+            pLits[1] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i+1), 1 );
+            sat_solver_addclause( p, pLits, pLits + 2 );
+            sat_solver_add_and( p, iVar, Vec_IntEntry(vVars, 2*i), Vec_IntEntry(vVars, 2*i+1), 1, 1, 1 );
+            Vec_IntWriteEntry( vVars, k++, iVar++ );
+        }
+        if ( Vec_IntSize(vVars) & 1 )
+            Vec_IntWriteEntry( vVars, k++, Vec_IntEntryLast(vVars) );
+        Vec_IntShrink( vVars, k );
+    }
+    return iVar;
+}
+void Cnf_AddCardinConstrTest()
+{
+    int i, status, nVars = 7;
+    Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
+    sat_solver * pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, nVars );
+    Cnf_AddCardinConstr( pSat, vVars );
+    while ( 1 )
+    {
+        status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+        if ( status != l_True )
+            break;
+        Vec_IntClear( vVars );
+        for ( i = 0; i < nVars; i++ )
+        {
+            Vec_IntPush( vVars, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
+            printf( "%d", sat_solver_var_value(pSat, i) );
+        }
+        printf( "\n" );
+        status = sat_solver_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
+        if ( status == 0 )
+            break;
+    }
+    sat_solver_delete( pSat );
+    Vec_IntFree( vVars );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -503,7 +564,7 @@ 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 fDump, int fDumpUntest, int fVerbose )
+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 nIterMax = 1000000;
     int i, Iter, LitRoot, status, nFuncVars = -1;
@@ -516,19 +577,29 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
 
     // select algorithm
     if ( Algo == 1 )
-        nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
+        printf( "FFTEST is computing test patterns for %sdelay faults...\n", fBasic ? "single " : "" );
     else if ( Algo == 2 )
-        nFuncVars = Gia_ManCiNum(p);
+        printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", fBasic ? "single " : "" );
     else if ( Algo == 3 )
-        nFuncVars = Gia_ManCiNum(p);
+        printf( "FFTEST is computing test patterns for %scomplement faults...\n", fBasic ? "single " : "" );
     else if ( Algo == 4 )
-        nFuncVars = Gia_ManCiNum(p);
+        printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", fBasic ? "single " : "" );
     else
     {
         printf( "Unregnized algorithm (%d).\n", Algo );
         return;
     }
 
+    // select algorithm
+    if ( Algo == 1 )
+        nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
+    else if ( Algo == 2 )
+        nFuncVars = Gia_ManCiNum(p);
+    else if ( Algo == 3 )
+        nFuncVars = Gia_ManCiNum(p);
+    else if ( Algo == 4 )
+        nFuncVars = Gia_ManCiNum(p);
+
     // collect test patterns from file
     if ( pFileName )
         vTests = Gia_ManGetTestPatterns( pFileName );
@@ -565,11 +636,6 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
         p0 = Gia_ManFOFUnfold( p, 0, fComplVars );
         p1 = Gia_ManFOFUnfold( p, 1, fComplVars );
     }
-    else
-    {
-        printf( "Unregnized algorithm (%d).\n", Algo );
-        return;
-    }
 
     // create miter
     pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
@@ -595,6 +661,16 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
         Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
     sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
 
+    // add cadinality constraint
+    if ( fBasic )
+    {
+        Vec_IntClear( vLits );
+        Gia_ManForEachPi( pM, pObj, i )
+            if ( i >= nFuncVars )
+                Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
+        Cnf_AddCardinConstr( pSat, vLits );
+    }
+
     // add available test-patterns
     if ( Vec_IntSize(vTests) > 0 )
     {
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 1003d54a..fb19490c 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -315,22 +315,22 @@ static inline int sat_solver_add_buffer_enable( sat_solver * pSat, int iVarA, in
     assert( Cid );
     return 2;
 }
-static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
+static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
 {
     lit Lits[3];
     int Cid;
 
-    Lits[0] = toLitCond( iVar, 1 );
+    Lits[0] = toLitCond( iVar, !fCompl );
     Lits[1] = toLitCond( iVar0, fCompl0 );
     Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
     assert( Cid );
 
-    Lits[0] = toLitCond( iVar, 1 );
+    Lits[0] = toLitCond( iVar, !fCompl );
     Lits[1] = toLitCond( iVar1, fCompl1 );
     Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
     assert( Cid );
 
-    Lits[0] = toLitCond( iVar, 0 );
+    Lits[0] = toLitCond( iVar, fCompl );
     Lits[1] = toLitCond( iVar0, !fCompl0 );
     Lits[2] = toLitCond( iVar1, !fCompl1 );
     Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );