luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merged two last changes.

This commit is contained in:
Alan Mishchenko 2011-06-25 09:45:04 -07:00
parent 15cc374fe3 5b639818e9
commit 49869d08ec
3 changed files with 134 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
src/base/io/io.c
View File

@ -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 );
@ -1423,6 +1425,52 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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 []

1
src/base/io/ioAbc.h
View File

@ -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 ===========================================================*/

85
src/base/io/ioWriteAiger.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////