summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/fra/fraSec.c2
-rw-r--r--src/aig/ioa/ioa.h4
-rw-r--r--src/aig/ioa/ioaReadAig.c162
-rw-r--r--src/aig/ioa/ioaWriteAig.c192
-rw-r--r--src/aig/tim/tim.c135
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-01 12:06:58 +0000