Commit 77536ad1 by Alan Mishchenko

Version abc51010

parent 8ed83f17
...@@ -310,6 +310,10 @@ SOURCE=.\src\base\abcs\abcSeq.c ...@@ -310,6 +310,10 @@ SOURCE=.\src\base\abcs\abcSeq.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\abcs\abcSeqMan.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abcs\abcShare.c SOURCE=.\src\base\abcs\abcShare.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -374,6 +378,10 @@ SOURCE=.\src\base\io\ioRead.c ...@@ -374,6 +378,10 @@ SOURCE=.\src\base\io\ioRead.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\io\ioReadBaf.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioReadBench.c SOURCE=.\src\base\io\ioReadBench.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -402,6 +410,10 @@ SOURCE=.\src\base\io\ioUtil.c ...@@ -402,6 +410,10 @@ SOURCE=.\src\base\io\ioUtil.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\io\ioWriteBaf.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteBench.c SOURCE=.\src\base\io\ioWriteBench.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
No preview for this file type
/**CFile****************************************************************
FileName [abcSeqMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Manager of sequential AIGs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcSeqMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Abc_SeqLat_t_ Abc_SeqLat_t;
struct Abc_SeqLat_t_
{
Abc_SeqLat_t * pNext; // the next Lat in the ring
Abc_SeqLat_t * pPrev; // the prev Lat in the ring
};
typedef struct Abc_SeqMan_t_ Abc_SeqMan_t;
struct Abc_SeqMan_t_
{
int nSize; // the number of entries in all internal arrays
Vec_Ptr_t * vInits; // the initial states for each edge in the AIG
Extra_MmFixed_t * pMmInits; // memory manager for initial states of the Lates
};
// reading the contents of the lat
static inline Abc_InitType_t Abc_SeqLatInit( Abc_SeqLat_t * pLat ) { return ((unsigned)pLat->pPrev) & 3; }
static inline Abc_SeqLat_t * Abc_SeqLatNext( Abc_SeqLat_t * pLat ) { return pLat->pNext; }
static inline Abc_SeqLat_t * Abc_SeqLatPrev( Abc_SeqLat_t * pLat ) { return (void *)(((unsigned)pLat->pPrev) & (ABC_FULL_MASK << 2)); }
// setting the contents of the lat
static inline void Abc_SeqLatSetInit( Abc_SeqLat_t * pLat, Abc_InitType_t Init ) { pLat->pPrev = (void *)( (3 & Init) | (((unsigned)pLat->pPrev) & (ABC_FULL_MASK << 2)) ); }
static inline void Abc_SeqLatSetNext( Abc_SeqLat_t * pLat, Abc_SeqLat_t * pNext ) { pLat->pNext = pNext; }
static inline void Abc_SeqLatSetPrev( Abc_SeqLat_t * pLat, Abc_SeqLat_t * pPrev ) { Abc_InitType_t Init = Abc_SeqLatInit(pLat); pLat->pPrev = pPrev; Abc_SeqLatSetInit(pLat, Init); }
// accessing initial state datastructure
static inline Vec_Ptr_t * Abc_SeqNodeInits( Abc_Obj_t * pObj ) { return ((Abc_SeqMan_t*)pObj->pNtk->pManFunc)->vInits; }
static inline Abc_SeqLat_t * Abc_SeqNodeReadInit( Abc_Obj_t * pObj, int Edge ) { return Vec_PtrEntry( Abc_SeqNodeInits(pObj), (pObj->Id<<1)+Edge ); }
static inline void Abc_SeqNodeSetInit ( Abc_Obj_t * pObj, int Edge, Abc_SeqLat_t * pInit ) { Vec_PtrWriteEntry( Abc_SeqNodeInits(pObj), (pObj->Id<<1)+Edge, pInit ); }
static inline Abc_SeqLat_t * Abc_SeqNodeCreateLat( Abc_Obj_t * pObj ) { return (Abc_SeqLat_t *)Extra_MmFixedEntryFetch( ((Abc_SeqMan_t*)pObj->pNtk->pManFunc)->pMmInits ); }
static inline void Abc_SeqNodeRecycleLat( Abc_Obj_t * pObj, Abc_SeqLat_t * pLat ) { Extra_MmFixedEntryRecycle( ((Abc_SeqMan_t*)pObj->pNtk->pManFunc)->pMmInits, (char *)pLat ); }
// getting the Lat with the given number
static inline Abc_SeqLat_t * Abc_SeqNodeGetLat( Abc_Obj_t * pObj, int Edge, int iLat )
{
int Counter;
Abc_SeqLat_t * pLat = Abc_SeqNodeReadInit(pObj, Edge);
for ( Counter = 0; Counter != iLat; Counter++ )
pLat = pLat->pNext;
return pLat;
}
// getting the first Lat
static inline Abc_SeqLat_t * Abc_SeqNodeGetLatFirst( Abc_Obj_t * pObj, int Edge )
{
return Abc_SeqNodeReadInit(pObj, Edge);
}
// getting the last Lat
static inline Abc_SeqLat_t * Abc_SeqNodeGetLatLast( Abc_Obj_t * pObj, int Edge )
{
return Abc_SeqLatPrev( Abc_SeqNodeReadInit(pObj, Edge) );
}
// getting the init value of the given Lat on the edge
static inline Abc_InitType_t Abc_SeqNodeGetInitOne( Abc_Obj_t * pObj, int Edge, int iLat )
{
return Abc_SeqLatInit( Abc_SeqNodeGetLat(pObj, Edge, iLat) );
}
// geting the init value of the first Lat on the edge
static inline Abc_InitType_t Abc_SeqNodeGetInitFirst( Abc_Obj_t * pObj, int Edge )
{
return Abc_SeqLatInit( Abc_SeqNodeGetLatFirst(pObj, Edge) );
}
// geting the init value of the last Lat on the edge
static inline Abc_InitType_t Abc_SeqNodeGetInitLast( Abc_Obj_t * pObj, int Edge )
{
return Abc_SeqLatInit( Abc_SeqNodeGetLatLast(pObj, Edge) );
}
// setting the init value of the given Lat on the edge
static inline void Abc_SeqNodeSetInitOne( Abc_Obj_t * pObj, int Edge, int iLat, Abc_InitType_t Init )
{
Abc_SeqLatSetInit( Abc_SeqNodeGetLat(pObj, Edge, iLat), Init );
}
// insert the first Lat on the edge
static inline void Abc_SeqNodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
{
Abc_SeqLat_t * pLat, * pRing, * pPrev;
pLat = Abc_SeqNodeCreateLat( pObj );
pRing = Abc_SeqNodeReadInit( pObj, Edge );
if ( pRing == NULL )
{
pLat->pNext = pLat->pPrev = pLat;
Abc_SeqNodeSetInit( pObj, Edge, pLat );
}
else
{
Abc_SeqLatSetPrev( pRing, pLat );
Abc_SeqLatSetNext( pLat, pRing );
pPrev = Abc_SeqLatPrev( pRing );
Abc_SeqLatSetPrev( pLat, pPrev );
Abc_SeqLatSetNext( pPrev, pLat );
Abc_SeqNodeSetInit( pObj, Edge, pLat ); // rotate the ring to make pLat the first
}
Abc_SeqLatSetInit( pLat, Init );
}
// insert the last Lat on the edge
static inline void Abc_SeqNodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
{
Abc_SeqLat_t * pLat, * pRing, * pPrev;
pLat = Abc_SeqNodeCreateLat( pObj );
pRing = Abc_SeqNodeReadInit( pObj, Edge );
if ( pRing == NULL )
{
pLat->pNext = pLat->pPrev = pLat;
Abc_SeqNodeSetInit( pObj, Edge, pLat );
}
else
{
Abc_SeqLatSetPrev( pRing, pLat );
Abc_SeqLatSetNext( pLat, pRing );
pPrev = Abc_SeqLatPrev( pRing );
Abc_SeqLatSetPrev( pLat, pPrev );
Abc_SeqLatSetNext( pPrev, pLat );
}
Abc_SeqLatSetInit( pLat, Init );
}
// delete the first Lat on the edge
static inline Abc_InitType_t Abc_SeqNodeDeleteFirst( Abc_Obj_t * pObj, int Edge )
{
Abc_SeqLat_t * pLat, * pRing, * pPrev, * pNext;
pRing = Abc_SeqNodeReadInit( pObj, Edge );
pLat = pRing; // consider the first latch
if ( pLat->pNext == pLat )
Abc_SeqNodeSetInit( pObj, Edge, NULL );
else
{
pPrev = Abc_SeqLatPrev( pLat );
pNext = Abc_SeqLatNext( pLat );
Abc_SeqLatSetPrev( pNext, pPrev );
Abc_SeqLatSetNext( pPrev, pNext );
Abc_SeqNodeSetInit( pObj, Edge, pNext ); // rotate the ring
}
Abc_SeqNodeRecycleLat( pObj, pLat );
}
// delete the last Lat on the edge
static inline Abc_InitType_t Abc_SeqNodeDeleteLast( Abc_Obj_t * pObj, int Edge )
{
Abc_SeqLat_t * pLat, * pRing, * pPrev, * pNext;
pRing = Abc_SeqNodeReadInit( pObj, Edge );
pLat = Abc_SeqLatPrev( pRing ); // consider the last latch
if ( pLat->pNext == pLat )
Abc_SeqNodeSetInit( pObj, Edge, NULL );
else
{
pPrev = Abc_SeqLatPrev( pLat );
pNext = Abc_SeqLatNext( pLat );
Abc_SeqLatSetPrev( pNext, pPrev );
Abc_SeqLatSetNext( pPrev, pNext );
}
Abc_SeqNodeRecycleLat( pObj, pLat );
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_SeqMan_t * Abc_SeqCreate( int nMaxId )
{
Abc_SeqMan_t * p;
// start the manager
p = ALLOC( Abc_SeqMan_t, 1 );
memset( p, 0, sizeof(Abc_SeqMan_t) );
p->nSize = nMaxId + 1;
// create internal data structures
p->vInits = Vec_PtrStart( 2 * p->nSize );
p->pMmInits = Extra_MmFixedStart( sizeof(Abc_SeqLat_t) );
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
...@@ -34,6 +34,7 @@ ...@@ -34,6 +34,7 @@
// the maximum number of latches on the edge // the maximum number of latches on the edge
#define ABC_MAX_EDGE_LATCH 16 #define ABC_MAX_EDGE_LATCH 16
#define ABC_FULL_MASK 0xFFFFFFFF
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// BASIC TYPES /// /// BASIC TYPES ///
......
...@@ -26,6 +26,7 @@ ...@@ -26,6 +26,7 @@
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandRead ( 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 IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
...@@ -34,6 +35,7 @@ static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv ); ...@@ -34,6 +35,7 @@ static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( 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 IoCommandReadTruth ( 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 IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
...@@ -60,6 +62,7 @@ static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv ); ...@@ -60,6 +62,7 @@ static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
void Io_Init( Abc_Frame_t * pAbc ) void Io_Init( Abc_Frame_t * pAbc )
{ {
Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 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_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
...@@ -68,6 +71,7 @@ void Io_Init( Abc_Frame_t * pAbc ) ...@@ -68,6 +71,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
...@@ -175,6 +179,79 @@ usage: ...@@ -175,6 +179,79 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
char * FileName;
FILE * pFile;
int fCheck;
int c;
fCheck = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
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" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
}
fclose( pFile );
// set the new network
pNtk = Io_ReadBaf( FileName, fCheck );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Reading network from BAF file has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_baf [-ch] <file>\n" );
fprintf( pAbc->Err, "\t read the network in Binary Aig Format (BAF)\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 IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv ) int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Abc_Ntk_t * pNtk, * pTemp; Abc_Ntk_t * pNtk, * pTemp;
...@@ -727,6 +804,65 @@ usage: ...@@ -727,6 +804,65 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
char * FileName;
int c;
util_getopt_reset();
while ( ( c = util_getopt( 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 != util_optind + 1 )
{
goto usage;
}
FileName = argv[util_optind];
// check the network type
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pAbc->Out, "Currently can only write strashed combinational AIGs.\n" );
return 0;
}
Io_WriteBaf( pNtk, FileName );
return 0;
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" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv ) int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
{ {
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
......
...@@ -47,6 +47,8 @@ ...@@ -47,6 +47,8 @@
/*=== abcRead.c ==========================================================*/ /*=== abcRead.c ==========================================================*/
extern Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ); extern Abc_Ntk_t * Io_Read( char * pFileName, int fCheck );
/*=== abcReadBaf.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck );
/*=== abcReadBlif.c ==========================================================*/ /*=== abcReadBlif.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ); extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
/*=== abcReadBench.c ==========================================================*/ /*=== abcReadBench.c ==========================================================*/
...@@ -67,6 +69,8 @@ extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, ...@@ -67,6 +69,8 @@ extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut,
extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 ); extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); 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 Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
/*=== abcWriteBaf.c ==========================================================*/
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/ /*=== abcWriteBlif.c ==========================================================*/
extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
......
...@@ -55,6 +55,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ) ...@@ -55,6 +55,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
pNtk = Io_ReadPla( pFileName, fCheck ); pNtk = Io_ReadPla( pFileName, fCheck );
else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) ) else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) )
pNtk = Io_ReadEqn( pFileName, fCheck ); pNtk = Io_ReadEqn( pFileName, fCheck );
else if ( Extra_FileNameCheckExtension( pFileName, "baf" ) )
return Io_ReadBaf( pFileName, fCheck );
else else
{ {
fprintf( stderr, "Unknown file format\n" ); fprintf( stderr, "Unknown file format\n" );
......
/**CFile****************************************************************
FileName [ioReadBaf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to read AIG in the binary format.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioReadBaf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the AIG in the binary format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
{
ProgressBar * pProgress;
FILE * pFile;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pNode0, * pNode1;
Abc_Ntk_t * pNtkNew;
int nInputs, nOutputs, nLatches, nAnds, nFileSize, Num, i;
char * pContents, * pName, * pCur;
unsigned * pBufferNode;
// 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 );
// skip the comments (comment lines begin with '#' and end with '\n')
for ( pCur = pContents; *pCur == '#'; )
while ( *pCur++ != '\n' );
// read the name
pName = pCur; while ( *pCur++ );
// read the number of inputs
nInputs = atoi( pCur ); while ( *pCur++ );
// read the number of outputs
nOutputs = atoi( pCur ); while ( *pCur++ );
// read the number of latches
nLatches = atoi( pCur ); while ( *pCur++ );
// read the number of nodes
nAnds = atoi( pCur ); while ( *pCur++ );
// allocate the empty AIG
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
pNtkNew->pName = util_strsav( pName );
pNtkNew->pSpec = util_strsav( pFileName );
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew->pManFunc) );
// create the PIs
for ( i = 0; i < nInputs; i++ )
{
pObj = Abc_NtkCreatePi(pNtkNew);
Abc_NtkLogicStoreName( pObj, pCur ); while ( *pCur++ );
Vec_PtrPush( vNodes, pObj );
}
// create the POs
for ( i = 0; i < nOutputs; i++ )
{
pObj = Abc_NtkCreatePo(pNtkNew);
Abc_NtkLogicStoreName( pObj, pCur ); while ( *pCur++ );
}
// create the latches
for ( i = 0; i < nLatches; i++ )
{
pObj = Abc_NtkCreateLatch(pNtkNew);
Abc_NtkLogicStoreName( pObj, pCur ); while ( *pCur++ );
Vec_PtrPush( vNodes, pObj );
Vec_PtrPush( pNtkNew->vCis, pObj );
Vec_PtrPush( pNtkNew->vCos, pObj );
}
// get the pointer to the beginning of the node array
pBufferNode = (int *)(pContents + (nFileSize - (2 * nAnds + nOutputs + nLatches) * sizeof(int)) );
// make sure we are at the place where the nodes begin
if ( pBufferNode != (int *)pCur )
{
free( pContents );
Vec_PtrFree( vNodes );
Abc_NtkDelete( pNtkNew );
printf( "Warning: Internal reader error.\n" );
return NULL;
}
// create the AND gates
pProgress = Extra_ProgressBarStart( stdout, nAnds );
for ( i = 0; i < nAnds; i++ )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, pBufferNode[2*i+0] >> 1), pBufferNode[2*i+0] & 1 );
pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, pBufferNode[2*i+1] >> 1), pBufferNode[2*i+1] & 1 );
Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
}
Extra_ProgressBarStop( pProgress );
// read the POs
Abc_NtkForEachCo( pNtkNew, pObj, i )
{
Num = pBufferNode[2*nAnds+i];
if ( Abc_ObjIsLatch(pObj) )
{
Abc_ObjSetData( pObj, (void *)(Num & 3) );
Num >>= 2;
}
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, Num >> 1), Num & 1 );
Abc_ObjAddFanin( pObj, pNode0 );
}
free( pContents );
Vec_PtrFree( vNodes );
// remove the extra nodes
Abc_AigCleanup( pNtkNew->pManFunc );
// check the result
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
{
printf( "Io_ReadBaf: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
/**CFile****************************************************************
FileName [ioWriteBaf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write AIG in the binary format.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioWriteBaf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*
Binary Aig Format
The motivation for this format is to have
- compact binary representation of large AIGs (~10x more compact than BLIF)
- consequently, fast reading/writing of large AIGs (~10x faster than BLIF)
- representation for all tech-ind info related to an AIG
- human-readable file header
The header:
(1) May contain several lines of human-readable comments.
Each comment line begins with symbol '#' and ends with symbol '\n'.
(2) Always contains the following data.
- benchmark name
- number of primary inputs
- number of primary outputs
- number of latches
- number of AIG nodes (excluding the constant 1 node)
Each entry is followed by 0-byte (character '\0'):
(3) Next follow the names of the PIs, POs, and latches in this order.
Each name is followed by 0-byte (character '\0').
Inside each set of names (PIs, POs, latches) there should be no
identical names but the PO names may coincide with PI/latch names.
The body:
(1) First part of the body contains binary information about the internal AIG nodes.
Each internal AIG node is represented using two 4-byte integers.
Each integer is the fanin ID followed by 1-bit representation of the complemented attribute.
(For example, complemented edge to node 10 will be represented as 2*10 + 1 = 21.)
The IDs of the nodes are created as follows: Constant 1 node has ID=0.
CIs (PIs and latch outputs) have 1-based IDs assigned in that order.
Each node in the array of the internal AIG nodes has the ID assigned in that order.
The constant 1 node is not written into the file.
(2) Second part of the body contains binary information about the edges connecting
the COs (POs and latch inputs) with the internal AIG nodes.
Each edge is represented by one 4-byte integer the same way as a node fanin.
*/
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the AIG in the binary format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName )
{
ProgressBar * pProgress;
FILE * pFile;
Abc_Obj_t * pObj;
int i, nNodes, nAnds, nBufferSize;
unsigned * pBufferNode;
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;
}
// write the comment
fprintf( pFile, "# BAF (Binary Aig Format) for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
// write the network name
fprintf( pFile, "%s%c", pNtk->pName, 0 );
// write the number of PIs
fprintf( pFile, "%d%c", Abc_NtkPiNum(pNtk), 0 );
// write the number of POs
fprintf( pFile, "%d%c", Abc_NtkPoNum(pNtk), 0 );
// write the number of latches
fprintf( pFile, "%d%c", Abc_NtkLatchNum(pNtk), 0 );
// write the number of internal nodes
fprintf( pFile, "%d%c", Abc_NtkNodeNum(pNtk), 0 );
// write PIs
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
// write POs
Abc_NtkForEachPo( pNtk, pObj, i )
fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
// write latches
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
// set the node numbers to be used in the output file
Abc_NtkCleanCopy( pNtk );
nNodes = 1;
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = (void *)nNodes++;
Abc_AigForEachAnd( pNtk, pObj, i )
pObj->pCopy = (void *)nNodes++;
// write the nodes into the buffer
nAnds = 0;
nBufferSize = Abc_NtkNodeNum(pNtk) * 2 + Abc_NtkCoNum(pNtk);
pBufferNode = ALLOC( int, nBufferSize );
pProgress = Extra_ProgressBarStart( stdout, nBufferSize );
Abc_AigForEachAnd( pNtk, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
pBufferNode[nAnds++] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
pBufferNode[nAnds++] = (((int)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj);
}
// write the COs into the buffer
Abc_NtkForEachCo( pNtk, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
pBufferNode[nAnds] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
if ( Abc_ObjIsLatch(pObj) )
pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((unsigned)Abc_ObjData(pObj) & 3);
nAnds++;
}
Extra_ProgressBarStop( pProgress );
assert( nBufferSize == nAnds );
// write the buffer
fwrite( pBufferNode, 1, sizeof(int) * nBufferSize, pFile );
fclose( pFile );
free( pBufferNode );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
SRC += src/base/io/io.c \ SRC += src/base/io/io.c \
src/base/io/ioRead.c \ src/base/io/ioRead.c \
src/base/io/ioReadBaf.c \
src/base/io/ioReadBench.c \ src/base/io/ioReadBench.c \
src/base/io/ioReadBlif.c \ src/base/io/ioReadBlif.c \
src/base/io/ioReadEdif.c \ src/base/io/ioReadEdif.c \
...@@ -7,6 +8,7 @@ SRC += src/base/io/io.c \ ...@@ -7,6 +8,7 @@ SRC += src/base/io/io.c \
src/base/io/ioReadPla.c \ src/base/io/ioReadPla.c \
src/base/io/ioReadVerilog.c \ src/base/io/ioReadVerilog.c \
src/base/io/ioUtil.c \ src/base/io/ioUtil.c \
src/base/io/ioWriteBaf.c \
src/base/io/ioWriteBench.c \ src/base/io/ioWriteBench.c \
src/base/io/ioWriteBlif.c \ src/base/io/ioWriteBlif.c \
src/base/io/ioWriteCnf.c \ src/base/io/ioWriteCnf.c \
......
...@@ -86,8 +86,8 @@ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString ...@@ -86,8 +86,8 @@ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString
return; return;
if ( nItemsCur > p->nItemsTotal ) if ( nItemsCur > p->nItemsTotal )
nItemsCur = p->nItemsTotal; nItemsCur = p->nItemsTotal;
p->posCur = (int)((float)nItemsCur * p->posTotal / p->nItemsTotal); p->posCur = (int)((double)nItemsCur * p->posTotal / p->nItemsTotal);
p->nItemsNext = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1; p->nItemsNext = (int)((double)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1;
if ( p->posCur == 0 ) if ( p->posCur == 0 )
p->posCur = 1; p->posCur = 1;
Extra_ProgressBarShow( p, pString ); Extra_ProgressBarShow( p, pString );
......
...@@ -125,6 +125,7 @@ p->timeStruct = clock() - clk; ...@@ -125,6 +125,7 @@ p->timeStruct = clock() - clk;
if ( fVerbose ) if ( fVerbose )
printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
// Sim_UtilCountPairsAllPrint( p );
Result = p->nPairsSymm; Result = p->nPairsSymm;
vResult = p->vMatrSymms; vResult = p->vMatrSymms;
......
...@@ -81,6 +81,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v ...@@ -81,6 +81,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v
// collect the results for the COs; // collect the results for the COs;
Abc_NtkForEachCo( pNtk, pTemp, i ) Abc_NtkForEachCo( pNtk, pTemp, i )
{ {
//printf( "Output %d:\n", i );
pTemp = Abc_ObjFanin0(pTemp); pTemp = Abc_ObjFanin0(pTemp);
if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) ) if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) )
continue; continue;
...@@ -444,6 +445,7 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, u ...@@ -444,6 +445,7 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, u
uSymm = (unsigned)vSymms->pArray[i]; uSymm = (unsigned)vSymms->pArray[i];
Ind1 = (uSymm & 0xffff); Ind1 = (uSymm & 0xffff);
Ind2 = (uSymm >> 16); Ind2 = (uSymm >> 16);
//printf( "%d,%d ", Ind1, Ind2 );
// skip variables that are not in the true support // skip variables that are not in the true support
assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) ); assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) ) if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
......
...@@ -612,6 +612,51 @@ int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport ) ...@@ -612,6 +612,51 @@ int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
{
int i, k, Index1, Index2;
Vec_IntForEachEntry( vSupport, i, Index1 )
Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
if ( Extra_BitMatrixLookup1( pMat, i, k ) )
printf( "(%d,%d) ", i, k );
return 0;
}
/**Function*************************************************************
Synopsis [Counts the number of entries in the array of matrices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sim_UtilCountPairsAllPrint( Sym_Man_t * p )
{
int i, clk;
clk = clock();
for ( i = 0; i < p->nOutputs; i++ )
{
printf( "Output %2d :", i );
Sim_UtilCountPairsOnePrint( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) );
printf( "\n" );
}
p->timeCount += clock() - clk;
}
/**Function*************************************************************
Synopsis [Counts the number of entries in the array of matrices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sim_UtilCountPairsAll( Sym_Man_t * p ) void Sim_UtilCountPairsAll( Sym_Man_t * p )
{ {
int nPairsTotal, nPairsSym, nPairsNonSym, i, clk; int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment