Usability improvements to &fftest.

3 files changed, 32 insertions, 11 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 50bcfb26..e0734996 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41762,7 +41762,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Gia_ParFfSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfdeunvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfcdeunvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41840,6 +41840,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fFfOnly ^= 1;
             break;
+        case 'c':
+            pPars->fCheckUntest ^= 1;
+            break;
         case 'd':
             pPars->fDump ^= 1;
             break;
@@ -41930,7 +41933,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfdeunvh] <file> [-G file] [-S str]\n" );
+    Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfcdeunvh] <file> [-G file] [-S str]\n" );
     Abc_Print( -2, "\t          performs functional fault test generation\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" );
@@ -41945,9 +41948,10 @@ usage:
     Abc_Print( -2, "\t-b      : toggles testing for single faults (the same as \"-K 1\") [default = %s]\n", pPars->fBasic?      "yes": "no" );
     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-f      : toggles faults at flop inputs only with \"-A 1\" and \"-S str\" [default = %s]\n",          pPars->fFfOnly?     "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-c      : toggles checking if there are untestable faults [default = %s]\n",       pPars->fCheckUntest? "yes": "no" );
+    Abc_Print( -2, "\t-d      : toggles dumping test patterns into file \"<file>_tests.txt\" [default = %s]\n", pPars->fDump?       "yes": "no" );
     Abc_Print( -2, "\t-e      : toggles dumping test pattern pairs (delay faults only) [default = %s]\n", pPars->fDumpDelay? "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-u      : toggles dumping untestable faults into \"<file>_untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" );
     Abc_Print( -2, "\t-n      : toggles dumping faults not detected by a given test set [default = %s]\n", pPars->fDumpNewFaults? "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");
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index cef93bb1..12439faa 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -188,6 +188,7 @@ struct Bmc_ParFf_t_
     int        fNonStrict;
     int        fBasic;
     int        fFfOnly;
+    int        fCheckUntest;
     int        fDump;
     int        fDumpDelay;
     int        fDumpUntest;
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 0f63fa64..096d8aaa 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -22,6 +22,7 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "aig/gia/giaAig.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -58,6 +59,7 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
     p->nIterCheck    =     0;
     p->fBasic        =     0; 
     p->fFfOnly       =     0;
+    p->fCheckUntest  =     0; 
     p->fDump         =     0; 
     p->fDumpUntest   =     0; 
     p->fVerbose      =     0; 
@@ -476,6 +478,7 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
     int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0;
+    int VarLimit = 4 * Gia_ManAndNum(p);
     pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -484,22 +487,22 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        if ( Vec_IntEntry(vMap, iFuncVars++) )
+        if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
             iCtrl0 = Gia_ManAppendCi(pNew);
         else
             iCtrl0 = 0, Gia_ManAppendCi(pNew);
 
-        if ( Vec_IntEntry(vMap, iFuncVars++) )
+        if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
             iCtrl1 = Gia_ManAppendCi(pNew);
         else
             iCtrl1 = 0, Gia_ManAppendCi(pNew);
 
-        if ( Vec_IntEntry(vMap, iFuncVars++) )
+        if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
             iCtrl2 = Gia_ManAppendCi(pNew);
         else
             iCtrl2 = 0, Gia_ManAppendCi(pNew);
 
-        if ( Vec_IntEntry(vMap, iFuncVars++) )
+        if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
             iCtrl3 = Gia_ManAppendCi(pNew);
         else
             iCtrl3 = 0, Gia_ManAppendCi(pNew);
@@ -1441,6 +1444,19 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
         return;
     }
 
+    printf( "Options: " );
+    printf( "Untestable faults = %s. ", pPars->fCheckUntest || pPars->fDumpDelay ? "yes": "no" );
+    if ( pPars->nCardConstr )
+        printf( "Using %sstrict cardinality %d. ", pPars->fNonStrict ? "non-" : "", pPars->nCardConstr );
+    if ( pPars->fFfOnly )
+        printf( "Faults at FF outputs only = yes. " );
+    if ( pPars->nTimeOut )
+        printf( "Runtime limit = %d sec.  ", pPars->nTimeOut );
+    if ( p != pG && pG->pSpec )
+        printf( "Golden model = %s. ", pG->pSpec );
+    printf( "Verbose = %s. ", pPars->fVerbose ? "yes": "no" );
+    printf( "\n" );
+
     // select algorithm
     if ( pPars->Algo == 0 )
         nFuncVars = Gia_ManCiNum(p);
@@ -1565,7 +1581,7 @@ finish:
     // dump the test suite
     if ( pPars->fDump )
     {
-        char * pFileName = "tests.txt";
+        char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_tests.txt") : "tests.txt";
         if ( pPars->fDumpDelay && pPars->Algo == 1 )
         {
             Gia_ManDumpTestsDelay( vTests, Iter, pFileName, p );
@@ -1579,7 +1595,7 @@ finish:
     }
 
     // compute untestable faults
-    if ( Iter && (p != pG || pPars->fDumpUntest) )
+    if ( Iter && (p != pG || pPars->fDumpUntest || pPars->fCheckUntest) )
     {
         abctime clkTotal = Abc_Clock();
         // restart the SAT solver
@@ -1680,7 +1696,7 @@ finish:
         if ( pPars->fDumpUntest && status == l_True )
         {
             abctime clk = Abc_Clock();
-            char * pFileName = "untest.txt";
+            char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_untest.txt") : "untest.txt";
             int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose );
             if ( p == pG )
                 printf( "Dumped %d untestable multiple faults into file \"%s\".  ", nUntests, pFileName );