Added switch 'write_counter -f' to output flop values in each time frame.

src/aig/saig/saig.h

@@ -168,6 +168,7 @@ extern Aig_Man_t *       Saig_ManDupOrpos( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
 extern Aig_Man_t *       Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
 extern int               Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern Abc_Cex_t *       Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern Aig_Man_t *       Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
 /*=== saigHaig.c ==========================================================*/

src/aig/saig/saigDup.c

@@ -315,6 +315,58 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Abc_Cex_t * pNew;
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    // create new counter-example
+    pNew = Abc_CexAlloc( 0, Aig_ManPiNum(pAig), p->iFrame + 1 );
+    pNew->iPo = p->iPo;
+    pNew->iFrame = p->iFrame;
+    // simulate the AIG
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+        ///////// write PI+LO values ////////////
+        Aig_ManForEachPi( pAig, pObj, k )
+            if ( pObj->fMarkB )
+                Aig_InfoSetBit(pNew->pData, Aig_ManPiNum(pAig)*i + k);
+        /////////////////////////////////////////
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB;
+    Aig_ManCleanMarkB(pAig);
+    if ( RetValue == 0 )
+        printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
 {
     Aig_Obj_t * pObj, * pObjRi, * pObjRo;

src/base/io/io.c

@@ -2018,17 +2018,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
     char * pFileName;
-    int c, fNames;
-    int fMinimize;
-    int forceSeq;
-    int fVerbose;
+    int c, fNames  = 0;
+    int fMinimize  = 0;
+    int forceSeq   = 0;
+    int fPrintFull = 0;
+    int fVerbose   = 0;
 
-    fNames = 0;
-    fMinimize = 0;
-    forceSeq = 0;
-    fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "snmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "snmfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2041,6 +2038,9 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'm':
                 fMinimize ^= 1;
                 break;
+            case 'f':
+                fPrintFull ^= 1;
+                break;
             case 'v':
                 fVerbose ^= 1;
                 break;
@@ -2050,28 +2050,25 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
-
     pNtk = pAbc->pNtkCur;
     if ( pNtk == NULL )
     {
         fprintf( pAbc->Out, "Empty network.\n" );
         return 0;
     }
-
+    if ( pNtk->pModel == NULL && pAbc->pCex == NULL )
+    {
+        fprintf( pAbc->Out, "Counter-example is not available.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
     {
         printf( "File name is missing on the command line.\n" );
         goto usage;
     }
+
     // get the input file name
     pFileName = argv[globalUtilOptind];
-
-    if ( pNtk->pModel == NULL && pAbc->pCex == NULL )
-    {
-        fprintf( pAbc->Out, "Counter-example is not available.\n" );
-        return 0;
-    }
-
     // write the counter-example into the file
     if ( pAbc->pCex )
     { 
@@ -2093,7 +2090,20 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
             fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
             return 1;
         }
-        if ( fNames )
+        if ( fPrintFull )
+        {
+            extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+            Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+            Abc_Cex_t * pCexFull = Saig_ManExtendCex( pAig, pCex );
+            Aig_ManStop( pAig );
+            // output PI values (while skipping the minimized ones)
+            assert( pCexFull->nBits == Abc_NtkCiNum(pNtk) * (pCex->iFrame + 1) );
+            for ( f = 0; f <= pCex->iFrame; f++ )
+                Abc_NtkForEachCi( pNtk, pObj, i )
+                    fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
+            Abc_CexFreeP( &pCexFull );
+        }
+        else if ( fNames )
         {
             Abc_Cex_t * pCare = NULL;
             if ( fMinimize )
@@ -2154,12 +2164,13 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_counter [-snmvh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_counter [-snmfvh] <file>\n" );
     fprintf( pAbc->Err, "\t         saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
     fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
     fprintf( pAbc->Err, "\t-s     : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
     fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
     fprintf( pAbc->Err, "\t-m     : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
+    fprintf( pAbc->Err, "\t-f     : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" );  
     fprintf( pAbc->Err, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );