diff options
Diffstat (limited to 'src/aig/saig/saigIoa.c')
| -rw-r--r-- | src/aig/saig/saigIoa.c | 399 |
1 files changed, 399 insertions, 0 deletions
diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c new file mode 100644 index 00000000..70870fe9 --- /dev/null +++ b/src/aig/saig/saigIoa.c @@ -0,0 +1,399 @@ +/**CFile**************************************************************** + + FileName [saigIoa.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Input/output for sequential AIGs using BLIF files.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigIoa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + static char Buffer[16]; + if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) + sprintf( Buffer, "n%0*d", Aig_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) ); + else if ( Saig_ObjIsPi(p, pObj) ) + sprintf( Buffer, "pi%0*d", Aig_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) ); + else if ( Saig_ObjIsPo(p, pObj) ) + sprintf( Buffer, "po%0*d", Aig_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) ); + else if ( Saig_ObjIsLo(p, pObj) ) + sprintf( Buffer, "lo%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) ); + else if ( Saig_ObjIsLi(p, pObj) ) + sprintf( Buffer, "li%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) ); + else + assert( 0 ); + return Buffer; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) +{ + FILE * pFile; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i; + if ( Aig_ManPoNum(p) == 0 ) + { + printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); + return; + } + Aig_ManSetPioNumbers( p ); + // write input file + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" ); + return; + } + fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" ); + fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" ); + fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n", + Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p), + Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) ); + fprintf( pFile, ".model %s\n", p->pName ); + // write primary inputs + fprintf( pFile, ".inputs" ); + Aig_ManForEachPiSeq( p, pObj, i ) + fprintf( pFile, " %s", Saig_ObjName(p, pObj) ); + fprintf( pFile, "\n" ); + // write primary outputs + fprintf( pFile, ".outputs" ); + Aig_ManForEachPoSeq( p, pObj, i ) + fprintf( pFile, " %s", Saig_ObjName(p, pObj) ); + fprintf( pFile, "\n" ); + // write registers + if ( Aig_ManRegNum(p) ) + { + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + fprintf( pFile, ".latch" ); + fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) ); + fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) ); + fprintf( pFile, " 0\n" ); + } + } + // check if constant is used + if ( Aig_ObjRefs(Aig_ManConst1(p)) ) + fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) ); + // write the nodes in the DFS order + Aig_ManForEachNode( p, pObj, i ) + { + fprintf( pFile, ".names" ); + fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) ); + fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) ); + fprintf( pFile, " %s", Saig_ObjName(p, pObj) ); + fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) ); + } + // write the POs + Aig_ManForEachPo( p, pObj, i ) + { + fprintf( pFile, ".names" ); + fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) ); + fprintf( pFile, " %s", Saig_ObjName(p, pObj) ); + fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) ); + } + fprintf( pFile, ".end\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Reads one token from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Saig_ManReadToken( FILE * pFile ) +{ + static char Buffer[1000]; + if ( fscanf( pFile, "%s", Buffer ) == 1 ) + return Buffer; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Returns the corresponding number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManReadNumber( Aig_Man_t * p, char * pToken ) +{ + if ( pToken[0] == 'n' ) + return atoi( pToken + 1 ); + if ( pToken[0] == 'p' ) + return atoi( pToken + 2 ); + if ( pToken[0] == 'l' ) + return atoi( pToken + 2 ); + assert( 0 ); + return -1; +} + +/**Function************************************************************* + + Synopsis [Returns the corresponding node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken ) +{ + int Num; + if ( pToken[0] == 'n' ) + { + Num = atoi( pToken + 1 ); + return Aig_ManObj( p, pNum2Id[Num] ); + } + if ( pToken[0] == 'p' ) + { + pToken++; + if ( pToken[0] == 'i' ) + { + Num = atoi( pToken + 1 ); + return Aig_ManPi( p, Num ); + } + if ( pToken[0] == 'o' ) + return NULL; + assert( 0 ); + return NULL; + } + if ( pToken[0] == 'l' ) + { + pToken++; + if ( pToken[0] == 'o' ) + { + Num = atoi( pToken + 1 ); + return Saig_ManLo( p, Num ); + } + if ( pToken[0] == 'i' ) + return NULL; + assert( 0 ); + return NULL; + } + assert( 0 ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Reads BLIF previously dumped by Saig_ManDumpBlif().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManReadBlif( char * pFileName ) +{ + FILE * pFile; + Aig_Man_t * p; + Aig_Obj_t * pFanin0, * pFanin1, * pNode; + char * pToken; + int i, nPis, nPos, nRegs, Number; + int * pNum2Id = NULL; // mapping of node numbers in the file into AIG node IDs + // open the file + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" ); + return NULL; + } + // skip through the comments + for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; } + // get he model + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; } + // start the package + p = Aig_ManStart( 10000 ); + p->pName = Aig_UtilStrsav( pToken ); + p->pSpec = Aig_UtilStrsav( pFileName ); + // count PIs + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL || strcmp( pToken, ".inputs" ) ) + { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; } + for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ ); + // count POs + if ( pToken == NULL || strcmp( pToken, ".outputs" ) ) + { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; } + for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ ); + // count latches + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; } + for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ ) + { + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; } + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; } + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; } + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; } + } + // create PIs and LOs + for ( i = 0; i < nPis + nRegs; i++ ) + Aig_ObjCreatePi( p ); + Aig_ManSetRegNum( p, nRegs ); + // create nodes + for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ ) + { + // first token + pToken = Saig_ManReadToken( pFile ); + if ( i == 0 && pToken[0] == 'n' ) + { // constant node + // read 1 + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL || strcmp( pToken, "1" ) ) + { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; } + // read next + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; } + continue; + } + pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken ); + + // second token + pToken = Saig_ManReadToken( pFile ); + if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') ) + { // buffer + // read complemented attribute + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; } + if ( pToken[0] == '0' ) + pFanin0 = Aig_Not(pFanin0); + // read 1 + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL || strcmp( pToken, "1" ) ) + { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; } + Aig_ObjCreatePo( p, pFanin0 ); + // read next + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; } + continue; + } + + // third token + // regular node + pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken ); + pToken = Saig_ManReadToken( pFile ); + Number = Saig_ManReadNumber( p, pToken ); + // allocate mapping + if ( pNum2Id == NULL ) + { + extern double pow( double x, double y ); + int Size = (int)pow(10.0, (double)(strlen(pToken) - 1)); + pNum2Id = CALLOC( int, Size ); + } + + // other tokens + // get the complemented attributes + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; } + if ( pToken[0] == '0' ) + pFanin0 = Aig_Not(pFanin0); + if ( pToken[1] == '0' ) + pFanin1 = Aig_Not(pFanin1); + // read 1 + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL || strcmp( pToken, "1" ) ) + { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; } + // read next + pToken = Saig_ManReadToken( pFile ); + if ( pToken == NULL ) + { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; } + + // create new node + pNode = Aig_And( p, pFanin0, pFanin1 ); + if ( Aig_IsComplement(pNode) ) + { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; } + // set mapping + pNum2Id[ Number ] = pNode->Id; + } + if ( pToken == NULL || strcmp( pToken, ".end" ) ) + { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; } + if ( nPos + nRegs != Aig_ManPoNum(p) ) + { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; } + // add non-node objects to the mapping + Aig_ManForEachPi( p, pNode, i ) + pNum2Id[pNode->Id] = pNode->Id; +// FREE( pNum2Id ); + p->pData = pNum2Id; + // check the new manager + Aig_ManSetRegNum( p, nRegs ); + if ( !Aig_ManCheck(p) ) + printf( "Saig_ManReadBlif(): Check has failed.\n" ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |