Improvements to the hierarchy/timing manager.

7 files changed, 160 insertions, 24 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 );
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index bbe0bbd1..bdf0613e 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -23,7 +23,7 @@
 
 ABC_NAMESPACE_IMPL_START
 
-//#define USE_ABC2
+#define USE_ABC2
 //#define USE_ABC85
  
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/if.h b/src/map/if/if.h
index e8a4c604..a22c4841 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -318,8 +318,11 @@ typedef struct If_Box_t_ If_Box_t;
 struct If_Box_t_
 {
     char *             pName;
+    char               fSeq;
+    char               fBlack;
+    char               fOuter;
+    char               fUnused;
     int                Id;
-    int                fBlack;
     int                nPis;
     int                nPos;
     int *              pDelays;
@@ -506,8 +509,10 @@ extern float           If_LibLutSlowestPinDelay( If_LibLut_t * p );
 extern If_LibBox_t *   If_LibBoxStart();
 extern void            If_LibBoxFree( If_LibBox_t * p );
 extern If_Box_t *      If_LibBoxReadBox( If_LibBox_t * p, int Id );
+extern If_Box_t *      If_LibBoxFindBox( If_LibBox_t * p, char * pName );
 extern void            If_LibBoxAdd( If_LibBox_t * p, If_Box_t * pBox );
 extern If_LibBox_t *   If_LibBoxRead( char * pFileName );
+extern If_LibBox_t *   If_LibBoxRead2( char * pFileName );
 extern void            If_LibBoxPrint( FILE * pFile, If_LibBox_t * p );
 extern void            If_LibBoxWrite( char * pFileName, If_LibBox_t * p );
 /*=== ifMan.c =============================================================*/
diff --git a/src/map/if/ifCom.c b/src/map/if/ifCom.c
index b14d857e..fda791c2 100644
--- a/src/map/if/ifCom.c
+++ b/src/map/if/ifCom.c
@@ -241,6 +241,7 @@ int If_CommandReadBox( Abc_Frame_t * pAbc, int argc, char **argv )
     If_LibBox_t * pLib;
     Abc_Ntk_t * pNet;
     char * FileName;
+    int fExtended;
     int fVerbose;
     int c;
 
@@ -249,12 +250,16 @@ int If_CommandReadBox( Abc_Frame_t * pAbc, int argc, char **argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set the defaults
+    fExtended = 0;
     fVerbose = 1;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) 
+    while ( (c = Extra_UtilGetopt(argc, argv, "evh")) != EOF ) 
     {
         switch (c) 
         {
+            case 'e':
+                fExtended ^= 1;
+                break;
             case 'v':
                 fVerbose ^= 1;
                 break;
@@ -282,7 +287,7 @@ int If_CommandReadBox( Abc_Frame_t * pAbc, int argc, char **argv )
     fclose( pFile );
 
     // set the new network
-    pLib = If_LibBoxRead( FileName );
+    pLib = fExtended ? If_LibBoxRead2( FileName ) : If_LibBoxRead( FileName );
     if ( pLib == NULL )
     {
         fprintf( pErr, "Reading LUT library has failed.\n" );
@@ -294,8 +299,9 @@ int If_CommandReadBox( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pErr, "\nusage: read_box [-vh]\n");
+    fprintf( pErr, "\nusage: read_box [-evh]\n");
     fprintf( pErr, "\t          read the box library from the file\n" );  
+    fprintf( pErr, "\t-e      : toggles reading extended format [default = %s]\n", (fExtended? "yes" : "no") );
     fprintf( pErr, "\t-v      : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") );
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;       /* error exit */
diff --git a/src/map/if/ifLibBox.c b/src/map/if/ifLibBox.c
index 042cb7f1..f420cf36 100644
--- a/src/map/if/ifLibBox.c
+++ b/src/map/if/ifLibBox.c
@@ -45,13 +45,15 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-If_Box_t * If_BoxStart( char * pName, int Id, int fBlack, int nPis, int nPos )
+If_Box_t * If_BoxStart( char * pName, int Id, int nPis, int nPos, int fSeq, int fBlack, int fOuter )
 {
     If_Box_t * p;
     p = ABC_CALLOC( If_Box_t, 1 );
     p->pName   = pName; // consumes memory
     p->Id      = Id;
-    p->fBlack  = fBlack;
+    p->fSeq    = (char)fSeq;
+    p->fBlack  = (char)fBlack;
+    p->fOuter  = (char)fOuter;
     p->nPis    = nPis;
     p->nPos    = nPos;
     p->pDelays = ABC_CALLOC( int, nPis * nPos );
@@ -119,6 +121,17 @@ If_Box_t * If_LibBoxReadBox( If_LibBox_t * p, int Id )
 {
     return (If_Box_t *)Vec_PtrEntry( p->vBoxes, Id );
 }
+If_Box_t * If_LibBoxFindBox( If_LibBox_t * p, char * pName )
+{
+    If_Box_t * pBox;
+    int i;
+    if ( p == NULL )
+        return NULL;
+    If_LibBoxForEachBox( p, pBox, i )
+        if ( !strcmp(pBox->pName, pName) )
+            return pBox;
+    return NULL;
+}
 void If_LibBoxAdd( If_LibBox_t * p, If_Box_t * pBox )
 {
     if ( pBox->Id >= Vec_PtrSize(p->vBoxes) )
@@ -127,6 +140,99 @@ void If_LibBoxAdd( If_LibBox_t * p, If_Box_t * pBox )
     Vec_PtrWriteEntry( p->vBoxes, pBox->Id, pBox );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_LibBox_t * If_LibBoxRead2( char * pFileName )
+{
+    int nSize = 100000;
+    char * pBuffer;
+    FILE * pFile;
+    If_LibBox_t * p = NULL;
+    If_Box_t * pBox = NULL;
+    char * pToken, * pName;
+    int fSeq, fBlack, fOuter;
+    int i, Id, nPis, nPos;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    // read lines
+    nPis = nPos = 0;
+    pBuffer = ABC_ALLOC( char, nSize );
+    while ( fgets( pBuffer, nSize, pFile ) )
+    {
+        pToken = strtok( pBuffer, " \n\r\t" );
+        if ( pToken == NULL )
+            continue;
+        if ( pToken[0] == '.' )
+        {
+            if ( !strcmp(pToken, ".box") )
+            {
+                // save ID
+                pToken = strtok( NULL, " \n\r\t" );
+                Id     = atoi( pToken );
+                // save name
+                pToken = strtok( NULL, " \n\r\t" );
+                pName  = Abc_UtilStrsav(pToken);
+                // save PIs
+                pToken = strtok( NULL, " \n\r\t" );
+                nPis   = atoi( pToken );
+                // save POs
+                pToken = strtok( NULL, " \n\r\t" );
+                nPos   = atoi( pToken );
+                // save attributes
+                fSeq = fBlack = fOuter = 0;
+                pToken = strtok( NULL, " \n\r\t" );
+                while ( pToken )
+                {
+                    if ( !strcmp(pToken, "seq") )
+                        fSeq = 1;
+                    else if ( !strcmp(pToken, "black") )
+                        fBlack = 1;
+                    else if ( !strcmp(pToken, "outer") )
+                        fOuter = 1;
+                    else assert( !strcmp(pToken, "comb") || !strcmp(pToken, "white") || !strcmp(pToken, "inner") );
+                    pToken = strtok( NULL, " \n\r\t" );
+                }
+                // create library
+                if ( p == NULL )
+                    p = If_LibBoxStart();
+                // create box
+                pBox = If_BoxStart( pName, Id, nPis, nPos, fSeq, fBlack, fOuter );
+                If_LibBoxAdd( p, pBox );
+            }
+            continue;
+        }
+        // read the table
+        assert( nPis > 0 && nPos > 0 );
+        for ( i = 0; i < nPis * nPos; i++ )
+        {
+            while ( pToken == NULL )
+            {
+                fgets( pBuffer, nSize, pFile );
+                pToken = strtok( pBuffer, " \n\r\t" );
+            }
+            pBox->pDelays[i] = (pToken[0] == '-') ? -1 : atoi(pToken);
+            pToken = strtok( NULL, " \n\r\t" );
+        }
+        pBox = NULL;
+    }
+    ABC_FREE( pBuffer );
+    fclose( pFile );
+    return p;
+}
+
 
 /**Function*************************************************************
 
@@ -167,9 +273,8 @@ If_LibBox_t * If_LibBoxRead( char * pFileName )
     FILE * pFile;
     If_LibBox_t * p;
     If_Box_t * pBox;
-    char * pToken;
-    char * pName;
-    int i, Id, fWhite, nPis, nPos;
+    char * pToken, * pName;
+    int i, Id, fBlack, nPis, nPos;
     pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
     {
@@ -180,9 +285,17 @@ If_LibBox_t * If_LibBoxRead( char * pFileName )
     pToken = If_LibBoxGetToken( pFile );
     if ( pToken == NULL )
     {
+        fclose( pFile );
         printf( "Cannot read library name from file \"%s\".\n", pFileName );
         return NULL;
     }
+    if ( pToken[0] == '.' )    
+    {
+        fclose( pFile );
+        printf( "Wrong box format. Please try \"read_box -e\".\n" );
+        return NULL;
+    }
+       
     // create library
     p = If_LibBoxStart();
     while ( pToken )
@@ -194,7 +307,7 @@ If_LibBox_t * If_LibBoxRead( char * pFileName )
         Id     = atoi( pToken );
         // save white/black
         pToken = If_LibBoxGetToken( pFile );
-        fWhite = atoi( pToken );
+        fBlack = !atoi( pToken );
         // save PIs
         pToken = If_LibBoxGetToken( pFile );
         nPis   = atoi( pToken );
@@ -202,7 +315,7 @@ If_LibBox_t * If_LibBoxRead( char * pFileName )
         pToken = If_LibBoxGetToken( pFile );
         nPos   = atoi( pToken );
         // create box
-        pBox   = If_BoxStart( pName, Id, !fWhite, nPis, nPos );
+        pBox   = If_BoxStart( pName, Id, nPis, nPos, 0, fBlack, 0 );
         If_LibBoxAdd( p, pBox );
         // read the table
         for ( i = 0; i < nPis * nPos; i++ )
diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h
index df787748..ba2b1bdb 100644
--- a/src/misc/tim/tim.h
+++ b/src/misc/tim/tim.h
@@ -143,6 +143,7 @@ extern int             Tim_ManCoNum( Tim_Man_t * p );
 extern int             Tim_ManPiNum( Tim_Man_t * p );
 extern int             Tim_ManPoNum( Tim_Man_t * p );
 extern int             Tim_ManBoxNum( Tim_Man_t * p );
+extern int             Tim_ManBlackBoxNum( Tim_Man_t * p );
 extern int             Tim_ManDelayTableNum( Tim_Man_t * p );
 extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
 extern void            Tim_ManTravIdDisable( Tim_Man_t * p );
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 51a0c381..9aec1190 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -607,6 +607,15 @@ int Tim_ManBoxNum( Tim_Man_t * p )
 {
     return p->vBoxes ? Vec_PtrSize(p->vBoxes) : 0;
 }
+int Tim_ManBlackBoxNum( Tim_Man_t * p )
+{
+    Tim_Box_t * pBox;
+    int i, Counter = 0;
+    if ( Tim_ManBoxNum(p) )
+        Tim_ManForEachBox( p, pBox, i )
+            Counter += pBox->fBlack;
+    return Counter;
+}
 int Tim_ManDelayTableNum( Tim_Man_t * p )
 {
     return p->vDelayTables ? Vec_PtrSize(p->vDelayTables) : 0;