Fixing the problem with outputting word-level CEXes after retiming.

5 files changed, 45 insertions, 19 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index e68985f3..0703d775 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2292,6 +2292,35 @@ ABC_NAMESPACE_IMPL_END
 
 ABC_NAMESPACE_IMPL_START
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void IoCommandPrintLatchName( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Obj_t * pObj, char * pObjName, Abc_Cex_t * pCex, Abc_Cex_t * pCare )
+{
+    int ii, NameLen = strlen(pObjName);
+    // check if there is a PI with a matching name
+    Abc_Obj_t * pObjPi;
+    Abc_NtkForEachPi( pNtk, pObjPi, ii )
+        if ( !strncmp(Abc_ObjName(pObjPi), pObjName, NameLen) && !strncmp(Abc_ObjName(pObjPi)+NameLen, "_init", 5) )
+        {
+            if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+ii) )
+                fprintf( pFile, "%s@%d=%c\n", pObjName, 0, '0'+Abc_InfoHasBit(pCex->pData, pCare->nRegs+ii) );
+            break;
+        }
+    if ( ii != Abc_NtkPiNum(pNtk) )
+        return;
+    if ( !strncmp(pObjName, "abc_reset_flop", 14) )
+        return;
+    fprintf( pFile, "%s@0=%c\n", pObjName, '0'+ (pObj ? !Abc_LatchIsInit0(pObj) : 0) );
+}
 
 /**Function*************************************************************
 
@@ -2307,6 +2336,7 @@ ABC_NAMESPACE_IMPL_START
 int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
+    Vec_Ptr_t * vNamesIn = NULL;
     char * pFileName;
     int c, fNames  = 0;
     int fMinimize  = 0;
@@ -2417,6 +2447,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
         else if ( fNames )
         {
             Abc_Cex_t * pCare = NULL;
+            char * pObjName = NULL;
             if ( fMinimize )
             {
                 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
@@ -2445,25 +2476,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
             fprintf( pFile, "\n");                                           
             fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
             // output flop values (unaffected by the minimization)
-            Abc_NtkForEachLatch( pNtk, pObj, i )
-            {
-                char * pObjName = Abc_ObjName(Abc_ObjFanout0(pObj));
-                int ii, NameLen = strlen(pObjName);
-                // check if there is a PI with a matching name
-                Abc_Obj_t * pObjPi;
-                Abc_NtkForEachPi( pNtk, pObjPi, ii )
-                    if ( !strncmp(Abc_ObjName(pObjPi), pObjName, NameLen) && !strncmp(Abc_ObjName(pObjPi)+NameLen, "_init", 5) )
-                    {
-                        if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+ii) )
-                            fprintf( pFile, "%s@%d=%c\n", pObjName, 0, '0'+Abc_InfoHasBit(pCex->pData, pCare->nRegs+ii) );
-                        break;
-                    }
-                if ( ii != Abc_NtkPiNum(pNtk) )
-                    continue;
-                if ( !strncmp(pObjName, "abc_reset_flop", 14) )
-                    continue;
-                fprintf( pFile, "%s@0=%c\n", pObjName, '0'+!Abc_LatchIsInit0(pObj) );
-            }
+            if ( (vNamesIn = Abc_FrameReadCexCiNames(pAbc)) != NULL )
+                Vec_PtrForEachEntryStart( char *, vNamesIn, pObjName, i, Abc_NtkPiNum(pNtk) )
+                    IoCommandPrintLatchName( pFile, pNtk, NULL, pObjName, pCex, pCare );
+            else
+                Abc_NtkForEachLatch( pNtk, pObj, i )
+                    IoCommandPrintLatchName( pFile, pNtk, pObj, Abc_ObjName(Abc_ObjFanout0(pObj)), pCex, pCare );
             // output PI values (while skipping the minimized ones)
             for ( f = 0; f <= pCex->iFrame; f++ )
                 Abc_NtkForEachPi( pNtk, pObj, i )
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 2efb3358..f4ec90e2 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -127,6 +127,8 @@ extern ABC_DLL int             Abc_FrameReadCexPiNum( Abc_Frame_t * p );
 extern ABC_DLL int             Abc_FrameReadCexRegNum( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadCexPo( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadCexFrame( Abc_Frame_t * p );              
+extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadCexCiNames( Abc_Frame_t * p );              
+extern ABC_DLL void            Abc_FrameSetCexCiNames( Vec_Ptr_t * vNames );              
 
 extern ABC_DLL void            Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); 
 extern ABC_DLL void            Abc_FrameSetNtkStoreSize( int nStored );  
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 1d54f4e4..71b21eb1 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -83,6 +83,9 @@ int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFr
 int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFrame->pCex->nRegs;  }               
 int         Abc_FrameReadCexPo( Abc_Frame_t * p )            { return s_GlobalFrame->pCex->iPo;    }               
 int         Abc_FrameReadCexFrame( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->iFrame; }               
+Vec_Ptr_t * Abc_FrameReadCexCiNames( Abc_Frame_t * p )       { return s_GlobalFrame->vCiNamesStore; }              
+void        Abc_FrameSetCexCiNames( Vec_Ptr_t * vNames )     { if ( s_GlobalFrame->vCiNamesStore ) Vec_PtrFreeFree(s_GlobalFrame->vCiNamesStore); s_GlobalFrame->vCiNamesStore = vNames; }
+
 
 void        Abc_FrameInputNdr( Abc_Frame_t * pAbc, void * pData ) { Ndr_Delete(s_GlobalFrame->pNdr); s_GlobalFrame->pNdr = pData;                        }
 void *      Abc_FrameOutputNdr( Abc_Frame_t * pAbc )         { void * pData = s_GlobalFrame->pNdr; s_GlobalFrame->pNdr = NULL; return pData;             }  
@@ -240,6 +243,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     Vec_WecFreeP( &s_GlobalFrame->vJsonObjs );  
     Ndr_Delete( s_GlobalFrame->pNdr );
     ABC_FREE( s_GlobalFrame->pNdrArray );
+    Vec_PtrFreeFree( s_GlobalFrame->vCiNamesStore );
 
     Gia_ManStopP( &p->pGiaMiniAig );
     Gia_ManStopP( &p->pGiaMiniLut );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 7317c36f..b5a914e4 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -152,6 +152,7 @@ struct Abc_Frame_t_
     int *           pBoxes;
     void *          pNdr;
     int *           pNdrArray;
+    Vec_Ptr_t *     vCiNamesStore;  // storage for CI names
 
     Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
 };
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index a4fc9549..80313c7a 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -1124,6 +1124,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "Finished dumping file \"pio_name_map.txt\" containing PI/PO name mapping.\n" );
         }
     }
+    Abc_FrameSetCexCiNames( Vec_PtrDupStr(pNew->vNamesIn) );
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage: