diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abcs/abcSeqMan.c | 218 | ||||
| -rw-r--r-- | src/base/abcs/abcs.h | 1 | ||||
| -rw-r--r-- | src/base/io/io.c | 136 | ||||
| -rw-r--r-- | src/base/io/io.h | 4 | ||||
| -rw-r--r-- | src/base/io/ioRead.c | 2 | ||||
| -rw-r--r-- | src/base/io/ioReadBaf.c | 164 | ||||
| -rw-r--r-- | src/base/io/ioWriteBaf.c | 163 | ||||
| -rw-r--r-- | src/base/io/module.make | 2 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilProgress.c | 4 | ||||
| -rw-r--r-- | src/opt/sim/simSym.c | 1 | ||||
| -rw-r--r-- | src/opt/sim/simSymStr.c | 2 | ||||
| -rw-r--r-- | src/opt/sim/simUtils.c | 45 |
12 files changed, 740 insertions, 2 deletions
diff --git a/src/base/abcs/abcSeqMan.c b/src/base/abcs/abcSeqMan.c new file mode 100644 index 00000000..b5db4bef --- /dev/null +++ b/src/base/abcs/abcSeqMan.c @@ -0,0 +1,218 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h index e250d929..fd0bc4c9 100644 --- a/src/base/abcs/abcs.h +++ b/src/base/abcs/abcs.h @@ -34,6 +34,7 @@ // the maximum number of latches on the edge #define ABC_MAX_EDGE_LATCH 16 +#define ABC_FULL_MASK 0xFFFFFFFF //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// diff --git a/src/base/io/io.c b/src/base/io/io.c index bffdfc10..bf71e72d 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 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 ); 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 ); static int IoCommandReadPla ( 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 IoCommandWriteBench ( 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 ); void Io_Init( Abc_Frame_t * pAbc ) { 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_bench", IoCommandReadBench, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); @@ -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_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_bench", IoCommandWriteBench, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); @@ -175,6 +179,79 @@ usage: 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 ) { Abc_Ntk_t * pNtk, * pTemp; @@ -727,6 +804,65 @@ usage: 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 ) { Abc_Ntk_t * pNtk; diff --git a/src/base/io/io.h b/src/base/io/io.h index a5aae529..8551a714 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -47,6 +47,8 @@ /*=== abcRead.c ==========================================================*/ extern Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ); +/*=== abcReadBaf.c ==========================================================*/ +extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ); /*=== abcReadBlif.c ==========================================================*/ extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ); /*=== abcReadBench.c ==========================================================*/ @@ -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_ReadCreateInv( 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 ==========================================================*/ extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c index acf4deda..28500a3d 100644 --- a/src/base/io/ioRead.c +++ b/src/base/io/ioRead.c @@ -55,6 +55,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ) pNtk = Io_ReadPla( pFileName, fCheck ); else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) ) pNtk = Io_ReadEqn( pFileName, fCheck ); + else if ( Extra_FileNameCheckExtension( pFileName, "baf" ) ) + return Io_ReadBaf( pFileName, fCheck ); else { fprintf( stderr, "Unknown file format\n" ); diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c new file mode 100644 index 00000000..7783373f --- /dev/null +++ b/src/base/io/ioReadBaf.c @@ -0,0 +1,164 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c new file mode 100644 index 00000000..3ecd8e73 --- /dev/null +++ b/src/base/io/ioWriteBaf.c @@ -0,0 +1,163 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/io/module.make b/src/base/io/module.make index 34582473..9938af12 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/ioReadBaf.c \ src/base/io/ioReadBench.c \ src/base/io/ioReadBlif.c \ src/base/io/ioReadEdif.c \ @@ -7,6 +8,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/ioWriteBaf.c \ src/base/io/ioWriteBench.c \ src/base/io/ioWriteBlif.c \ src/base/io/ioWriteCnf.c \ diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c index 7b0efb5c..b8d7c8a8 100644 --- a/src/misc/extra/extraUtilProgress.c +++ b/src/misc/extra/extraUtilProgress.c @@ -86,8 +86,8 @@ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString return; if ( nItemsCur > p->nItemsTotal ) nItemsCur = p->nItemsTotal; - p->posCur = (int)((float)nItemsCur * p->posTotal / p->nItemsTotal); - p->nItemsNext = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1; + p->posCur = (int)((double)nItemsCur * p->posTotal / p->nItemsTotal); + p->nItemsNext = (int)((double)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1; if ( p->posCur == 0 ) p->posCur = 1; Extra_ProgressBarShow( p, pString ); diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c index 93e0426e..0635526e 100644 --- a/src/opt/sim/simSym.c +++ b/src/opt/sim/simSym.c @@ -125,6 +125,7 @@ p->timeStruct = clock() - clk; if ( fVerbose ) printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); +// Sim_UtilCountPairsAllPrint( p ); Result = p->nPairsSymm; vResult = p->vMatrSymms; diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c index ed7e93bf..c909d986 100644 --- a/src/opt/sim/simSymStr.c +++ b/src/opt/sim/simSymStr.c @@ -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; Abc_NtkForEachCo( pNtk, pTemp, i ) { +//printf( "Output %d:\n", i ); pTemp = Abc_ObjFanin0(pTemp); if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) ) continue; @@ -444,6 +445,7 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, u uSymm = (unsigned)vSymms->pArray[i]; Ind1 = (uSymm & 0xffff); Ind2 = (uSymm >> 16); +//printf( "%d,%d ", Ind1, Ind2 ); // skip variables that are not in the true support assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) ); if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) ) diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c index 6a3a911b..31baaec8 100644 --- a/src/opt/sim/simUtils.c +++ b/src/opt/sim/simUtils.c @@ -612,6 +612,51 @@ int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport ) 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 ) { int nPairsTotal, nPairsSym, nPairsNonSym, i, clk; |