diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-21 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-21 08:01:00 -0800 |
commit | d4fecf91efcd090caa9a5cbfb05059361e84c4ec (patch) | |
tree | 87dfc18934e7460a3be8c7cea0a587756e66aeb2 /src/aig | |
parent | 61850d5942fcff634b16696bf3ca7ee0fc465d1c (diff) | |
download | abc-d4fecf91efcd090caa9a5cbfb05059361e84c4ec.tar.gz abc-d4fecf91efcd090caa9a5cbfb05059361e84c4ec.tar.bz2 abc-d4fecf91efcd090caa9a5cbfb05059361e84c4ec.zip |
Version abc80121
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/fra/fraSec.c | 2 | ||||
-rw-r--r-- | src/aig/ioa/ioa.h | 4 | ||||
-rw-r--r-- | src/aig/ioa/ioaReadAig.c | 162 | ||||
-rw-r--r-- | src/aig/ioa/ioaWriteAig.c | 192 | ||||
-rw-r--r-- | src/aig/tim/tim.c | 135 |
5 files changed, 331 insertions, 164 deletions
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 4ccb48e3..c6bdc20e 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -276,7 +276,7 @@ PRT( "Time", clock() - clkTotal ); printf( "Networks are UNDECIDED. " ); PRT( "Time", clock() - clkTotal ); sprintf( pFileName, "sm%03d.aig", Counter++ ); - Ioa_WriteAiger( pNew, pFileName, 0 ); + Ioa_WriteAiger( pNew, pFileName, 0, 0 ); printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); } Aig_ManStop( pNew ); diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h index 3458d12e..e697a729 100644 --- a/src/aig/ioa/ioa.h +++ b/src/aig/ioa/ioa.h @@ -36,7 +36,7 @@ extern "C" { #include <time.h> #include "vec.h" -#include "bar.h" +//#include "bar.h" #include "aig.h" //////////////////////////////////////////////////////////////////////// @@ -62,7 +62,7 @@ extern "C" { /*=== ioaReadAig.c ========================================================*/ extern Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ); /*=== ioaWriteAig.c =======================================================*/ -extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ); +extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); /*=== ioaUtil.c =======================================================*/ extern int Ioa_FileSize( char * pFileName ); extern char * Ioa_FileNameGeneric( char * FileName ); diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c index 937e446f..498cdd30 100644 --- a/src/aig/ioa/ioaReadAig.c +++ b/src/aig/ioa/ioaReadAig.c @@ -25,14 +25,69 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -unsigned Ioa_ReadAigerDecode( char ** ppPos ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Extracts one unsigned AIG edge from the input buffer.] + + Description [This procedure is a slightly modified version of Armin Biere's + procedure "unsigned decode (FILE * file)". ] + + SideEffects [Updates the current reading position.] + + SeeAlso [] + +***********************************************************************/ +unsigned Ioa_ReadAigerDecode( char ** ppPos ) +{ + unsigned x = 0, i = 0; + unsigned char ch; + +// while ((ch = getnoneofch (file)) & 0x80) + while ((ch = *(*ppPos)++) & 0x80) + x |= (ch & 0x7f) << (7 * i++); + + return x | (ch << (7 * i)); +} + +/**Function************************************************************* + + Synopsis [Decodes the encoded array of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries ) +{ + Vec_Int_t * vLits; + int Lit, LitPrev, Diff, i; + vLits = Vec_IntAlloc( nEntries ); + LitPrev = Ioa_ReadAigerDecode( ppPos ); + Vec_IntPush( vLits, LitPrev ); + for ( i = 1; i < nEntries; i++ ) + { +// Diff = Lit - LitPrev; +// Diff = (Lit < LitPrev)? -Diff : Diff; +// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev); + Diff = Ioa_ReadAigerDecode( ppPos ); + Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1; + Lit = Diff + LitPrev; + Vec_IntPush( vLits, Lit ); + LitPrev = Lit; + } + return vLits; +} + + +/**Function************************************************************* + Synopsis [Reads the AIG in the binary AIGER format.] Description [] @@ -44,8 +99,9 @@ unsigned Ioa_ReadAigerDecode( char ** ppPos ); ***********************************************************************/ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) { - Bar_Progress_t * pProgress; +// Bar_Progress_t * pProgress; FILE * pFile; + Vec_Int_t * vLits = NULL; Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms; Aig_Obj_t * pObj, * pNode0, * pNode1; Aig_Man_t * pManNew; @@ -61,7 +117,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) fclose( pFile ); // check if the input file format is correct - if ( strncmp(pContents, "aig", 3) != 0 ) + if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') ) { fprintf( stdout, "Wrong input file format.\n" ); return NULL; @@ -127,21 +183,27 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) // Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL ); // printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id ); } -*/ - +*/ + // remember the beginning of latch/PO literals pDrivers = pCur; - - // scroll to the beginning of the binary data - for ( i = 0; i < nLatches + nOutputs; ) - if ( *pCur++ == '\n' ) - i++; + if ( pContents[3] == ' ' ) // standard AIGER + { + // scroll to the beginning of the binary data + for ( i = 0; i < nLatches + nOutputs; ) + if ( *pCur++ == '\n' ) + i++; + } + else // modified AIGER + { + vLits = Ioa_WriteDecodeLiterals( &pCur, nLatches + nOutputs ); + } // create the AND gates - pProgress = Bar_ProgressStart( stdout, nAnds ); +// pProgress = Bar_ProgressStart( stdout, nAnds ); for ( i = 0; i < nAnds; i++ ) { - Bar_ProgressUpdate( pProgress, i, NULL ); +// Bar_ProgressUpdate( pProgress, i, NULL ); uLit = ((i + 1 + nInputs + nLatches) << 1); uLit1 = uLit - Ioa_ReadAigerDecode( &pCur ); uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur ); @@ -151,33 +213,50 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches ); Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) ); } - Bar_ProgressStop( pProgress ); +// Bar_ProgressStop( pProgress ); // remember the place where symbols begin pSymbols = pCur; // read the latch driver literals vDrivers = Vec_PtrAlloc( nLatches + nOutputs ); - pCur = pDrivers; -// Aig_ManForEachLatchInput( pManNew, pObj, i ) - for ( i = 0; i < nLatches; i++ ) + if ( pContents[3] == ' ' ) // standard AIGER { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); -// Aig_ObjAddFanin( pObj, pNode0 ); - Vec_PtrPush( vDrivers, pNode0 ); + pCur = pDrivers; + for ( i = 0; i < nLatches; i++ ) + { + uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); + Vec_PtrPush( vDrivers, pNode0 ); + } + // read the PO driver literals + for ( i = 0; i < nOutputs; i++ ) + { + uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); + Vec_PtrPush( vDrivers, pNode0 ); + } + } - // read the PO driver literals -// Aig_ManForEachPo( pManNew, pObj, i ) - for ( i = 0; i < nOutputs; i++ ) + else { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); -// Aig_ObjAddFanin( pObj, pNode0 ); - Vec_PtrPush( vDrivers, pNode0 ); + // read the latch driver literals + for ( i = 0; i < nLatches; i++ ) + { + uLit0 = Vec_IntEntry( vLits, i ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); + Vec_PtrPush( vDrivers, pNode0 ); + } + // read the PO driver literals + for ( i = 0; i < nOutputs; i++ ) + { + uLit0 = Vec_IntEntry( vLits, i+nLatches ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); + Vec_PtrPush( vDrivers, pNode0 ); + } + Vec_IntFree( vLits ); } - // create the POs for ( i = 0; i < nOutputs; i++ ) Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) ); @@ -280,31 +359,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) } -/**Function************************************************************* - - Synopsis [Extracts one unsigned AIG edge from the input buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "unsigned decode (FILE * file)". ] - - SideEffects [Updates the current reading position.] - - SeeAlso [] - -***********************************************************************/ -unsigned Ioa_ReadAigerDecode( char ** ppPos ) -{ - unsigned x = 0, i = 0; - unsigned char ch; - -// while ((ch = getnoneofch (file)) & 0x80) - while ((ch = *(*ppPos)++) & 0x80) - x |= (ch & 0x7f) << (7 * i++); - - return x | (ch << (7 * i)); -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c index a6c23fd4..166dca4b 100644 --- a/src/aig/ioa/ioaWriteAig.c +++ b/src/aig/ioa/ioaWriteAig.c @@ -125,11 +125,9 @@ Binary Format Definition */ -static unsigned Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; } -static unsigned Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return (unsigned)pObj->pData; } -static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->pData = (void *)Num; } - -int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); +static int Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; } +static int Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return pObj->iData; } +static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->iData = Num; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -137,6 +135,111 @@ int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); /**Function************************************************************* + Synopsis [Adds one unsigned AIG edge to the output buffer.] + + Description [This procedure is a slightly modified version of Armin Biere's + procedure "void encode (FILE * file, unsigned x)" ] + + SideEffects [Returns the current writing position.] + + SeeAlso [] + +***********************************************************************/ +int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ) +{ + unsigned char ch; + while (x & ~0x7f) + { + ch = (x & 0x7f) | 0x80; +// putc (ch, file); + pBuffer[Pos++] = ch; + x >>= 7; + } + ch = x; +// putc (ch, file); + pBuffer[Pos++] = ch; + return Pos; +} + +/**Function************************************************************* + + Synopsis [Create the array of literals to be written.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ioa_WriteAigerLiterals( Aig_Man_t * pMan ) +{ + Vec_Int_t * vLits; + Aig_Obj_t * pObj, * pDriver; + int i; + vLits = Vec_IntAlloc( Aig_ManPoNum(pMan) ); + Aig_ManForEachLiSeq( pMan, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + } + Aig_ManForEachPoSeq( pMan, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + } + return vLits; +} + +/**Function************************************************************* + + Synopsis [Creates the binary encoded array of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits ) +{ + Vec_Str_t * vBinary; + int Pos = 0, Lit, LitPrev, Diff, i; + vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) ); + LitPrev = Vec_IntEntry( vLits, 0 ); + Pos = Ioa_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev ); + Vec_IntForEachEntryStart( vLits, Lit, i, 1 ) + { + Diff = Lit - LitPrev; + Diff = (Lit < LitPrev)? -Diff : Diff; + Diff = (Diff << 1) | (int)(Lit < LitPrev); + Pos = Ioa_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff ); + LitPrev = Lit; + if ( Pos + 10 > vBinary->nCap ) + Vec_StrGrow( vBinary, vBinary->nCap+1 ); + } + vBinary->nSize = Pos; +/* + // verify + { + extern Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries ); + char * pPos = Vec_StrArray( vBinary ); + Vec_Int_t * vTemp = Ioa_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) ); + for ( i = 0; i < Vec_IntSize(vLits); i++ ) + { + int Entry1 = Vec_IntEntry(vLits,i); + int Entry2 = Vec_IntEntry(vTemp,i); + assert( Entry1 == Entry2 ); + } + Vec_IntFree( vTemp ); + } +*/ + return vBinary; +} + +/**Function************************************************************* + Synopsis [Writes the AIG in the binary AIGER format.] Description [] @@ -146,9 +249,9 @@ int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); SeeAlso [] ***********************************************************************/ -void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) +void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ) { - Bar_Progress_t * pProgress; +// Bar_Progress_t * pProgress; FILE * pFile; Aig_Obj_t * pObj, * pDriver; int i, nNodes, Pos, nBufferSize; @@ -180,7 +283,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) Ioa_ObjSetAigerNum( pObj, nNodes++ ); // write the header "M I L O A" where M = I + L + A - fprintf( pFile, "aig %u %u %u %u %u\n", + fprintf( pFile, "aig%s %u %u %u %u %u\n", + fCompact? "2" : "", Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan), Aig_ManRegNum(pMan), @@ -191,34 +295,45 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) // because, in the AIGER format, literal 0/1 is represented as number 0/1 // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0 - // write latch drivers - Aig_ManForEachLiSeq( pMan, pObj, i ) + if ( !fCompact ) { - pDriver = Aig_ObjFanin0(pObj); - fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); - } + // write latch drivers + Aig_ManForEachLiSeq( pMan, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + } - // write PO drivers - Aig_ManForEachPoSeq( pMan, pObj, i ) + // write PO drivers + Aig_ManForEachPoSeq( pMan, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + } + } + else { - pDriver = Aig_ObjFanin0(pObj); - fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan ); + Vec_Str_t * vBinary = Ioa_WriteEncodeLiterals( vLits ); + fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile ); + Vec_StrFree( vBinary ); + Vec_IntFree( vLits ); } // write the nodes into the buffer Pos = 0; nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge - pBuffer = ALLOC( char, nBufferSize ); - pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) ); + pBuffer = ALLOC( unsigned char, nBufferSize ); +// pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) ); Aig_ManForEachNode( pMan, pObj, i ) { - Bar_ProgressUpdate( pProgress, i, NULL ); +// Bar_ProgressUpdate( pProgress, i, NULL ); uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 ); uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); assert( uLit0 < uLit1 ); - Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); - Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); + Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) ); + Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) ); if ( Pos > nBufferSize - 10 ) { printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); @@ -227,7 +342,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) } } assert( Pos < nBufferSize ); - Bar_ProgressStop( pProgress ); +// Bar_ProgressStop( pProgress ); // write the buffer fwrite( pBuffer, 1, Pos, pFile ); @@ -251,40 +366,11 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) fprintf( pFile, "c\n" ); if ( pMan->pName ) fprintf( pFile, ".model %s\n", pMan->pName ); - fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() ); + fprintf( pFile, "This file was produced by the AIG package on %s\n", Ioa_TimeStamp() ); fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); fclose( pFile ); } -/**Function************************************************************* - - Synopsis [Adds one unsigned AIG edge to the output buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "void encode (FILE * file, unsigned x)" ] - - SideEffects [Returns the current writing position.] - - SeeAlso [] - -***********************************************************************/ -int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ) -{ - unsigned char ch; - while (x & ~0x7f) - { - ch = (x & 0x7f) | 0x80; -// putc (ch, file); - pBuffer[Pos++] = ch; - x >>= 7; - } - ch = x; -// putc (ch, file); - pBuffer[Pos++] = ch; - return Pos; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c index 364f7d20..1bd21089 100644 --- a/src/aig/tim/tim.c +++ b/src/aig/tim/tim.c @@ -45,7 +45,7 @@ struct Tim_Man_t_ { Vec_Ptr_t * vBoxes; // the timing boxes Vec_Ptr_t * vDelayTables; // pointers to the delay tables - Mem_Flex_t * pMemObj; // memory manager for boxes + Mem_Flex_t * pMemObj; // memory manager for boxes int nTravIds; // traversal ID of the manager int nPis; // the number of PIs int nPos; // the number of POs @@ -74,13 +74,27 @@ struct Tim_Obj_t_ float timeReq; // required time of the object }; +static inline Tim_Obj_t * Tim_ManPi( Tim_Man_t * p, int i ) { assert( i < p->nPis ); return p->pPis + i; } +static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i ) { assert( i < p->nPos ); return p->pPos + i; } + +static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i ) { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); } +static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i ) { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); } + +static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i ) { return p->pPos + pBox->Inouts[i]; } +static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i ) { return p->pPis + pBox->Inouts[pBox->nInputs+i]; } + +#define Tim_ManBoxForEachInput( p, pBox, pObj, i ) \ + for ( i = 0; (i < (pBox)->nInputs) && ((pObj) = Tim_ManBoxInput(p, pBox, i)); i++ ) +#define Tim_ManBoxForEachOutput( p, pBox, pObj, i ) \ + for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Starts the network manager.] + Synopsis [Starts the timing manager.] Description [] @@ -113,7 +127,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos ) /**Function************************************************************* - Synopsis [Stops the network manager.] + Synopsis [Stops the timing manager.] Description [] @@ -141,7 +155,7 @@ void Tim_ManStop( Tim_Man_t * p ) /**Function************************************************************* - Synopsis [Increments the trav ID of the manager.] + Synopsis [Sets the vector of timing tables associated with the manager.] Description [] @@ -252,7 +266,7 @@ void Tim_ManIncrementTravId( Tim_Man_t * p ) /**Function************************************************************* - Synopsis [Creates the new timing box.] + Synopsis [Initializes arrival time of the PI.] Description [] @@ -269,7 +283,7 @@ void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay ) /**Function************************************************************* - Synopsis [Creates the new timing box.] + Synopsis [Initializes required time of the PO.] Description [] @@ -286,7 +300,7 @@ void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay ) /**Function************************************************************* - Synopsis [Creates the new timing box.] + Synopsis [Updates arrival time of the PO.] Description [] @@ -305,7 +319,7 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay ) /**Function************************************************************* - Synopsis [Returns PI arrival time.] + Synopsis [Updates required time of the PI.] Description [] @@ -314,52 +328,18 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay ) SeeAlso [] ***********************************************************************/ -float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi ) +void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay ) { - Tim_Box_t * pBox; - Tim_Obj_t * pObj; - float * pDelays; - float DelayMax; - int i, k; assert( iPi < p->nPis ); - if ( p->pPis[iPi].iObj2Box < 0 ) - return p->pPis[iPi].timeArr; - pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box ); - // check if box timing is updated - if ( pBox->TravId == p->nTravIds ) - { - assert( pBox->TravId == p->nTravIds ); - return p->pPis[iPi].timeArr; - } - pBox->TravId = p->nTravIds; - // update box timing - // get the arrival times of the inputs of the box (POs) - for ( i = 0; i < pBox->nInputs; i++ ) - { - pObj = p->pPos + pBox->Inouts[i]; - if ( pObj->TravId != p->nTravIds ) - printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" ); - } - // compute the required times for each output of the box (PIs) - for ( i = 0; i < pBox->nOutputs; i++ ) - { - pDelays = pBox->pDelayTable + i * pBox->nInputs; - DelayMax = -AIG_INFINITY; - for ( k = 0; k < pBox->nInputs; k++ ) - { - pObj = p->pPos + pBox->Inouts[k]; - DelayMax = AIG_MAX( DelayMax, pObj->timeArr + pDelays[k] ); - } - pObj = p->pPis + pBox->Inouts[pBox->nInputs+i]; - pObj->timeArr = DelayMax; - pObj->TravId = p->nTravIds; - } - return p->pPis[iPi].timeArr; + assert( p->pPis[iPi].TravId != p->nTravIds ); + p->pPis[iPi].timeReq = Delay; + p->pPis[iPi].TravId = p->nTravIds; } + /**Function************************************************************* - Synopsis [Returns PO required time.] + Synopsis [Returns PI arrival time.] Description [] @@ -368,12 +348,33 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi ) SeeAlso [] ***********************************************************************/ -void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay ) +float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi ) { - assert( iPi < p->nPis ); - assert( p->pPis[iPi].TravId != p->nTravIds ); - p->pPis[iPi].timeReq = Delay; - p->pPis[iPi].TravId = p->nTravIds; + Tim_Box_t * pBox; + Tim_Obj_t * pObj, * pObjRes; + float * pDelays, DelayBest; + int i, k; + // consider the main PI or the already processed PI + pBox = Tim_ManPiBox( p, iPi ); + if ( pBox == NULL || pBox->TravId == p->nTravIds ) + return Tim_ManPi(p, iPi)->timeArr; + // update box timing + pBox->TravId = p->nTravIds; + // get the arrival times of the inputs of the box (POs) + Tim_ManBoxForEachInput( p, pBox, pObj, i ) + if ( pObj->TravId != p->nTravIds ) + printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" ); + // compute the required times for each output of the box (PIs) + Tim_ManBoxForEachOutput( p, pBox, pObjRes, i ) + { + pDelays = pBox->pDelayTable + i * pBox->nInputs; + DelayBest = -AIG_INFINITY; + Tim_ManBoxForEachInput( p, pBox, pObj, k ) + DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] ); + pObjRes->timeArr = DelayBest; + pObjRes->TravId = p->nTravIds; + } + return Tim_ManPi(p, iPi)->timeArr; } /**Function************************************************************* @@ -389,7 +390,33 @@ void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay ) ***********************************************************************/ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo ) { - return 0.0; + Tim_Box_t * pBox; + Tim_Obj_t * pObj, * pObjRes; + float * pDelays, DelayBest; + int i, k; + // consider the main PO or the already processed PO + pBox = Tim_ManPoBox( p, iPo ); + if ( pBox == NULL || pBox->TravId == p->nTravIds ) + return Tim_ManPo(p, iPo)->timeReq; + // update box timing + pBox->TravId = p->nTravIds; + // get the arrival times of the inputs of the box (POs) + Tim_ManBoxForEachOutput( p, pBox, pObj, i ) + if ( pObj->TravId != p->nTravIds ) + printf( "Tim_ManGetPoRequired(): PI required times of the box are not up to date!\n" ); + // compute the required times for each output of the box (PIs) + Tim_ManBoxForEachInput( p, pBox, pObjRes, i ) + { + DelayBest = AIG_INFINITY; + Tim_ManBoxForEachOutput( p, pBox, pObj, k ) + { + pDelays = pBox->pDelayTable + k * pBox->nInputs; + DelayBest = AIG_MIN( DelayBest, pObj->timeReq + pDelays[i] ); + } + pObjRes->timeReq = DelayBest; + pObjRes->TravId = p->nTravIds; + } + return Tim_ManPo(p, iPo)->timeReq; } |