summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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
-rw-r--r--src/base/abci/abc.c9
-rw-r--r--src/base/io/io.c25
-rw-r--r--src/base/io/io.h2
-rw-r--r--src/base/io/ioReadAiger.c146
-rw-r--r--src/base/io/ioUtil.c2
-rw-r--r--src/base/io/ioWriteAiger.c174
-rw-r--r--src/map/if/if.h11
-rw-r--r--src/map/if/ifCut.c189
-rw-r--r--src/map/if/ifMan.c4
-rw-r--r--src/map/if/ifReduce.c5
-rw-r--r--src/map/if/ifUtil.c2
-rw-r--r--src/map/pcm/module.make0
-rw-r--r--src/map/ply/module.make0
18 files changed, 687 insertions, 377 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;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0a27ee15..396cf598 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6384,7 +6384,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern void Abc_NtkDarTestBlif( char * pFileName );
@@ -6543,6 +6543,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for logic circuits.\n" );
return 0;
}
+*/
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
@@ -6555,7 +6556,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
+
// Abc_NtkDarHaigRecord( pNtk );
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
@@ -10363,8 +10364,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// disable cut-expansion if edge-based heuristics are selected
- if ( pPars->fEdge )
- pPars->fExpRed = 0;
+// if ( pPars->fEdge )
+// pPars->fExpRed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
{
diff --git a/src/base/io/io.c b/src/base/io/io.c
index ed314fcd..fe88a285 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1174,17 +1174,22 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int fWriteSymbols;
+ int fCompact;
int c;
- fWriteSymbols = 1;
+ fCompact = 1;
+ fWriteSymbols = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF )
{
switch ( c )
{
case 's':
fWriteSymbols ^= 1;
break;
+ case 'c':
+ fCompact ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -1196,23 +1201,19 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
- if ( fWriteSymbols )
- Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER );
- else
+ if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
- if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
- {
- fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
- return 1;
- }
- Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 );
+ fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
+ return 1;
}
+ Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact );
return 0;
usage:
- fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\n" );
+ fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" );
fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
+ fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" );
return 1;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 45762b77..126de332 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -87,7 +87,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck );
/*=== abcReadVerilog.c ========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
/*=== abcWriteAiger.c =========================================================*/
-extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols );
+extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact );
/*=== abcWriteBaf.c ===========================================================*/
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 273b2d5a..4820bced 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -25,14 +25,68 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-unsigned Io_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 Io_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 * Io_WriteDecodeLiterals( char ** ppPos, int nEntries )
+{
+ Vec_Int_t * vLits;
+ int Lit, LitPrev, Diff, i;
+ vLits = Vec_IntAlloc( nEntries );
+ LitPrev = Io_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 = Io_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 []
@@ -47,6 +101,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
ProgressBar * pProgress;
FILE * pFile;
Vec_Ptr_t * vNodes, * vTerms;
+ Vec_Int_t * vLits = NULL;
Abc_Obj_t * pObj, * pNode0, * pNode1;
Abc_Ntk_t * pNtkNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
@@ -61,7 +116,7 @@ Abc_Ntk_t * Io_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;
@@ -125,13 +180,20 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// printf( "Creating latch %s with input %d and output %d.\n", Abc_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
+ {
+ // 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++;
+ }
+ else // modified AIGER
+ {
+ vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
+ }
// create the AND gates
pProgress = Extra_ProgressBarStart( stdout, nAnds );
@@ -154,21 +216,39 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// read the latch driver literals
pCur = pDrivers;
- Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
+ if ( pContents[3] == ' ' ) // standard AIGER
{
- uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
- Abc_ObjAddFanin( pObj, pNode0 );
-
-// printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
-
+ Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
+ {
+ uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+ Abc_ObjAddFanin( pObj, pNode0 );
+ }
+ // read the PO driver literals
+ Abc_NtkForEachPo( pNtkNew, pObj, i )
+ {
+ uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+ Abc_ObjAddFanin( pObj, pNode0 );
+ }
}
- // read the PO driver literals
- Abc_NtkForEachPo( pNtkNew, pObj, i )
+ else
{
- uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
- Abc_ObjAddFanin( pObj, pNode0 );
+ // read the latch driver literals
+ Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
+ {
+ uLit0 = Vec_IntEntry( vLits, i );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+ Abc_ObjAddFanin( pObj, pNode0 );
+ }
+ // read the PO driver literals
+ Abc_NtkForEachPo( pNtkNew, pObj, i )
+ {
+ uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+ Abc_ObjAddFanin( pObj, pNode0 );
+ }
+ Vec_IntFree( vLits );
}
// read the names if present
@@ -278,30 +358,6 @@ Abc_Ntk_t * Io_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 Io_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/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 94ec4316..4f9f2e9f 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
return;
}
if ( FileType == IO_FILE_AIGER )
- Io_WriteAiger( pNtk, pFileName, 1 );
+ Io_WriteAiger( pNtk, pFileName, 1, 0 );
else // if ( FileType == IO_FILE_BAF )
Io_WriteBaf( pNtk, pFileName );
return;
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index ff34b177..758e5335 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -129,14 +129,116 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (V
static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj ) { return (unsigned)pObj->pCopy; }
static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (void *)Num; }
-int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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 Io_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 * Io_WriteAigerLiterals( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vLits;
+ Abc_Obj_t * pObj, * pDriver;
+ int i;
+ vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
+ Abc_NtkForEachLatchInput( pNtk, pObj, i )
+ {
+ pDriver = Abc_ObjFanin0(pObj);
+ Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+ }
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ pDriver = Abc_ObjFanin0(pObj);
+ Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+ }
+ return vLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the binary encoded array of literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Str_t * Io_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 = Io_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 = Io_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 * Io_WriteDecodeLiterals( char ** ppPos, int nEntries );
+ char * pPos = Vec_StrArray( vBinary );
+ Vec_Int_t * vTemp = Io_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 );
+ }
+ }
+*/
+ return vBinary;
+}
+
+/**Function*************************************************************
+
Synopsis [Writes the AIG in the binary AIGER format.]
Description []
@@ -146,7 +248,7 @@ int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
SeeAlso []
***********************************************************************/
-void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
{
ProgressBar * pProgress;
FILE * pFile;
@@ -179,7 +281,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
Io_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" : "",
Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
Abc_NtkPiNum(pNtk),
Abc_NtkLatchNum(pNtk),
@@ -190,24 +293,34 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, 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
- Abc_NtkForEachLatchInput( pNtk, pObj, i )
+ if ( !fCompact )
{
- pDriver = Abc_ObjFanin0(pObj);
- fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+ // write latch drivers
+ Abc_NtkForEachLatchInput( pNtk, pObj, i )
+ {
+ pDriver = Abc_ObjFanin0(pObj);
+ fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+ }
+ // write PO drivers
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ pDriver = Abc_ObjFanin0(pObj);
+ fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+ }
}
-
- // write PO drivers
- Abc_NtkForEachPo( pNtk, pObj, i )
+ else
{
- pDriver = Abc_ObjFanin0(pObj);
- fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+ Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
+ Vec_Str_t * vBinary = Io_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 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
- pBuffer = ALLOC( char, nBufferSize );
+ pBuffer = ALLOC( unsigned char, nBufferSize );
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_AigForEachAnd( pNtk, pObj, i )
{
@@ -216,8 +329,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
assert( uLit0 < uLit1 );
- Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
- Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
+ Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
+ Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
if ( Pos > nBufferSize - 10 )
{
printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
@@ -255,35 +368,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
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 Io_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/map/if/if.h b/src/map/if/if.h
index 17040742..07816790 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -326,8 +326,13 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r
extern int If_ManPerformMapping( If_Man_t * p );
extern int If_ManPerformMappingComb( If_Man_t * p );
/*=== ifCut.c ============================================================*/
+extern int If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
+extern void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
+extern int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
extern void If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
extern void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
+extern void If_CutLift( If_Cut_t * pCut );
+extern void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
extern float If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
@@ -339,12 +344,6 @@ extern float If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut );
-extern int If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
-extern void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
-extern int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
-extern void If_CutLift( If_Cut_t * pCut );
-extern void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
-extern void If_ManSortCuts( If_Man_t * p, int Mode );
/*=== ifMan.c =============================================================*/
extern If_Man_t * If_ManStart( If_Par_t * pPars );
extern void If_ManRestart( If_Man_t * p );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 915cedf9..cc842c19 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -311,21 +311,21 @@ int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+int If_CutCompareDelay( If_Man_t * p, If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
{
If_Cut_t * pC0 = *ppC0;
If_Cut_t * pC1 = *ppC1;
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
return 0;
}
@@ -341,17 +341,17 @@ int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
SeeAlso []
***********************************************************************/
-int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+int If_CutCompareDelayOld( If_Man_t * p, If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
{
If_Cut_t * pC0 = *ppC0;
If_Cut_t * pC1 = *ppC1;
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
@@ -371,13 +371,13 @@ int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
SeeAlso []
***********************************************************************/
-int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+int If_CutCompareArea( If_Man_t * p, If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
{
If_Cut_t * pC0 = *ppC0;
If_Cut_t * pC1 = *ppC1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
if ( pC0->AveRefs > pC1->AveRefs )
return -1;
@@ -387,9 +387,9 @@ int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
return 0;
}
@@ -433,13 +433,13 @@ static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC
{
if ( p->SortMode == 1 ) // area
{
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
- if ( pC0->Edge < pC1->Edge - 0.0001 )
+ if ( pC0->Edge < pC1->Edge - p->fEpsilon )
return -1;
- if ( pC0->Edge > pC1->Edge + 0.0001 )
+ if ( pC0->Edge > pC1->Edge + p->fEpsilon )
return 1;
if ( pC0->AveRefs > pC1->AveRefs )
return -1;
@@ -449,44 +449,44 @@ static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
return 0;
}
if ( p->SortMode == 0 ) // delay
{
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
- if ( pC0->Edge < pC1->Edge - 0.0001 )
+ if ( pC0->Edge < pC1->Edge - p->fEpsilon )
return -1;
- if ( pC0->Edge > pC1->Edge + 0.0001 )
+ if ( pC0->Edge > pC1->Edge + p->fEpsilon )
return 1;
return 0;
}
assert( p->SortMode == 2 ); // delay old
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
- if ( pC0->Edge < pC1->Edge - 0.0001 )
+ if ( pC0->Edge < pC1->Edge - p->fEpsilon )
return -1;
- if ( pC0->Edge > pC1->Edge + 0.0001 )
+ if ( pC0->Edge > pC1->Edge + p->fEpsilon )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
@@ -510,9 +510,9 @@ static inline int If_ManSortCompare_old( If_Man_t * p, If_Cut_t * pC0, If_Cut_t
{
if ( p->SortMode == 1 ) // area
{
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
if ( pC0->AveRefs > pC1->AveRefs )
return -1;
@@ -522,36 +522,36 @@ static inline int If_ManSortCompare_old( If_Man_t * p, If_Cut_t * pC0, If_Cut_t
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
return 0;
}
if ( p->SortMode == 0 ) // delay
{
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
return 0;
}
assert( p->SortMode == 2 ); // delay old
- if ( pC0->Delay < pC1->Delay - 0.0001 )
+ if ( pC0->Delay < pC1->Delay - p->fEpsilon )
return -1;
- if ( pC0->Delay > pC1->Delay + 0.0001 )
+ if ( pC0->Delay > pC1->Delay + p->fEpsilon )
return 1;
- if ( pC0->Area < pC1->Area - 0.0001 )
+ if ( pC0->Area < pC1->Area - p->fEpsilon )
return -1;
- if ( pC0->Area > pC1->Area + 0.0001 )
+ if ( pC0->Area > pC1->Area + p->fEpsilon )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
@@ -646,6 +646,56 @@ void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut )
/**Function*************************************************************
+ Synopsis [Moves the cut over the latch.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void If_CutLift( If_Cut_t * pCut )
+{
+ unsigned i;
+ for ( i = 0; i < pCut->nLeaves; i++ )
+ {
+ assert( (pCut->pLeaves[i] & 255) < 255 );
+ pCut->pLeaves[i]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area of the first level.]
+
+ Description [The cut need to be derefed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
+{
+ int * pLeaves;
+ char * pPerm;
+ unsigned * pTruth;
+ // save old arrays
+ pLeaves = pCutDest->pLeaves;
+ pPerm = pCutDest->pPerm;
+ pTruth = pCutDest->pTruth;
+ // copy the cut info
+ memcpy( pCutDest, pCutSrc, p->nCutBytes );
+ // restore the arrays
+ pCutDest->pLeaves = pLeaves;
+ pCutDest->pPerm = pPerm;
+ pCutDest->pTruth = pTruth;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Computes area flow.]
Description []
@@ -931,55 +981,6 @@ float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
}
-/**Function*************************************************************
-
- Synopsis [Moves the cut over the latch.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void If_CutLift( If_Cut_t * pCut )
-{
- unsigned i;
- for ( i = 0; i < pCut->nLeaves; i++ )
- {
- assert( (pCut->pLeaves[i] & 255) < 255 );
- pCut->pLeaves[i]++;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes area of the first level.]
-
- Description [The cut need to be derefed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
-{
- int * pLeaves;
- char * pPerm;
- unsigned * pTruth;
- // save old arrays
- pLeaves = pCutDest->pLeaves;
- pPerm = pCutDest->pPerm;
- pTruth = pCutDest->pTruth;
- // copy the cut info
- memcpy( pCutDest, pCutSrc, p->nCutBytes );
- // restore the arrays
- pCutDest->pLeaves = pLeaves;
- pCutDest->pPerm = pPerm;
- pCutDest->pTruth = pTruth;
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 50ce63e9..977d69c9 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -68,8 +68,8 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
// p->pMemSet = Mem_FixedStart( p->nSetBytes );
// report expected memory usage
if ( p->pPars->fVerbose )
- printf( "Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n",
- 4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
+ printf( "K = %d. Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n",
+ p->pPars->nLutSize, 4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
// room for temporary truth tables
p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index ab7de609..0912a965 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -150,6 +150,7 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
int CostBef, CostAft, i;
float DelayOld, AreaBef, AreaAft;
pCut = If_ObjCutBest(pObj);
+ pCut->Delay = If_CutDelay( p, pCut );
assert( pCut->Delay <= pObj->Required + p->fEpsilon );
if ( pObj->nRefs == 0 )
return;
@@ -449,8 +450,8 @@ int If_ManImproveNodeFaninCompact_int( If_Man_t * p, If_Obj_t * pObj, int nLimit
return 1;
if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact1(p, pObj, nLimit, vFront, vVisited) )
return 1;
- if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
- return 1;
+// if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
+// return 1;
assert( Vec_PtrSize(vFront) <= nLimit );
return 0;
}
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index f4fcf94a..3bb39e2f 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -212,7 +212,7 @@ void If_ManComputeRequired( If_Man_t * p )
Vec_PtrForEachEntry( p->vMapped, pObj, i )
If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
}
-
+
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 09:29:05 +0000