Adding switch &fftest -e to dump delay-tests in a special format.

src/base/abci/abc.c

@@ -36342,7 +36342,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, "ATNSGsbfduvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ATNSGsbfdeuvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -36409,6 +36409,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDump ^= 1;
             break;
+        case 'e':
+            pPars->fDumpDelay ^= 1;
+            break;
         case 'u':
             pPars->fDumpUntest ^= 1;
             break;
@@ -36490,7 +36493,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fftest [-ATN num] [-sbfduvh] <file> [-G file] [-S str]\n" );
+    Abc_Print( -2, "usage: &fftest [-ATN num] [-sbfdeuvh] <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" );
@@ -36504,6 +36507,7 @@ usage:
     Abc_Print( -2, "\t-b      : toggles testing for single faults only [default = %s]\n",                pPars->fBasic?      "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-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-v      : toggles printing verbose information [default = %s]\n",                  pPars->fVerbose?    "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");

src/sat/bmc/bmc.h

@@ -133,6 +133,7 @@ struct Bmc_ParFf_t_
     int        fBasic;
     int        fFfOnly;
     int        fDump;
+    int        fDumpDelay;
     int        fDumpUntest;
     int        fVerbose;
 };

src/sat/bmc/bmcFault.c

@@ -688,6 +688,70 @@ void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManDumpTestsSimulate( Gia_Man_t * p, Vec_Int_t * vValues )
+{
+    Gia_Obj_t * pObj; int k;
+    assert( Vec_IntSize(vValues) == Gia_ManCiNum(p) );
+    Gia_ManConst0(p)->fMark0 = 0;
+    Gia_ManForEachCi( p, pObj, k )
+        pObj->fMark0 = Vec_IntEntry( vValues, k );
+    Gia_ManForEachAnd( p, pObj, k )
+        pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                       (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+    Gia_ManForEachCo( p, pObj, k )
+        pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+    // collect flop input values
+    Vec_IntClear( vValues );
+    Gia_ManForEachRi( p, pObj, k )
+        Vec_IntPush( vValues, pObj->fMark0 );
+    assert( Vec_IntSize(vValues) == Gia_ManRegNum(p) );
+}
+void Gia_ManDumpTestsDelay( Vec_Int_t * vTests, int nIter, char * pFileName, Gia_Man_t * p )
+{
+    FILE * pFile = fopen( pFileName, "wb" );
+    Vec_Int_t * vValues = Vec_IntAlloc( Gia_ManCiNum(p) );
+    int i, v, nVars = Vec_IntSize(vTests) / nIter;
+    assert( Vec_IntSize(vTests) % nIter == 0 );
+    assert( nVars == 2 * Gia_ManPiNum(p) + Gia_ManRegNum(p) );
+    for ( i = 0; i < nIter; i++ )
+    {
+        // collect PIs followed by flops
+        Vec_IntClear( vValues );
+        for ( v = Gia_ManRegNum(p); v < Gia_ManCiNum(p); v++ )
+        {
+            fprintf( pFile, "%d", Vec_IntEntry(vTests, i * nVars + v) );
+            Vec_IntPush( vValues, Vec_IntEntry(vTests, i * nVars + v) );
+        }
+        for ( v = 0; v < Gia_ManRegNum(p); v++ )
+        {
+            fprintf( pFile, "%d", Vec_IntEntry(vTests, i * nVars + v) );
+            Vec_IntPush( vValues, Vec_IntEntry(vTests, i * nVars + v) );
+        }
+        fprintf( pFile, "\n" );
+        // derive next-state values
+        Gia_ManDumpTestsSimulate( p, vValues );
+        // collect PIs followed by flops
+        for ( v = Gia_ManCiNum(p); v < nVars; v++ )
+            fprintf( pFile, "%d", Vec_IntEntry(vTests, i * nVars + v) );
+        for ( v = 0; v < Vec_IntSize(vValues); v++ )
+            fprintf( pFile, "%d", Vec_IntEntry(vValues, v) );
+        fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
+    Vec_IntFree( vValues );
+}
+
+/**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+" );
@@ -1264,8 +1328,16 @@ finish:
     if ( pPars->fDump )
     {
         char * pFileName = "tests.txt";
-        Gia_ManDumpTests( vTests, Iter, pFileName );
-        printf( "Dumping %d computed test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
+        if ( pPars->fDumpDelay )
+        {
+            Gia_ManDumpTestsDelay( vTests, Iter, pFileName, p );
+            printf( "Dumping %d pairs of test patterns (total %d pattern) into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, 2*Vec_IntSize(vTests) / nFuncVars, pFileName );
+        }
+        else
+        {
+            Gia_ManDumpTests( vTests, Iter, pFileName );
+            printf( "Dumping %d test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
+        }
     }
 
     // compute untestable faults