summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp8
-rw-r--r--abc.rc2
-rw-r--r--src/aig/ivy/ivyMem.c7
-rw-r--r--src/base/abc/abcCheck.c11
-rw-r--r--src/base/abc/abcNames.c2
-rw-r--r--src/base/abci/abc.c8
-rw-r--r--src/base/abci/abcPrint.c2
-rw-r--r--src/base/io/io.c168
-rw-r--r--src/base/io/io.h4
-rw-r--r--src/base/io/ioRead.c2
-rw-r--r--src/base/io/ioReadAiger.c273
-rw-r--r--src/base/io/ioReadBaf.c4
-rw-r--r--src/base/io/ioWriteAiger.c281
-rw-r--r--src/base/io/module.make2
-rw-r--r--src/map/fpga/fpgaCutUtils.c4
-rw-r--r--src/map/fpga/fpgaInt.h4
-rw-r--r--src/map/fpga/fpgaMatch.c22
-rw-r--r--src/map/if/if.h6
-rw-r--r--src/map/if/ifCut.c8
-rw-r--r--src/map/if/ifMap.c61
-rw-r--r--src/map/if/ifSeq.c8
-rw-r--r--src/map/if/ifTime.c6
-rw-r--r--src/map/if/ifUtil.c6
-rw-r--r--src/misc/vec/vecPtr.h5
-rw-r--r--src/opt/ret/retLvalue.c10
-rw-r--r--src/opt/rwr/rwrEva.c34
26 files changed, 862 insertions, 86 deletions
diff --git a/abc.dsp b/abc.dsp
index 5a4c1b0e..052fb4f8 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -410,6 +410,10 @@ SOURCE=.\src\base\io\ioRead.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\io\ioReadAiger.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\io\ioReadBaf.c
# End Source File
# Begin Source File
@@ -438,6 +442,10 @@ SOURCE=.\src\base\io\ioUtil.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\io\ioWriteAiger.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\io\ioWriteBaf.c
# End Source File
# Begin Source File
diff --git a/abc.rc b/abc.rc
index c73f3276..1677e8be 100644
--- a/abc.rc
+++ b/abc.rc
@@ -1,7 +1,7 @@
# global parameters
set check # checks intermediate networks
#set checkfio # prints warnings when fanins/fanouts are duplicated
-#set checkread # checks new networks after reading from file
+set checkread # checks new networks after reading from file
set backup # saves backup networks retrived by "undo" and "recall"
set savesteps 1 # sets the maximum number of backup networks to save
set progressbar # display the progress bar
diff --git a/src/aig/ivy/ivyMem.c b/src/aig/ivy/ivyMem.c
index 09c73c49..2a96857c 100644
--- a/src/aig/ivy/ivyMem.c
+++ b/src/aig/ivy/ivyMem.c
@@ -87,15 +87,16 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
{
char * pMemory;
int i, nBytes;
- assert( sizeof(Ivy_Obj_t) <= 64 );
+ int EntrySizeMax = 128;
+ assert( sizeof(Ivy_Obj_t) <= EntrySizeMax );
assert( p->pListFree == NULL );
// assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
// allocate new memory page
- nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
+ nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + EntrySizeMax;
pMemory = ALLOC( char, nBytes );
Vec_PtrPush( p->vChunks, pMemory );
// align memory at the 32-byte boundary
- pMemory = pMemory + 64 - (((int)pMemory) & 63);
+ pMemory = pMemory + EntrySizeMax - (((int)pMemory) & (EntrySizeMax-1));
// remember the manager in the first entry
Vec_PtrPush( p->vPages, pMemory );
// break the memory down into nodes
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 7ade6740..bd11afb9 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -422,6 +422,10 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
fprintf( stdout, "NetworkCheck: Object \"%s\" has incorrect ID.\n", Abc_ObjName(pObj) );
return 0;
}
+
+ if ( !Abc_FrameIsFlagEnabled("checkfio") )
+ return Value;
+
// go through the fanins of the object and make sure fanins have this object as a fanout
Abc_ObjForEachFanin( pObj, pFanin, i )
{
@@ -443,9 +447,6 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
}
}
- if ( !Abc_FrameIsFlagEnabled("checkfio") )
- return Value;
-
// make sure fanins are not duplicated
for ( i = 0; i < pObj->vFanins.nSize; i++ )
for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -706,10 +707,10 @@ bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
// for each PI of pNet1 find corresponding PI of pNet2 and reorder them
Abc_NtkForEachBox( pNtk1, pObj1, i )
{
- if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkBox(pNtk2,i)) ) != 0 )
+ if ( strcmp( Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) ) != 0 )
{
printf( "Box #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n",
- i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkBox(pNtk2,i)) );
+ i, Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) );
return 0;
}
}
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 274cf243..2029994c 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -320,7 +320,7 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
Abc_NtkForEachPo( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
Abc_NtkForEachBox( pNtk, pObj, i )
- pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+ pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(Abc_ObjFanout0(pObj));
// order objects alphabetically
qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *),
(int (*)(const void *, const void *)) Abc_NodeCompareNames );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0619b26a..278812ef 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7542,7 +7542,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fTruth = 0;
pPars->nLatches = pNtk? Abc_NtkLatchNum(pNtk) : 0;
pPars->fLiftLeaves = 0;
- pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
+ pPars->pLutLib = Abc_FrameReadLibLut();
pPars->pTimesArr = NULL;
pPars->pTimesArr = NULL;
pPars->pFuncCost = NULL;
@@ -7562,6 +7562,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
globalUtilOptind++;
if ( pPars->nLutSize < 0 )
goto usage;
+ // if the LUT size is specified, disable library
+ pPars->pLutLib = NULL;
break;
case 'C':
if ( globalUtilOptind >= argc )
@@ -7709,7 +7711,7 @@ usage:
sprintf( LutSize, "library" );
else
sprintf( LutSize, "%d", pPars->nLutSize );
- fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrstvh]\n" );
+ fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" );
fprintf( pErr, "\t performs FPGA technology mapping of the network\n" );
fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
fprintf( pErr, "\t-C num : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -7720,7 +7722,7 @@ usage:
fprintf( pErr, "\t-r : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
fprintf( pErr, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
fprintf( pErr, "\t-s : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
- fprintf( pErr, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
+// fprintf( pErr, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : prints the command usage\n");
return 1;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 27235d0a..6698e738 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -124,7 +124,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
/*
{
FILE * pTable;
- pTable = fopen( "a/seqmap__stats.txt", "a+" );
+ pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
fprintf( pTable, "%s ", pNtk->pName );
fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index b1ea03c1..f6d71d52 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -26,6 +26,7 @@
////////////////////////////////////////////////////////////////////////
static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -37,6 +38,7 @@ static int IoCommandReadVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -71,6 +73,7 @@ extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fC
void Io_Init( Abc_Frame_t * pAbc )
{
Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
@@ -82,6 +85,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
@@ -157,7 +161,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -177,7 +181,80 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network from file in Verilog/BLIF/BENCH format\n" );
+ fprintf( pAbc->Err, "\t read the network from file in BLIF/BENCH/PLA/BAF/AIGER format\n" );
+ fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+ fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
+ fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandReadAiger( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != globalUtilOptind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[globalUtilOptind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ pNtk = Io_ReadAiger( FileName, fCheck );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from the AIGER file has failed.\n" );
+ return 1;
+ }
+
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_aiger [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
@@ -229,7 +306,7 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -240,7 +317,7 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtk = Io_ReadBaf( FileName, fCheck );
if ( pNtk == NULL )
{
- fprintf( pAbc->Err, "Reading network from BAF file has failed.\n" );
+ fprintf( pAbc->Err, "Reading network from the BAF file has failed.\n" );
return 1;
}
@@ -302,7 +379,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -383,7 +460,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -463,7 +540,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -543,7 +620,7 @@ int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -626,7 +703,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -709,7 +786,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -799,7 +876,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -875,7 +952,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -992,6 +1069,65 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * FileName;
+ int c;
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ pNtk = pAbc->pNtkCur;
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( argc != globalUtilOptind + 1 )
+ {
+ goto usage;
+ }
+ FileName = argv[globalUtilOptind];
+
+ // check the network type
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pAbc->Out, "Writing AIGER is only possible for structurally hashed AIGs.\n" );
+ return 0;
+ }
+ Io_WriteAiger( pNtk, FileName );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_aiger [-lh] <file>\n" );
+ fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
+ 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;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
@@ -1026,7 +1162,7 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
// check the network type
if ( !Abc_NtkIsStrash(pNtk) )
{
- fprintf( pAbc->Out, "Currently can only write strashed combinational AIGs.\n" );
+ fprintf( pAbc->Out, "Writing BAF is only possible for structurally hashed AIGs.\n" );
return 0;
}
Io_WriteBaf( pNtk, FileName );
@@ -1036,7 +1172,7 @@ usage:
fprintf( pAbc->Err, "usage: write_baf [-lh] <file>\n" );
fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
- fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .baf)\n" );
return 1;
}
@@ -1102,7 +1238,7 @@ usage:
fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
- fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
return 1;
}
@@ -1176,7 +1312,7 @@ usage:
fprintf( pAbc->Err, "\t write the network in BENCH format\n" );
// fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
- fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" );
return 1;
}
diff --git a/src/base/io/io.h b/src/base/io/io.h
index e7971b8d..776a1b2d 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -51,6 +51,8 @@ extern "C" {
/*=== abcRead.c ==========================================================*/
extern Abc_Ntk_t * Io_Read( char * pFileName, int fCheck );
+/*=== abcReadAiger.c ==========================================================*/
+extern Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck );
/*=== abcReadBaf.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck );
/*=== abcReadBlif.c ==========================================================*/
@@ -75,6 +77,8 @@ extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bo
extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
+/*=== abcWriteAiger.c ==========================================================*/
+extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBaf.c ==========================================================*/
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 33f23796..36619a19 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -60,6 +60,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
pNtk = Io_ReadEqn( pFileName, fCheck );
else if ( Extra_FileNameCheckExtension( pFileName, "baf" ) )
return Io_ReadBaf( pFileName, fCheck );
+ else if ( Extra_FileNameCheckExtension( pFileName, "aig" ) )
+ return Io_ReadAiger( pFileName, fCheck );
else
{
fprintf( stderr, "Unknown file format\n" );
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
new file mode 100644
index 00000000..b581aa0f
--- /dev/null
+++ b/src/base/io/ioReadAiger.c
@@ -0,0 +1,273 @@
+/**CFile****************************************************************
+
+ FileName [ioReadAiger.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to read binary AIGER format developed by
+ Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - December 16, 2006.]
+
+ Revision [$Id: ioReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned Io_ReadAigerDecode( char ** ppPos );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Reads the AIG in the binary AIGER format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
+{
+ ProgressBar * pProgress;
+ FILE * pFile;
+ Vec_Ptr_t * vNodes, * vTerms;
+ Abc_Obj_t * pObj, * pNode0, * pNode1;
+ Abc_Ntk_t * pNtkNew;
+ int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
+ char * pContents, * pDrivers, * pSymbols, * pCur, * pName, * pType;
+ unsigned uLit0, uLit1, uLit;
+
+ // read the file into the buffer
+ nFileSize = Extra_FileSize( pFileName );
+ pFile = fopen( pFileName, "rb" );
+ pContents = ALLOC( char, nFileSize );
+ fread( pContents, nFileSize, 1, pFile );
+ fclose( pFile );
+
+ // check if the input file format is correct
+ if ( strncmp(pContents, "aig", 3) != 0 )
+ {
+ fprintf( stdout, "Wrong input file format." );
+ return NULL;
+ }
+
+ // allocate the empty AIG
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ pName = Extra_FileNameGeneric( pFileName );
+ pNtkNew->pName = Extra_UtilStrsav( pName );
+ pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
+ free( pName );
+
+
+ // read the file type
+ pCur = pContents; while ( *pCur++ != ' ' );
+ // read the number of objects
+ nTotal = atoi( pCur ); while ( *pCur++ != ' ' );
+ // read the number of inputs
+ nInputs = atoi( pCur ); while ( *pCur++ != ' ' );
+ // read the number of latches
+ nLatches = atoi( pCur ); while ( *pCur++ != ' ' );
+ // read the number of outputs
+ nOutputs = atoi( pCur ); while ( *pCur++ != ' ' );
+ // read the number of nodes
+ nAnds = atoi( pCur ); while ( *pCur++ != '\n' );
+ // check the parameters
+ if ( nTotal != nInputs + nLatches + nAnds )
+ {
+ fprintf( stdout, "The paramters are wrong." );
+ return NULL;
+ }
+
+ // prepare the array of nodes
+ vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
+ Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );
+
+ // create the PIs
+ for ( i = 0; i < nInputs; i++ )
+ {
+ pObj = Abc_NtkCreatePi(pNtkNew);
+ Vec_PtrPush( vNodes, pObj );
+ }
+ // create the POs
+ for ( i = 0; i < nOutputs; i++ )
+ {
+ pObj = Abc_NtkCreatePo(pNtkNew);
+ }
+ // create the latches
+ nDigits = Extra_Base10Log( nLatches );
+ for ( i = 0; i < nLatches; i++ )
+ {
+ pObj = Abc_NtkCreateLatch(pNtkNew);
+ Abc_LatchSetInit0( pObj );
+ pNode0 = Abc_NtkCreateBi(pNtkNew);
+ pNode1 = Abc_NtkCreateBo(pNtkNew);
+ Abc_ObjAddFanin( pObj, pNode0 );
+ Abc_ObjAddFanin( pNode1, pObj );
+ Vec_PtrPush( vNodes, pNode1 );
+ // assign names to latch and its input
+ Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
+ }
+
+ // 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++;
+
+ // create the AND gates
+ pProgress = Extra_ProgressBarStart( stdout, nAnds );
+ for ( i = 0; i < nAnds; i++ )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ uLit = ((i + 1 + nInputs + nLatches) << 1);
+ uLit1 = uLit - Io_ReadAigerDecode( &pCur );
+ uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
+ assert( uLit1 > uLit0 );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
+ pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
+ assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
+ Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
+ }
+ Extra_ProgressBarStop( pProgress );
+
+ // remember the place where symbols begin
+ pSymbols = pCur;
+
+ // read the latch driver literals
+ pCur = pDrivers;
+ 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 names if present
+ pCur = pSymbols;
+ while ( pCur < pContents + nFileSize && *pCur != 'c' )
+ {
+ // get the terminal type
+ pType = pCur;
+ if ( *pCur == 'i' )
+ vTerms = pNtkNew->vPis;
+ else if ( *pCur == 'l' )
+ vTerms = pNtkNew->vBoxes;
+ else if ( *pCur == 'o' )
+ vTerms = pNtkNew->vPos;
+ else
+ {
+ fprintf( stdout, "Wrong terminal type." );
+ return NULL;
+ }
+ // get the terminal number
+ iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
+ // get the node
+ if ( iTerm >= Vec_PtrSize(vTerms) )
+ {
+ fprintf( stdout, "The number of terminal is out of bound." );
+ return NULL;
+ }
+ pObj = Vec_PtrEntry( vTerms, iTerm );
+ if ( *pType == 'l' )
+ pObj = Abc_ObjFanout0(pObj);
+ // assign the name
+ pName = pCur; while ( *pCur++ != '\n' );
+ // assign this name
+ *(pCur-1) = 0;
+ Abc_ObjAssignName( pObj, pName, NULL );
+ if ( *pType == 'l' )
+ Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
+ // mark the node as named
+ pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+ }
+ // skipping the comments
+ free( pContents );
+ Vec_PtrFree( vNodes );
+
+ // assign the remaining names
+ Abc_NtkForEachPi( pNtkNew, pObj, i )
+ {
+ if ( pObj->pCopy ) continue;
+ Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+ }
+ Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
+ {
+ if ( pObj->pCopy ) continue;
+ Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+ Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL );
+ }
+ Abc_NtkForEachPo( pNtkNew, pObj, i )
+ {
+ if ( pObj->pCopy ) continue;
+ Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+ }
+
+ // remove the extra nodes
+// Abc_AigCleanup( pNtkNew->pManFunc );
+
+ // check the result
+ if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
+ {
+ printf( "Io_ReadAiger: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkNew );
+ return NULL;
+ }
+ return pNtkNew;
+}
+
+
+/**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/ioReadBaf.c b/src/base/io/ioReadBaf.c
index a6e0c2e2..8dce54af 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -30,7 +30,7 @@
/**Function*************************************************************
- Synopsis [Writes the AIG in the binary format.]
+ Synopsis [Reads the AIG in the binary format.]
Description []
@@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
Vec_PtrFree( vNodes );
// remove the extra nodes
- Abc_AigCleanup( pNtkNew->pManFunc );
+// Abc_AigCleanup( pNtkNew->pManFunc );
// check the result
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
new file mode 100644
index 00000000..2bc2ded3
--- /dev/null
+++ b/src/base/io/ioWriteAiger.c
@@ -0,0 +1,281 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteAiger.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write binary AIGER format developed by
+ Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - December 16, 2006.]
+
+ Revision [$Id: ioWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+ The following is taken from the AIGER format description,
+ which can be found at http://fmv.jku.at/aiger
+*/
+
+
+/*
+ The AIGER And-Inverter Graph (AIG) Format Version 20061129
+ ----------------------------------------------------------
+ Armin Biere, Johannes Kepler University, 2006
+
+ This report describes the AIG file format as used by the AIGER library.
+ The purpose of this report is not only to motivate and document the
+ format, but also to allow independent implementations of writers and
+ readers by giving precise and unambiguous definitions.
+
+ ...
+
+Introduction
+
+ The name AIGER contains as one part the acronym AIG of And-Inverter
+ Graphs and also if pronounced in German sounds like the name of the
+ 'Eiger', a mountain in the Swiss alps. This choice should emphasize the
+ origin of this format. It was first openly discussed at the Alpine
+ Verification Meeting 2006 in Ascona as a way to provide a simple, compact
+ file format for a model checking competition affiliated to CAV 2007.
+
+ ...
+
+Binary Format Definition
+
+ The binary format is semantically a subset of the ASCII format with a
+ slightly different syntax. The binary format may need to reencode
+ literals, but translating a file in binary format into ASCII format and
+ then back in to binary format will result in the same file.
+
+ The main differences of the binary format to the ASCII format are as
+ follows. After the header the list of input literals and all the
+ current state literals of a latch can be omitted. Furthermore the
+ definitions of the AND gates are binary encoded. However, the symbol
+ table and the comment section are as in the ASCII format.
+
+ The header of an AIGER file in binary format has 'aig' as format
+ identifier, but otherwise is identical to the ASCII header. The standard
+ file extension for the binary format is therefore '.aig'.
+
+ A header for the binary format is still in ASCII encoding:
+
+ aig M I L O A
+
+ Constants, variables and literals are handled in the same way as in the
+ ASCII format. The first simplifying restriction is on the variable
+ indices of inputs and latches. The variable indices of inputs come first,
+ followed by the pseudo-primary inputs of the latches and then the variable
+ indices of all LHS of AND gates:
+
+ input variable indices 1, 2, ... , I
+ latch variable indices I+1, I+2, ... , (I+L)
+ AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
+
+ The corresponding unsigned literals are
+
+ input literals 2, 4, ... , 2*I
+ latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
+ AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
+
+ All literals have to be defined, and therefore 'M = I + L + A'. With this
+ restriction it becomes possible that the inputs and the current state
+ literals of the latches do not have to be listed explicitly. Therefore,
+ after the header only the list of 'L' next state literals follows, one per
+ latch on a single line, and then the 'O' outputs, again one per line.
+
+ In the binary format we assume that the AND gates are ordered and respect
+ the child parent relation. AND gates with smaller literals on the LHS
+ come first. Therefore we can assume that the literals on the right-hand
+ side of a definition of an AND gate are smaller than the LHS literal.
+ Furthermore we can sort the literals on the RHS, such that the larger
+ literal comes first. A definition thus consists of three literals
+
+ lhs rhs0 rhs1
+
+ with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are
+ pairwise different to avoid combinational self loops. Since the LHS
+ indices of the definitions are all consecutive (as even integers),
+ the binary format does not have to keep 'lhs'. In addition, we can use
+ the order restriction and only write the differences 'delta0' and 'delta1'
+ instead of 'rhs0' and 'rhs1', with
+
+ delta0 = lhs - rhs0, delta1 = rhs0 - rhs1
+
+ The differences will all be strictly positive, and in practice often very
+ small. We can take advantage of this fact by the simple little-endian
+ encoding of unsigned integers of the next section. After the binary delta
+ encoding of the RHSs of all AND gates, the optional symbol table and
+ optional comment section start in the same format as in the ASCII case.
+
+ ...
+
+*/
+
+static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
+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; }
+
+static int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the AIG in the binary AIGER format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ ProgressBar * pProgress;
+ FILE * pFile;
+ Abc_Obj_t * pObj, * pDriver;
+ int i, nNodes, Pos, nBufferSize;
+ unsigned char * pBuffer;
+ unsigned uLit0, uLit1, uLit;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // start the output stream
+ pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteBaf(): Cannot open the output file \"%s\".\n", pFileName );
+ return;
+ }
+
+ // set the node numbers to be used in the output file
+ nNodes = 0;
+ Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ Io_ObjSetAigerNum( pObj, nNodes++ );
+ Abc_AigForEachAnd( pNtk, pObj, i )
+ 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",
+ Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
+ Abc_NtkPiNum(pNtk),
+ Abc_NtkLatchNum(pNtk),
+ Abc_NtkPoNum(pNtk),
+ Abc_NtkNodeNum(pNtk) );
+
+ // if the driver node is a constant, we need to complement the literal below
+ // 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 )
+ {
+ 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 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 );
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+ Abc_AigForEachAnd( pNtk, pObj, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
+ 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 );
+ if ( Pos > nBufferSize - 10 )
+ {
+ printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
+ fclose( pFile );
+ return;
+ }
+ }
+ assert( Pos < nBufferSize );
+ Extra_ProgressBarStop( pProgress );
+
+ // write the buffer
+ fwrite( pBuffer, 1, Pos, pFile );
+ free( pBuffer );
+
+ // write the symbol table
+ // write PIs
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
+ // write latches
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
+ // write POs
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
+
+ // write the comment
+ fprintf( pFile, "c\n" );
+ fprintf( pFile, "%s\n", pNtk->pName );
+ fprintf( pFile, "This file in the AIGER format was written by ABC on %s\n", Extra_TimeStamp() );
+ fprintf( pFile, "For information about the 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 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/base/io/module.make b/src/base/io/module.make
index 2d5e4b9e..1feffa0b 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -1,5 +1,6 @@
SRC += src/base/io/io.c \
src/base/io/ioRead.c \
+ src/base/io/ioReadAiger.c \
src/base/io/ioReadBaf.c \
src/base/io/ioReadBench.c \
src/base/io/ioReadBlif.c \
@@ -8,6 +9,7 @@ SRC += src/base/io/io.c \
src/base/io/ioReadPla.c \
src/base/io/ioReadVerilog.c \
src/base/io/ioUtil.c \
+ src/base/io/ioWriteAiger.c \
src/base/io/ioWriteBaf.c \
src/base/io/ioWriteBench.c \
src/base/io/ioWriteBlif.c \
diff --git a/src/map/fpga/fpgaCutUtils.c b/src/map/fpga/fpgaCutUtils.c
index 7779be1e..e60a1dee 100644
--- a/src/map/fpga/fpgaCutUtils.c
+++ b/src/map/fpga/fpgaCutUtils.c
@@ -340,7 +340,7 @@ float Fpga_CutGetAreaRefed( Fpga_Man_t * pMan, Fpga_Cut_t * pCut )
return 0;
aResult = Fpga_CutDeref( pMan, NULL, pCut, 0 );
aResult2 = Fpga_CutRef( pMan, NULL, pCut, 0 );
- assert( aResult == aResult2 );
+ assert( Fpga_FloatEqual( pMan, aResult, aResult2 ) );
return aResult;
}
@@ -362,7 +362,7 @@ float Fpga_CutGetAreaDerefed( Fpga_Man_t * pMan, Fpga_Cut_t * pCut )
return 0;
aResult2 = Fpga_CutRef( pMan, NULL, pCut, 0 );
aResult = Fpga_CutDeref( pMan, NULL, pCut, 0 );
- assert( aResult == aResult2 );
+ assert( Fpga_FloatEqual( pMan, aResult, aResult2 ) );
return aResult;
}
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index 14c2cbdb..b93eacab 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -278,6 +278,10 @@ struct Fpga_NodeVecStruct_t_
pFanout = pFanout2, \
pFanout2 = Fpga_NodeReadNextFanout(pNode, pFanout) )
+static inline Fpga_FloatMoreThan( Fpga_Man_t * p, float Arg1, float Arg2 ) { return Arg1 > Arg2 + p->fEpsilon; }
+static inline Fpga_FloatLessThan( Fpga_Man_t * p, float Arg1, float Arg2 ) { return Arg1 < Arg2 - p->fEpsilon; }
+static inline Fpga_FloatEqual( Fpga_Man_t * p, float Arg1, float Arg2 ) { return Arg1 > Arg2 - p->fEpsilon && Arg1 < Arg2 + p->fEpsilon; }
+
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c
index 9557494c..73fa1258 100644
--- a/src/map/fpga/fpgaMatch.c
+++ b/src/map/fpga/fpgaMatch.c
@@ -140,7 +140,7 @@ clk = clock();
Fpga_CutGetParameters( p, pCut );
//p->time2 += clock() - clk;
// drop the cut if it does not meet the required times
- if ( pCut->tArrival > pNode->tRequired )
+ if ( Fpga_FloatMoreThan(p, pCut->tArrival, pNode->tRequired) )
continue;
// if no cut is assigned, use the current one
if ( pNode->pCutBest == NULL )
@@ -152,11 +152,11 @@ clk = clock();
// (1) delay oriented mapping (first traversal), delay first, area-flow as a tie-breaker
// (2) area recovery (subsequent traversals), area-flow first, delay as a tie-breaker
if ( (fDelayOriented &&
- (pNode->pCutBest->tArrival > pCut->tArrival ||
- pNode->pCutBest->tArrival == pCut->tArrival && pNode->pCutBest->aFlow > pCut->aFlow)) ||
+ (Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival) ||
+ Fpga_FloatEqual(p, pNode->pCutBest->tArrival, pCut->tArrival) && Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) )) ||
(!fDelayOriented &&
- (pNode->pCutBest->aFlow > pCut->aFlow ||
- pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival)) )
+ (Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) ||
+ Fpga_FloatEqual(p, pNode->pCutBest->aFlow, pCut->aFlow) && Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival))) )
{
pNode->pCutBest = pCut;
}
@@ -289,7 +289,7 @@ clk = clock();
pCut->tArrival = Fpga_TimeCutComputeArrival( p, pCut );
//p->time2 += clock() - clk;
// drop the cut if it does not meet the required times
- if ( pCut->tArrival > pNode->tRequired )
+ if ( Fpga_FloatMoreThan( p, pCut->tArrival, pNode->tRequired ) )
continue;
// get the area of this cut
pCut->aFlow = Fpga_CutGetAreaDerefed( p, pCut );
@@ -300,8 +300,8 @@ clk = clock();
continue;
}
// choose the best cut as follows: exact area first, delay as a tie-breaker
- if ( pNode->pCutBest->aFlow > pCut->aFlow ||
- pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival )
+ if ( Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) ||
+ Fpga_FloatEqual(p, pNode->pCutBest->aFlow, pCut->aFlow) && Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival) )
{
pNode->pCutBest = pCut;
}
@@ -410,7 +410,7 @@ clk = clock();
pCut->tArrival = Fpga_TimeCutComputeArrival( p, pCut );
//p->time2 += clock() - clk;
// drop the cut if it does not meet the required times
- if ( pCut->tArrival > pNode->tRequired )
+ if ( Fpga_FloatMoreThan( p, pCut->tArrival, pNode->tRequired ) )
continue;
// get the area of this cut
pCut->aFlow = Fpga_CutGetSwitchDerefed( p, pNode, pCut );
@@ -421,8 +421,8 @@ clk = clock();
continue;
}
// choose the best cut as follows: exact area first, delay as a tie-breaker
- if ( pNode->pCutBest->aFlow > pCut->aFlow ||
- pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival )
+ if ( Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) ||
+ Fpga_FloatEqual(p, pNode->pCutBest->aFlow, pCut->aFlow) && Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival) )
{
pNode->pCutBest = pCut;
}
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 1bbed29d..eaa08a3a 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -273,10 +273,10 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r
#define If_ObjForEachCutStart( pObj, pCut, i, Start ) \
for ( i = Start; (i < (int)(pObj)->nCuts) && ((pCut) = (pObj)->Cuts + i); i++ )
// iterator over the leaves of the cut
-//#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \
-// for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \
- for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
+ for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
+//#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \
+// for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
// iterator over the leaves of the sequential cut
#define If_CutForEachLeafSeq( p, pCut, pLeaf, Shift, i ) \
for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i] >> 8)) && (((Shift) = ((pCut)->pLeaves[i] & 255)) >= 0); i++ )
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 5366aaf5..8c092b99 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -257,9 +257,11 @@ static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t
pC->pLeaves[k++] = pC1->pLeaves[i];
pC->nLeaves++;
}
+/*
assert( pC->nLeaves <= pC->nLimit );
for ( i = 1; i < (int)pC->nLeaves; i++ )
assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
+*/
return 1;
}
@@ -574,7 +576,8 @@ float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
aResult2 = If_CutRef( p, pCut, nLevels );
aResult = If_CutDeref( p, pCut, nLevels );
- assert( aResult == aResult2 );
+ assert( aResult > aResult2 - p->fEpsilon );
+ assert( aResult < aResult2 + p->fEpsilon );
return aResult;
}
@@ -595,7 +598,8 @@ float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
aResult2 = If_CutDeref( p, pCut, nLevels );
aResult = If_CutRef( p, pCut, nLevels );
- assert( aResult == aResult2 );
+ assert( aResult > aResult2 - p->fEpsilon );
+ assert( aResult < aResult2 + p->fEpsilon );
return aResult;
}
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 4d422359..4cdd7a87 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -189,38 +189,43 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
pCut = p->ppCuts[iCut];
// generate cuts
for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
- If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
{
- assert( pTemp->nCuts > 1 );
- assert( pTemp == pObj || pTemp->nRefs == 0 );
- // copy the cut into storage
- If_CutCopy( pCut, pCutTemp );
- // check if this cut is contained in any of the available cuts
- if ( If_CutFilter( p, pCut ) )
- continue;
- // the cuts have been successfully merged
- // check if the cut satisfies the required times
- assert( pCut->Delay == If_CutDelay( p, pCut ) );
- if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
- continue;
- // set the phase attribute
- pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
- // compute area of the cut (this area may depend on the application specific cost)
- pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
- pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
- // make sure the cut is the last one (after filtering it may not be so)
- assert( pCut == p->ppCuts[iCut] );
- p->ppCuts[iCut] = p->ppCuts[p->nCuts];
- p->ppCuts[p->nCuts] = pCut;
- // count the cut
- p->nCuts++;
- // prepare room for the next cut
- iCut = p->nCuts;
- pCut = p->ppCuts[iCut];
+ If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
+ {
+ assert( pTemp->nCuts > 1 );
+ assert( pTemp == pObj || pTemp->nRefs == 0 );
+ // copy the cut into storage
+ If_CutCopy( pCut, pCutTemp );
+ // check if this cut is contained in any of the available cuts
+ if ( If_CutFilter( p, pCut ) )
+ continue;
+ // the cuts have been successfully merged
+ // check if the cut satisfies the required times
+ assert( pCut->Delay == If_CutDelay( p, pCut ) );
+ if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
+ continue;
+ // set the phase attribute
+ pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
+ // compute area of the cut (this area may depend on the application specific cost)
+ pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+ pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
+ // make sure the cut is the last one (after filtering it may not be so)
+ assert( pCut == p->ppCuts[iCut] );
+ p->ppCuts[iCut] = p->ppCuts[p->nCuts];
+ p->ppCuts[p->nCuts] = pCut;
+ // count the cut
+ p->nCuts++;
+ // prepare room for the next cut
+ iCut = p->nCuts;
+ pCut = p->ppCuts[iCut];
+ // quit if we exceeded the number of cuts
+ if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
+ break;
+ }
// quit if we exceeded the number of cuts
if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
break;
- }
+ }
assert( p->nCuts > 0 );
// sort if we have more cuts
If_ManSortCuts( p, Mode );
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index ddc74a49..cd90a313 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -96,7 +96,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
// print the statistic into a file
{
FILE * pTable;
- pTable = fopen( "a/seqmap__stats.txt", "a+" );
+ pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
fprintf( pTable, "%d ", p->Period );
fprintf( pTable, "\n" );
fclose( pTable );
@@ -198,7 +198,7 @@ int If_ManBinarySearchPeriod( If_Man_t * p, int Mode )
// report the results
if ( p->pPars->fVerbose )
{
- p->AreaGlo = p->pPars->fLiftLeaves? If_ManScanMappingSeq(p) : If_ManScanMapping(p);
+ p->AreaGlo = p->pPars->fLiftLeaves? 0/*If_ManScanMappingSeq(p)*/ : If_ManScanMapping(p);
printf( "Attempt = %2d. Iters = %3d. Area = %10.2f. Fi = %6.2f. ", p->nAttempts, c, p->AreaGlo, (float)p->Period );
if ( fConverged )
printf( " Feasible" );
@@ -358,7 +358,9 @@ int If_ManPrepareMappingSeq( If_Man_t * p )
pCut->Delay -= p->Period;
pCut->fCompl ^= pObj->fCompl0;
- pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
+ // there is a bug here, which shows when there are choices...
+// pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
+ pTemp = If_ManObj(p, pCut->pLeaves[0]);
assert( !If_ObjIsLatch(pTemp) );
}
}
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index f0041868..0cf2f73c 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -186,7 +186,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
If_Obj_t * pLeaf;
int i, j, best_i, temp;
// start the trivial permutation and collect pin delays
- If_CutForEachLeaf( p, pCut, pLeaf, i );
+ If_CutForEachLeaf( p, pCut, pLeaf, i )
{
pPinPerm[i] = i;
pPinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
@@ -206,8 +206,12 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
pPinPerm[best_i] = temp;
}
// verify
+ assert( pPinPerm[0] < pCut->nLeaves );
for ( i = 1; i < (int)pCut->nLeaves; i++ )
+ {
+ assert( pPinPerm[i] < (int)pCut->nLeaves );
assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
+ }
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index 4b136f55..797d853d 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -269,7 +269,11 @@ float If_ManScanMappingSeq_rec( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vMapp
If_Cut_t * pCutBest;
float aArea;
int i, Shift;
- if ( pObj->nRefs++ || If_ObjIsCi(pObj) || If_ObjIsConst1(pObj) )
+ // treat latches transparently
+ if ( If_ObjIsLatch(pObj) )
+ return If_ManScanMappingSeq_rec( p, If_ObjFanin0(pObj), vMapped );
+ // consider trivial cases
+ if ( pObj->nRefs++ || If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) )
return 0.0;
// store the node in the structure by level
assert( If_ObjIsAnd(pObj) );
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 38513a93..3b8662ec 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -388,10 +388,11 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
int i;
if ( p->nSize >= nSize )
return;
- if ( p->nSize < 2 * nSize )
+ assert( p->nSize < nSize );
+ if ( 2 * p->nSize > nSize )
Vec_PtrGrow( p, 2 * nSize );
else
- Vec_PtrGrow( p, p->nSize );
+ Vec_PtrGrow( p, nSize );
for ( i = p->nSize; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
diff --git a/src/opt/ret/retLvalue.c b/src/opt/ret/retLvalue.c
index ca4b289f..b4d9e946 100644
--- a/src/opt/ret/retLvalue.c
+++ b/src/opt/ret/retLvalue.c
@@ -127,6 +127,14 @@ clkIter = clock() - clk;
NodeLag = Abc_NodeComputeLag( Abc_NodeGetLValue(pNode), FiBest );
Vec_IntWriteEntry( vLags, pNode->Id, NodeLag );
}
+/*
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ printf( "%d ", Abc_NodeGetLValue(Abc_ObjFanin0(pNode)) );
+ printf( "\n" );
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ printf( "%d/%d ", Abc_NodeGetLValue(Abc_ObjFanout0(pNode)), Abc_NodeGetLValue(Abc_ObjFanout0(pNode)) + FiBest );
+ printf( "\n" );
+*/
// print the result
// if ( fVerbose )
@@ -134,7 +142,7 @@ clkIter = clock() - clk;
/*
{
FILE * pTable;
- pTable = fopen( "a/seqmap__stats.txt", "a+" );
+ pTable = fopen( "iscas/seqmap__stats2.txt", "a+" );
fprintf( pTable, "%d ", FiBest );
fprintf( pTable, "\n" );
fclose( pTable );
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index fc612f95..4ce71a9b 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -28,6 +28,7 @@
static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
static int Rwr_CutIsBoolean( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
static int Rwr_CutCountNumNodes( Abc_Obj_t * pObj, Cut_Cut_t * pCut );
+static int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -186,6 +187,13 @@ p->timeRes += clock() - clk;
// copy the leaves
Vec_PtrForEachEntry( p->vFanins, pFanin, i )
Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
+/*
+ printf( "(" );
+ Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+ printf( " %d", Abc_ObjRegular(pFanin)->vFanouts.nSize - 1 );
+ printf( " ) " );
+*/
+// printf( "%d ", Rwr_NodeGetDepth_rec( pNode, p->vFanins ) );
p->nScores[p->pMap[uTruthBest]]++;
p->nNodesGained += GainBest;
@@ -384,6 +392,32 @@ int Rwr_CutCountNumNodes( Abc_Obj_t * pObj, Cut_Cut_t * pCut )
return Counter;
}
+
+/**Function*************************************************************
+
+ Synopsis [Returns depth of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
+{
+ Abc_Obj_t * pLeaf;
+ int i, Depth0, Depth1;
+ if ( Abc_ObjIsCi(pObj) )
+ return 0;
+ Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+ if ( pObj == Abc_ObjRegular(pLeaf) )
+ return 0;
+ Depth0 = Rwr_NodeGetDepth_rec( Abc_ObjFanin0(pObj), vLeaves );
+ Depth1 = Rwr_NodeGetDepth_rec( Abc_ObjFanin1(pObj), vLeaves );
+ return 1 + ABC_MAX( Depth0, Depth1 );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:53:01 +0000