diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-06-25 09:45:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-06-25 09:45:04 -0700 |
commit | 49869d08ec3b318e649109936eb7593390e7f878 (patch) | |
tree | 32bfb3b4c28ef5da6bfcc5d50b0e53797d32b5b0 /src/base | |
parent | 15cc374fe35ff37d989baf1dade97162e6a20e8e (diff) | |
parent | 5b639818e95dc5978ad04d3685bfc4e15831c0ce (diff) | |
download | abc-49869d08ec3b318e649109936eb7593390e7f878.tar.gz abc-49869d08ec3b318e649109936eb7593390e7f878.tar.bz2 abc-49869d08ec3b318e649109936eb7593390e7f878.zip |
Merged two last changes.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/io/io.c | 48 | ||||
-rw-r--r-- | src/base/io/ioAbc.h | 1 | ||||
-rw-r--r-- | src/base/io/ioWriteAiger.c | 85 |
3 files changed, 134 insertions, 0 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index 7f077e29..d8277b08 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -48,6 +48,7 @@ static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBblif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -111,6 +112,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write", IoCommandWrite, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_aiger_cex", IoCommandWriteAigerCex, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bblif", IoCommandWriteBblif, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); @@ -1434,6 +1436,52 @@ usage: SeeAlso [] ***********************************************************************/ +int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + char * pFileName; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pCex == NULL ) + { + fprintf( pAbc->Out, "There is no current CEX.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + // get the output file name + pFileName = argv[globalUtilOptind]; + Io_WriteAigerCex( pAbc->pCex, pAbc->pNtkCur, pAbc->pGia, pFileName ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_aiger_cex [-h] <file>\n" ); + fprintf( pAbc->Err, "\t writes the current CEX 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\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h index 841fce40..fa3f6240 100644 --- a/src/base/io/ioAbc.h +++ b/src/base/io/ioAbc.h @@ -97,6 +97,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck ) extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); /*=== abcWriteAiger.c =========================================================*/ extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ); +extern void Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName ); /*=== abcWriteBaf.c ===========================================================*/ extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); /*=== abcWriteBblif.c ===========================================================*/ diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 1087af4f..18264d6b 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -752,6 +752,91 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f ABC_FREE(b.buf); } + +#include "giaAig.h" +#include "saig.h" + +/**Function************************************************************* + + Synopsis [Writes the AIG in the binary AIGER format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName ) +{ + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + FILE * pFile; + Aig_Man_t * pAig; + Aig_Obj_t * pObj, * pObj2; + Gia_Man_t * pGia = (Gia_Man_t *)pG; + int k, f, b; + assert( pCex != NULL ); + + // derive AIG + if ( pNtk != NULL && + Abc_NtkPiNum(pNtk) == pCex->nPis && + Abc_NtkLatchNum(pNtk) == pCex->nRegs ) + { + pAig = Abc_NtkToDar( pNtk, 0, 1 ); + } + else if ( pGia != NULL && + Gia_ManPiNum(pGia) == pCex->nPis && + Gia_ManRegNum(pGia) == pCex->nRegs ) + { + pAig = Gia_ManToAigSimple( pGia ); + } + else + { + printf( "AIG parameters do not match those of the CEX.\n" ); + return; + } + + // create output file + pFile = fopen( pFileName, "wb" ); + fprintf( pFile, "1\n" ); + b = pCex->nRegs; + for ( k = 0; k < pCex->nRegs; k++ ) + fprintf( pFile, "0" ); + fprintf( pFile, " " ); + Aig_ManCleanMarkA( pAig ); + for ( f = 0; f <= pCex->iFrame; f++ ) + { + for ( k = 0; k < pCex->nPis; k++ ) + { + fprintf( pFile, "%d", Aig_InfoHasBit(pCex->pData, b) ); + Aig_ManPi( pAig, k )->fMarkA = Aig_InfoHasBit(pCex->pData, b++); + } + fprintf( pFile, " " ); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)); + Saig_ManForEachPo( pAig, pObj, k ) + fprintf( pFile, "%d", pObj->fMarkA ); + fprintf( pFile, " " ); + Saig_ManForEachLi( pAig, pObj, k ) + fprintf( pFile, "%d", pObj->fMarkA ); + fprintf( pFile, "\n" ); + if ( f == pCex->iFrame ) + break; + Saig_ManForEachLi( pAig, pObj, k ) + fprintf( pFile, "%d", pObj->fMarkA ); + fprintf( pFile, " " ); + Saig_ManForEachLiLo( pAig, pObj, pObj2, k ) + pObj2->fMarkA = pObj->fMarkA; + } + assert( b == pCex->nBits ); + fclose( pFile ); + Aig_ManCleanMarkA( pAig ); + Aig_ManStop( pAig ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |