From dcc89071613ac466e59ec4d098b4d219f46d717b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 5 Mar 2013 16:53:18 -0800 Subject: Improvements to the hierarchy/timing manager. --- src/aig/gia/giaTim.c | 26 +++++----- src/base/main/mainInit.c | 2 +- src/map/if/if.h | 7 ++- src/map/if/ifCom.c | 12 +++-- src/map/if/ifLibBox.c | 127 ++++++++++++++++++++++++++++++++++++++++++++--- src/misc/tim/tim.h | 1 + src/misc/tim/timMan.c | 9 ++++ 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; -- cgit v1.2.3