Added transformation of CEX after 'fix_aig' and checking of transformed CEXes using 'testcex -a'.

2 files changed, 89 insertions, 24 deletions

diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 6c9961a1..8481e582 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -712,6 +712,57 @@ Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose )
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resimulates CEX and return the ID of the PO that failed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p )
+{
+    Abc_Obj_t * pObj;
+    int RetValue, i, k, iBit = 0;
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( p->nPis  == Abc_NtkPiNum(pNtk) );
+    assert( p->nRegs == Abc_NtkLatchNum(pNtk) );
+    Abc_NtkCleanMarkC( pNtk );
+    Abc_AigConst1(pNtk)->fMarkC = 1;
+    // initialize flops
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
+    // simulate timeframes
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Abc_NtkForEachPi( pNtk, pObj, k )
+            pObj->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
+        Abc_NtkForEachNode( pNtk, pObj, k )
+            pObj->fMarkC = (Abc_ObjFanin0(pObj)->fMarkC ^ Abc_ObjFaninC0(pObj)) & 
+                           (Abc_ObjFanin1(pObj)->fMarkC ^ Abc_ObjFaninC1(pObj));
+        Abc_NtkForEachCo( pNtk, pObj, k )
+            pObj->fMarkC = Abc_ObjFanin0(pObj)->fMarkC ^ Abc_ObjFaninC0(pObj);
+        Abc_NtkForEachLatch( pNtk, pObj, k )
+            Abc_ObjFanout0(pObj)->fMarkC = Abc_ObjFanin0(pObj)->fMarkC;
+    }
+    assert( iBit == p->nBits );
+    // figure out the number of failed output
+    RetValue = -1;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pObj->fMarkC )
+        {
+            RetValue = i;
+            break;
+        }
+    }
+    Abc_NtkCleanMarkC( pNtk );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3fc68dda..3e0a26ff 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16185,13 +16185,16 @@ usage:
 int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
+    int c, fUseCex = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fUseCex ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -16205,6 +16208,35 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( fUseCex )
+    {
+        char * pInit; 
+        Abc_Cex_t * pTemp;
+        int k, nFlopsX = 0;
+        if ( pAbc->pCex == NULL )
+        {
+            Abc_Print( -1, "Current CEX is not available.\n" );
+            return 1;
+        }
+        pInit = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
+        // count the number of X-valued flops
+        for ( k = 0; k < Abc_NtkLatchNum(pAbc->pNtkCur); k++ )
+            nFlopsX += (int)(pInit[k] == 'x');
+        // compare this value
+        if ( Abc_NtkPiNum(pNtk) + nFlopsX != pAbc->pCex->nPis )
+        {
+            Abc_Print( -1, "The number of PIs (%d) plus X-valued flops (%d) in the original network does not match the number of PIs in the current CEX (%d).\n", 
+                Abc_NtkPiNum(pNtk), Abc_NtkLatchNum(pNtk), pAbc->pCex->nPis );
+            return 1;
+        }
+        pAbc->pCex = Abc_CexTransformUndc( pTemp = pAbc->pCex, pInit );
+        assert( pAbc->pCex->nPis == Abc_NtkPiNum(pAbc->pNtkCur) );
+        assert( pAbc->pCex->nRegs == Abc_NtkLatchNum(pAbc->pNtkCur) );
+        Abc_CexFree( pTemp );
+        ABC_FREE( pInit );
+        return 0;
+    }
+
     if ( Abc_NtkIsComb(pNtk) )
     {
         Abc_Print( -1, "The current network is combinational.\n" );
@@ -16222,8 +16254,9 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: undc [-h]\n" );
+    Abc_Print( -2, "usage: undc [-ch]\n" );
     Abc_Print( -2, "\t        converts latches with DC init values into free PIs\n" );
+    Abc_Print( -2, "\t-c    : toggles transforming CEX after \"logic;undc;st;zero\" [default = %s]\n", fUseCex? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -23617,28 +23650,17 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
         else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
             Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
-//      else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
-//          Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
-//      else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
-//          Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
         else
         {
-            Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-            Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
-    //        if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
+            extern int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p );
             int iPoOld = pAbc->pCex->iPo;
-            pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex, nOutputs );
+            pAbc->pCex->iPo = Abc_NtkVerifyCex( pNtk, pAbc->pCex );
             if ( pAbc->pCex->iPo == -1 )
-            {
-//                pAbc->pCex->iPo = iPoOld;
                 Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
-            }
             else if ( iPoOld != pAbc->pCex->iPo )
                 Abc_Print( 1, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
             else
                 Abc_Print( 1, "Main AIG: The cex is correct.\n" );
-            Gia_ManStop( pGia );
-            Aig_ManStop( pAig );
         }
     }
     else
@@ -23648,20 +23670,12 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "And  AIG: There is no current network.\n");
         else if ( Gia_ManPiNum(pAbc->pGia) != pAbc->pCex->nPis )
             Abc_Print( 1, "And  AIG: The number of PIs (%d) is different from cex (%d).\n", Gia_ManPiNum(pAbc->pGia), pAbc->pCex->nPis );
-//      else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
-//          Abc_Print( 1, "And  AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
-//      else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
-//          Abc_Print( 1, "And  AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
         else
         {
-    //        if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
             int iPoOld = pAbc->pCex->iPo;
             pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex, nOutputs );
             if ( pAbc->pCex->iPo == -1 )
-            {
-//                pAbc->pCex->iPo = iPoOld;
                 Abc_Print( 1, "And  AIG: The cex does not fail any outputs.\n" );
-            }
             else if ( iPoOld != pAbc->pCex->iPo )
                 Abc_Print( 1, "And  AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
             else