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

1 files changed, 38 insertions, 24 deletions

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