diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abc/abcCheck.c | 11 | ||||
| -rw-r--r-- | src/base/abc/abcNames.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 8 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/base/io/io.c | 168 | ||||
| -rw-r--r-- | src/base/io/io.h | 4 | ||||
| -rw-r--r-- | src/base/io/ioRead.c | 2 | ||||
| -rw-r--r-- | src/base/io/ioReadAiger.c | 273 | ||||
| -rw-r--r-- | src/base/io/ioReadBaf.c | 4 | ||||
| -rw-r--r-- | src/base/io/ioWriteAiger.c | 281 | ||||
| -rw-r--r-- | src/base/io/module.make | 2 |
11 files changed, 729 insertions, 28 deletions
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 \ |