From be6a484a997a8477d4c3b03c17f798c1b0061bf1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 16 Dec 2006 08:01:00 -0800 Subject: Version abc61216 --- src/aig/ivy/ivyMem.c | 7 +- src/base/abc/abcCheck.c | 11 +- src/base/abc/abcNames.c | 2 +- src/base/abci/abc.c | 8 +- src/base/abci/abcPrint.c | 2 +- src/base/io/io.c | 168 +++++++++++++++++++++++--- src/base/io/io.h | 4 + src/base/io/ioRead.c | 2 + src/base/io/ioReadAiger.c | 273 ++++++++++++++++++++++++++++++++++++++++++ src/base/io/ioReadBaf.c | 4 +- src/base/io/ioWriteAiger.c | 281 ++++++++++++++++++++++++++++++++++++++++++++ src/base/io/module.make | 2 + src/map/fpga/fpgaCutUtils.c | 4 +- src/map/fpga/fpgaInt.h | 4 + src/map/fpga/fpgaMatch.c | 22 ++-- src/map/if/if.h | 6 +- src/map/if/ifCut.c | 8 +- src/map/if/ifMap.c | 61 +++++----- src/map/if/ifSeq.c | 8 +- src/map/if/ifTime.c | 6 +- src/map/if/ifUtil.c | 6 +- src/misc/vec/vecPtr.h | 5 +- src/opt/ret/retLvalue.c | 10 +- src/opt/rwr/rwrEva.c | 34 ++++++ 24 files changed, 853 insertions(+), 85 deletions(-) create mode 100644 src/base/io/ioReadAiger.c create mode 100644 src/base/io/ioWriteAiger.c (limited to 'src') 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<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] \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] \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; @@ -981,6 +1058,65 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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] \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 [] @@ -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] \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 /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3