luke/abc
1
0
Fork 0
mirror of https://github.com/YosysHQ/abc.git synced 2026-09-04 08:33:58 +02:00
Code Issues Packages Projects Releases Wiki Activity

Version abc80701

Browse Source
This commit is contained in:
Alan Mishchenko
2008-07-01 08:01:00 -07:00
parent d0341836dd
commit 4a9789e58d
34 changed files with 10624 additions and 59 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/base/abci/abc.c
+29 -16
View File
@@ -17462,22 +17462,23 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
extern int Ntl_ManIsComb( void * p );
// set defaults
pPars->nPartSize = 0;
pPars->nOverSize = 0;
pPars->nFramesP = 0;
pPars->nFramesK = 1;
pPars->nMaxImps = 5000;
pPars->nMaxLevs = 0;
pPars->fUseImps = 0;
pPars->fRewrite = 0;
pPars->fFraiging = 0;
pPars->fLatchCorr = 0;
pPars->fWriteImps = 0;
pPars->fUse1Hot = 0;
pPars->fVerbose = 0;
pPars->TimeLimit = 0;
pPars->nPartSize = 0;
pPars->nOverSize = 0;
pPars->nFramesP = 0;
pPars->nFramesK = 1;
pPars->nMaxImps = 5000;
pPars->nMaxLevs = 0;
pPars->nMinDomSize = 100;
pPars->fUseImps = 0;
pPars->fRewrite = 0;
pPars->fFraiging = 0;
pPars->fLatchCorr = 0;
pPars->fWriteImps = 0;
pPars->fUse1Hot = 0;
pPars->fVerbose = 0;
pPars->TimeLimit = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILCirfletvh" ) ) != EOF )
{
switch ( c )
{
@@ -17547,6 +17548,17 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nMaxLevs <= 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMinDomSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMinDomSize <= 0 )
goto usage;
break;
case 'i':
pPars->fUseImps ^= 1;
break;
@@ -17623,13 +17635,14 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( stdout, "usage: *ssw [-PQNFL num] [-lrfetvh]\n" );
fprintf( stdout, "usage: *ssw [-PQNFLC num] [-lrfetvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction on the netlist \n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
fprintf( stdout, "\t-C num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
// fprintf( stdout, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
// fprintf( stdout, "\t-i : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
src/base/io/ioReadAiger.c
+99 -5
View File
@@ -20,6 +20,7 @@
***********************************************************************/
#include "ioAbc.h"
#include <bzlib.h>
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -85,6 +86,92 @@ Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries )
return vLits;
}
/**Function*************************************************************
Synopsis [Reads the file into a character buffer.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
typedef struct buflist {
char buf[1<<20];
int nBuf;
struct buflist * next;
} buflist;
static char * Ioa_ReadLoadFileBz2Aig( char * pFileName )
{
FILE * pFile;
int nFileSize = 0;
char * pContents;
BZFILE * b;
int bzError;
struct buflist * pNext;
buflist * bufHead = NULL, * buf = NULL;
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Ioa_ReadLoadFileBz2(): The file is unavailable (absent or open).\n" );
return NULL;
}
b = BZ2_bzReadOpen(&bzError,pFile,0,0,NULL,0);
if (bzError != BZ_OK) {
printf( "Ioa_ReadLoadFileBz2(): BZ2_bzReadOpen() failed with error %d.\n",bzError );
return NULL;
}
do {
if (!bufHead)
buf = bufHead = ALLOC( buflist, 1 );
else
buf = buf->next = ALLOC( buflist, 1 );
nFileSize += buf->nBuf = BZ2_bzRead(&bzError,b,buf->buf,1<<20);
buf->next = NULL;
} while (bzError == BZ_OK);
if (bzError == BZ_STREAM_END) {
// we're okay
char * p;
int nBytes = 0;
BZ2_bzReadClose(&bzError,b);
p = pContents = ALLOC( char, nFileSize + 10 );
buf = bufHead;
do {
memcpy(p+nBytes,buf->buf,buf->nBuf);
nBytes += buf->nBuf;
// } while((buf = buf->next));
pNext = buf->next;
free( buf );
} while((buf = pNext));
} else if (bzError == BZ_DATA_ERROR_MAGIC) {
// not a BZIP2 file
BZ2_bzReadClose(&bzError,b);
fseek( pFile, 0, SEEK_END );
nFileSize = ftell( pFile );
if ( nFileSize == 0 )
{
printf( "Ioa_ReadLoadFileBz2(): The file is empty.\n" );
return NULL;
}
pContents = ALLOC( char, nFileSize + 10 );
rewind( pFile );
fread( pContents, nFileSize, 1, pFile );
} else {
// Some other error.
printf( "Ioa_ReadLoadFileBz2(): Unable to read the compressed BLIF.\n" );
return NULL;
}
fclose( pFile );
// finish off the file with the spare .end line
// some benchmarks suddenly break off without this line
strcpy( pContents + nFileSize, "\n.end\n" );
return pContents;
}
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
@@ -109,11 +196,18 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
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 );
if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
pContents = Ioa_ReadLoadFileBz2Aig( pFileName );
else
{
// pContents = Ioa_ReadLoadFile( pFileName );
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 || (pContents[3] != ' ' && pContents[3] != '2') )
src/base/io/ioWriteAiger.c
+255 -7
View File
@@ -21,6 +21,13 @@
#include "ioAbc.h"
#include <bzlib.h>
#include <stdarg.h>
#ifdef _WIN32
#define vsnprintf _vsnprintf
#endif
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -248,7 +255,7 @@ Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits )
SeeAlso []
***********************************************************************/
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
{
ProgressBar * pProgress;
FILE * pFile;
@@ -258,6 +265,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
unsigned uLit0, uLit1, uLit;
assert( Abc_NtkIsStrash(pNtk) );
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
return;
}
// start the output stream
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
@@ -265,12 +279,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
return;
}
// set the node numbers to be used in the output file
nNodes = 0;
@@ -368,6 +376,246 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Procedure to write data into BZ2 file.]
Description [Based on the vsnprintf() man page.]
SideEffects []
SeeAlso []
***********************************************************************/
typedef struct bz2file {
FILE * f;
BZFILE * b;
char * buf;
int nBytes;
int nBytesMax;
} bz2file;
int fprintfBz2Aig( bz2file * b, char * fmt, ... ) {
if (b->b) {
char * newBuf;
int bzError;
va_list ap;
while (1) {
va_start(ap,fmt);
b->nBytes = vsnprintf(b->buf,b->nBytesMax,fmt,ap);
va_end(ap);
if (b->nBytes > -1 && b->nBytes < b->nBytesMax)
break;
if (b->nBytes > -1)
b->nBytesMax = b->nBytes + 1;
else
b->nBytesMax *= 2;
if ((newBuf = REALLOC( char,b->buf,b->nBytesMax )) == NULL)
return -1;
else
b->buf = newBuf;
}
BZ2_bzWrite( &bzError, b->b, b->buf, b->nBytes );
if (bzError == BZ_IO_ERROR) {
fprintf( stdout, "Ioa_WriteBlif(): I/O error writing to compressed stream.\n" );
return -1;
}
return b->nBytes;
} else {
int n;
va_list ap;
va_start(ap,fmt);
n = vfprintf( b->f, fmt, ap);
va_end(ap);
return n;
}
}
/**Function*************************************************************
Synopsis [Writes the AIG in the binary AIGER format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
{
ProgressBar * pProgress;
// FILE * pFile;
Abc_Obj_t * pObj, * pDriver;
int i, nNodes, Pos, nBufferSize, bzError;
unsigned char * pBuffer;
unsigned uLit0, uLit1, uLit;
bz2file b;
// check that the network is valid
assert( Abc_NtkIsStrash(pNtk) );
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
return;
}
memset(&b,0,sizeof(b));
b.nBytesMax = (1<<12);
b.buf = ALLOC( char,b.nBytesMax );
// start the output stream
b.f = fopen( pFileName, "wb" );
if ( b.f == NULL )
{
fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName );
FREE(b.buf);
return;
}
if (!strncmp(pFileName+strlen(pFileName)-4,".bz2",4)) {
b.b = BZ2_bzWriteOpen( &bzError, b.f, 9, 0, 0 );
if ( bzError != BZ_OK ) {
BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
fprintf( stdout, "Ioa_WriteBlif(): Cannot start compressed stream.\n" );
fclose( b.f );
FREE(b.buf);
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
fprintfBz2Aig( &b, "aig%s %u %u %u %u %u\n",
fCompact? "2" : "",
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
if ( !fCompact )
{
// write latch drivers
Abc_NtkForEachLatchInput( pNtk, pObj, i )
{
pDriver = Abc_ObjFanin0(pObj);
fprintfBz2Aig( &b, "%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);
fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
}
}
else
{
Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
if ( !b.b )
fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), b.f );
else
{
BZ2_bzWrite( &bzError, b.b, Vec_StrArray(vBinary), Vec_StrSize(vBinary) );
if (bzError == BZ_IO_ERROR) {
fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
fclose( b.f );
FREE(b.buf);
return;
}
}
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
// write the nodes into the buffer
Pos = 0;
nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
pBuffer = ALLOC( unsigned 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, (unsigned)(uLit - uLit1) );
Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
if ( Pos > nBufferSize - 10 )
{
printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
fclose( b.f );
FREE(b.buf);
return;
}
}
assert( Pos < nBufferSize );
Extra_ProgressBarStop( pProgress );
// write the buffer
if ( !b.b )
fwrite( pBuffer, 1, Pos, b.f );
else
{
BZ2_bzWrite( &bzError, b.b, pBuffer, Pos );
if (bzError == BZ_IO_ERROR) {
fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
fclose( b.f );
FREE(b.buf);
return;
}
}
free( pBuffer );
// write the symbol table
if ( fWriteSymbols )
{
// write PIs
Abc_NtkForEachPi( pNtk, pObj, i )
fprintfBz2Aig( &b, "i%d %s\n", i, Abc_ObjName(pObj) );
// write latches
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintfBz2Aig( &b, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
// write POs
Abc_NtkForEachPo( pNtk, pObj, i )
fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) );
}
// write the comment
fprintfBz2Aig( &b, "c\n" );
if ( pNtk->pName && strlen(pNtk->pName) > 0 )
fprintfBz2Aig( &b, ".model %s\n", pNtk->pName );
fprintfBz2Aig( &b, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
// close the file
if (b.b) {
BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
if (bzError == BZ_IO_ERROR) {
fprintf( stdout, "Io_WriteAiger(): I/O error closing compressed stream.\n" );
fclose( b.f );
FREE(b.buf);
return;
}
}
fclose( b.f );
FREE(b.buf);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////