Enabled 'cec' to be applied to networks derived from BLIF with EXDCs.

4 files changed, 40 insertions, 5 deletions

diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index feeaa617..8c5a4a83 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n
     assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
     assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
     // check that the networks have the same PIs/POs/latches
-    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 0, fComb ) )
+    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fImplic, fComb ) )
         return NULL;
     // make sure the circuits are strashed 
     fRemove1 = (!Abc_NtkIsStrash(pNtk1) || Abc_NtkGetChoiceNum(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 38b21a13..d6883105 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -380,6 +380,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
 //        printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
 
     fflush( stdout );
+    if ( pNtk->pExdc )
+        Abc_NtkPrintStats( pNtk->pExdc, fFactored, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 8367d23c..7d9973b1 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -125,9 +125,32 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Prove_Params_t Params, * pParams = &Params;
 //    Fraig_Params_t Params;
 //    Fraig_Man_t * pMan;
-    Abc_Ntk_t * pMiter;
+    Abc_Ntk_t * pMiter, * pTemp;
+    Abc_Ntk_t * pExdc = NULL;
     int RetValue;
 
+    if ( pNtk1->pExdc != NULL || pNtk2->pExdc != NULL )
+    {
+        if ( pNtk1->pExdc != NULL && pNtk2->pExdc != NULL )
+        {
+            printf( "Comparing EXDC of the two networks:\n" );
+            Abc_NtkCecFraig( pNtk1->pExdc, pNtk2->pExdc, nSeconds, fVerbose );
+            printf( "Comparing networks under EXDC of the first network.\n" );
+            pExdc = pNtk1->pExdc;
+        }
+        else if ( pNtk1->pExdc != NULL )
+        {
+            printf( "Second network has no EXDC. Comparing main networks under EXDC of the first network.\n" );
+            pExdc = pNtk1->pExdc;
+        }
+        else if ( pNtk2->pExdc != NULL ) 
+        {
+            printf( "First network has no EXDC. Comparing main networks under EXDC of the second network.\n" );
+            pExdc = pNtk2->pExdc;
+        }
+        else assert( 0 );
+    }
+
     // get the miter of the two networks
     pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 );
     if ( pMiter == NULL )
@@ -135,6 +158,15 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
         printf( "Miter computation has failed.\n" );
         return;
     }
+    // add EXDC to the miter
+    if ( pExdc )
+    {
+        assert( Abc_NtkPoNum(pMiter) == 1 );
+        assert( Abc_NtkPoNum(pExdc) == 1 );
+        pMiter = Abc_NtkMiter( pTemp = pMiter, pExdc, 1, 0, 1, 0 );
+        Abc_NtkDelete( pTemp );
+    }
+    // handle trivial case
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 5b2a760a..e14c22c2 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -210,7 +210,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     {
         pNtk = (Abc_Ntk_t *)Vec_PtrEntry(pDesign->vModules, 0);
         Vec_PtrForEachEntryStart( Abc_Ntk_t *, pDesign->vModules, pExdc, i, 1 )
-            if ( !strcmp(pExdc->pName, "exdc") )
+            if ( !strcmp(pExdc->pName, "EXDC") )
             {
                 assert( pNtk->pExdc == NULL );
                 pNtk->pExdc = pExdc;
@@ -678,7 +678,8 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
         }
         else if ( !strncmp(pCur, "exdc", 4) )
         {
-            fprintf( stdout, "Line %d: The design contains EXDC network (warning only).\n", Io_MvGetLine(p, pCur) );
+//            fprintf( stdout, "Line %d: The design contains EXDC network (warning only).\n", Io_MvGetLine(p, pCur) );
+            fprintf( stdout, "Warning: The design contains EXDC network.\n" );
             if ( p->pLatest )
                 Vec_PtrPush( p->vModels, p->pLatest );
             p->pLatest = Io_MvModAlloc();
@@ -928,7 +929,7 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
     if ( pLine == NULL )
     {
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
-        p->pNtk->pName = Extra_UtilStrsav( "exdc" );
+        p->pNtk->pName = Extra_UtilStrsav( "EXDC" );
         return 1;
     }
     Io_MvSplitIntoTokens( vTokens, pLine, '\0' );