Experiments with delay fault testing.

2 files changed, 164 insertions, 15 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0c9e3098..9c8a2972 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -394,6 +394,7 @@ static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9FunFaTest          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -950,6 +951,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&funfatest",    Abc_CommandAbc9FunFaTest,    0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -32438,6 +32440,72 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose );
+    int c, nTimeOut = 0, fDump = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Tdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut < 0 )
+                goto usage;
+            break;
+        case 'd':
+            fDump ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): AIG is combinational.\n" );
+        return 0;
+    }
+    Gia_ManFaultTest( pAbc->pGia, nTimeOut, fDump, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &funfatest [-T num] [-dvh]\n" );
+    Abc_Print( -2, "\t         performs functional fault test generation\n" );
+    Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n",           nTimeOut );
+    Abc_Print( -2, "\t-d     : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", fDump? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",                  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     return -1;
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index bfc09cc1..49ed63d6 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -92,7 +92,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i, iThis;
+    int i, iCtrl, iThis;
     pNew = Gia_ManStart( (2 + 3 * fUseMuxes) * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -108,16 +108,17 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
         pObj->Value = Gia_ObjFanin0Copy(pObj);
     // add second timeframe
     Gia_ManForEachRo( p, pObj, i )
-        pObj->Value = Gia_ObjRoToRi(pNew, pObj)->Value;
+        pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
     Gia_ManForEachPi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
+        iCtrl = Gia_ManAppendCi( pNew );
         iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( fUseMuxes )
-            pObj->Value = Gia_ManHashMux( pNew, Gia_ManAppendCi(pNew), iThis, pObj->Value );
+            pObj->Value = Gia_ManHashMux( pNew, iCtrl, iThis, pObj->Value );
         else
-            pObj->Value = iThis, Gia_ManAppendCi(pNew);
+            pObj->Value = iThis;
     }
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
@@ -175,12 +176,66 @@ Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFaultTest( Gia_Man_t * p )
+void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter )
 {
-    int nTimeOut = 0;
-    int nIterMax = 100;
-    int i, status;
-    Vec_Int_t * vLits;
+    FILE * pFile = fopen( "tests.txt", "wb" );
+    int i, k, v, nVars = Vec_IntSize(vTests) / nIter;
+    assert( Vec_IntSize(vTests) % nIter == 0 );
+    for ( v = i = 0; i < nIter; i++, fprintf(pFile, "\n") )
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, "%d", Vec_IntEntry(vTests, v++) );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime clk )
+{
+    FILE * pTable = fopen( "fault_stats.txt", "a+" );
+
+    fprintf( pTable, "%s ", Gia_ManName(p) );
+    fprintf( pTable, "%d ", Gia_ManPiNum(p) );
+    fprintf( pTable, "%d ", Gia_ManPoNum(p) );
+    fprintf( pTable, "%d ", Gia_ManRegNum(p) );
+    fprintf( pTable, "%d ", Gia_ManAndNum(p) );
+
+    fprintf( pTable, "%d ", sat_solver_nvars(pSat) );
+    fprintf( pTable, "%d ", sat_solver_nclauses(pSat) );
+    fprintf( pTable, "%d ", sat_solver_nconflicts(pSat) );
+
+    fprintf( pTable, "%d ", nIter );
+    fprintf( pTable, "%.2f", 1.0*clk/CLOCKS_PER_SEC );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose )
+{
+    int nIterMax = 1000000;
+    int i, Iter, status;
+    abctime clkTotal = Abc_Clock();
+    abctime clkSat = 0;
+    Vec_Int_t * vLits, * vTests;
     sat_solver * pSat;
     Gia_Obj_t * pObj;
     Gia_Man_t * pC;
@@ -190,10 +245,11 @@ void Gia_ManFaultTest( Gia_Man_t * p )
     Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM ), * pCnf2;
     Gia_ManStop( p0 );
     Gia_ManStop( p1 );
+    assert( Gia_ManRegNum(p) > 0 );
 
     // start the SAT solver
     pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, pCnf->nVars * 10 );
+    sat_solver_setnvars( pSat, pCnf->nVars );
     sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
     // add timeframe clauses
     for ( i = 0; i < pCnf->nClauses; i++ )
@@ -207,17 +263,33 @@ void Gia_ManFaultTest( Gia_Man_t * p )
     sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
 
     // iterate through the test vectors
-    for ( i = 0; i < nIterMax; i++ )
+    vTests = Vec_IntAlloc( 10000 );
+    for ( Iter = 0; Iter < nIterMax; Iter++ )
     {
+        abctime clk = Abc_Clock();
         status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        clkSat += Abc_Clock() - clk;
+        if ( fVerbose )
+        {
+            printf( "Iter%6d : ",       Iter );
+            printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
+            printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
+            printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
+//            Abc_PrintTime( 1, "Time", clkSat );
+            ABC_PRTr( "Solver time", clkSat );
+        }
         if ( status == l_Undef )
         {
-            printf( "Timeout reached after %d seconds.\n", nTimeOut );
+            if ( fVerbose )
+                printf( "\n" );
+            printf( "Timeout reached after %d seconds and %d iterations.  ", nTimeOut, Iter );
             break;
         }
         if ( status == l_False )
         {
-            printf( "The problem is UNSAT.\n" );
+            if ( fVerbose )
+                printf( "\n" );
+            printf( "The problem is UNSAT after %d iterations.  ", Iter );
             break;
         }
         assert( status == l_True );
@@ -226,11 +298,12 @@ void Gia_ManFaultTest( Gia_Man_t * p )
         Gia_ManForEachPi( pM, pObj, i )
             if ( i < Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p) )
                 Vec_IntPush( vLits, sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) );
+        Vec_IntAppend( vTests, vLits );
         // derive the cofactor
         pC = Gia_ManFaultCofactor( pM, vLits );
         // derive new CNF
         pCnf2 = Cnf_DeriveGiaRemapped( pC );
-        Cnf_DataLiftGia( pCnf2, pC, pCnf->nVars );
+        Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) );
         // add timeframe clauses
         for ( i = 0; i < pCnf2->nClauses; i++ )
             if ( !sat_solver_addclause( pSat, pCnf2->pClauses[i], pCnf2->pClauses[i+1] ) )
@@ -238,7 +311,7 @@ void Gia_ManFaultTest( Gia_Man_t * p )
         // add constraint clauses
         Gia_ManForEachPo( pC, pObj, i )
         {
-            int Lit = Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pC, pObj)], 1);
+            int Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 );
             if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
                 assert( 0 );
         }
@@ -249,11 +322,19 @@ void Gia_ManFaultTest( Gia_Man_t * p )
         Cnf_DataFree( pCnf2 );
         Gia_ManStop( pC );
     }
+    // print results
+//    if ( status == l_False )
+//        Gia_ManPrintResults( p, pSat, Iter, Abc_Clock() - clkTotal );
     // cleanup
     Vec_IntFree( vLits );
     sat_solver_delete( pSat );
     Cnf_DataFree( pCnf );
     Gia_ManStop( pM );
+    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    // dump the test suite
+    if ( fDump )
+        Gia_ManDumpTests( vTests, Iter );
+    Vec_IntFree( vTests );
 }
 
 ////////////////////////////////////////////////////////////////////////