Improvements to the hierarchy/timing manager.

1 files changed, 14 insertions, 12 deletions

diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 01601625..a00c6d0c 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -529,22 +529,24 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
     }
     // if timing managers have different number of black boxes,
     // it is possible that some of the boxes are swept away
-    // but specification cannot have fewer boxes than implementation
-    if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) < Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+    if ( Tim_ManBlackBoxNum( (Tim_Man_t *)pSpec->pManTime ) > 0 )
     {
-        printf( "Spec has more boxes than the design. Cannot proceed.\n" );
-        return Status;
-    }
-    // in this case, it is expected that the boxes can be aligned
-    // find what boxes of pSpec are dropped in pGia
-    if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) != Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
-    {
-        vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
-        if ( vBoxPres == NULL )
+        // specification cannot have fewer boxes than implementation
+        if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) < Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
         {
-            printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
+            printf( "Spec has more boxes than the design. Cannot proceed.\n" );
             return Status;
         }
+        // to align the boxes, find what boxes of pSpec are dropped in pGia
+        if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) != Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+        {
+            vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
+            if ( vBoxPres == NULL )
+            {
+                printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
+                return Status;
+            }
+        }
     }
     // collapse two designs
     pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres );