diff options
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/module.make | 1 | ||||
-rw-r--r-- | src/base/wlc/wlc.h | 6 | ||||
-rw-r--r-- | src/base/wlc/wlcCom.c | 32 | ||||
-rw-r--r-- | src/base/wlc/wlcNtk.c | 2 | ||||
-rw-r--r-- | src/base/wlc/wlcReadSmt.c | 681 | ||||
-rw-r--r-- | src/base/wlc/wlcReadVer.c | 31 |
6 files changed, 725 insertions, 28 deletions
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make index 84cc7620..717444d0 100644 --- a/src/base/wlc/module.make +++ b/src/base/wlc/module.make @@ -2,5 +2,6 @@ SRC += src/base/wlc/wlcAbs.c \ src/base/wlc/wlcBlast.c \ src/base/wlc/wlcCom.c \ src/base/wlc/wlcNtk.c \ + src/base/wlc/wlcReadSmt.c \ src/base/wlc/wlcReadVer.c \ src/base/wlc/wlcWriteVer.c diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 3b7c9153..5954ec18 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -252,9 +252,11 @@ extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ); extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); -/*=== wlcReadWord.c ========================================================*/ +/*=== wlcReadSmt.c ========================================================*/ +extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ); +/*=== wlcReadVer.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName ); -/*=== wlcWriteWord.c ========================================================*/ +/*=== wlcWriteVer.c ========================================================*/ extern void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 68373522..88c91c51 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -28,8 +28,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_CommandReadVer ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandWriteVer ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -55,8 +55,8 @@ static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ******************************************************************************/ void Wlc_Init( Abc_Frame_t * pAbc ) { - Cmd_CommandAdd( pAbc, "Word level", "%read_ver", Abc_CommandReadVer, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%write_ver", Abc_CommandWriteVer, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); @@ -90,7 +90,7 @@ void Wlc_End( Abc_Frame_t * pAbc ) SeeAlso [] ******************************************************************************/ -int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pFile; Wlc_Ntk_t * pNtk = NULL; @@ -112,7 +112,7 @@ int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc != globalUtilOptind + 1 ) { - printf( "Abc_CommandReadVer(): Input file name should be given on the command line.\n" ); + printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" ); return 0; } // get the file name @@ -120,7 +120,7 @@ int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( pFileName, "r" )) == NULL ) { Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName ); - if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".smt", NULL, NULL, NULL )) ) + if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".smt", ".smt2", NULL, NULL )) ) Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); Abc_Print( 1, "\n" ); return 0; @@ -128,11 +128,19 @@ int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv ) fclose( pFile ); // perform reading - pNtk = Wlc_ReadVer( pFileName ); + if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) + pNtk = Wlc_ReadVer( pFileName ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" ) ) + pNtk = Wlc_ReadSmt( pFileName ); + else + { + printf( "Abc_CommandReadWlc(): Unknown file extension.\n" ); + return 0; + } Wlc_AbcUpdateNtk( pAbc, pNtk ); return 0; usage: - Abc_Print( -2, "usage: %%read_ver [-vh] <file_name>\n" ); + Abc_Print( -2, "usage: %%read [-vh] <file_name>\n" ); Abc_Print( -2, "\t reads word-level design from Verilog file\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -150,7 +158,7 @@ usage: SeeAlso [] ******************************************************************************/ -int Abc_CommandWriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); char * pFileName = NULL; @@ -171,7 +179,7 @@ int Abc_CommandWriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pNtk == NULL ) { - Abc_Print( 1, "Abc_CommandWriteVer(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandWriteWlc(): There is no current design.\n" ); return 0; } if ( argc == globalUtilOptind ) @@ -186,7 +194,7 @@ int Abc_CommandWriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_WriteVer( pNtk, pFileName ); return 0; usage: - Abc_Print( -2, "usage: %%write_ver [-vh]\n" ); + Abc_Print( -2, "usage: %%write [-vh]\n" ); Abc_Print( -2, "\t writes the design into a file\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 90287781..8c09467e 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -471,7 +471,9 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ) Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins ); Wlc_NtkForEachCo( p, pObj, i ) Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi ); + if ( p->vInits ) pNew->vInits = Vec_IntDup( p->vInits ); + if ( p->pInits ) pNew->pInits = Abc_UtilStrsav( p->pInits ); Vec_IntFree( vFanins ); return pNew; diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c new file mode 100644 index 00000000..35d3ed87 --- /dev/null +++ b/src/base/wlc/wlcReadSmt.c @@ -0,0 +1,681 @@ +/**CFile**************************************************************** + + FileName [wlcReadSmt.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Parses several flavors of word-level Verilog.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcReadSmt.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// parser name types +typedef enum { + PRS_SMT_NONE = 0, + PRS_SMT_INPUT, + PRS_SMT_CONST, + PRS_SMT_LET, + PRS_SMT_ASSERT +} Prs_ManType_t; + +// parser +typedef struct Prs_Smt_t_ Prs_Smt_t; +struct Prs_Smt_t_ +{ + // input data + char * pName; // file name + char * pBuffer; // file contents + char * pLimit; // end of file + char * pCur; // current position + Abc_Nam_t * pStrs; // string manager + // network structure + Vec_Int_t vData; + // error handling + char ErrorStr[1000]; +}; + + +// create error message +static inline int Prs_SmtErrorSet( Prs_Smt_t * p, char * pError, int Value ) +{ + assert( !p->ErrorStr[0] ); + sprintf( p->ErrorStr, "%s", pError ); + return Value; +} +// clear error message +static inline void Prs_SmtErrorClear( Prs_Smt_t * p ) +{ + p->ErrorStr[0] = '\0'; +} +// print error message +static inline int Prs_SmtErrorPrint( Prs_Smt_t * p ) +{ + char * pThis; int iLine = 0; + if ( !p->ErrorStr[0] ) return 1; + for ( pThis = p->pBuffer; pThis < p->pCur; pThis++ ) + iLine += (int)(*pThis == '\n'); + printf( "Line %d: %s\n", iLine, p->ErrorStr ); + return 0; +} +static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit ) +{ + char * pBuffer; + int nFileSize, RetValue; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open input file.\n" ); + return NULL; + } + // get the file size, in bytes + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + // move the file current reading position to the beginning + rewind( pFile ); + // load the contents of the file into memory + pBuffer = ABC_ALLOC( char, nFileSize + 3 ); + pBuffer[0] = '\n'; + RetValue = fread( pBuffer+1, nFileSize, 1, pFile ); + // terminate the string with '\0' + pBuffer[nFileSize + 0] = '\n'; + pBuffer[nFileSize + 1] = '\0'; + *ppLimit = pBuffer + nFileSize + 2; + return pBuffer; +} +static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName ) +{ + Prs_Smt_t * p; + char * pBuffer, * pLimit; + pBuffer = Prs_SmtLoadFile( pFileName, &pLimit ); + if ( pBuffer == NULL ) + return NULL; + p = ABC_CALLOC( Prs_Smt_t, 1 ); + p->pName = pFileName; + p->pBuffer = pBuffer; + p->pLimit = pLimit; + p->pCur = pBuffer; + p->pStrs = Abc_NamStart( 1000, 24 ); + Vec_IntGrow ( &p->vData, 1000 ); + return p; +} + +static inline void Prs_SmtFree( Prs_Smt_t * p ) +{ + if ( p->pStrs ) + Abc_NamDeref( p->pStrs ); + Vec_IntErase( &p->vData ); + ABC_FREE( p->pBuffer ); + ABC_FREE( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Prs_SmtRemoveComments( Prs_Smt_t * p ) +{ + char * pTemp; + for ( pTemp = p->pBuffer; pTemp < p->pLimit; pTemp++ ) + if ( *pTemp == ';' ) + while ( *pTemp && *pTemp != '\n' ) + *pTemp++ = ' '; +} +static inline void Prs_SmtSkipSpaces( Prs_Smt_t * p ) +{ + while ( *p->pCur == ' ' || *p->pCur == '\t' || *p->pCur == '\r' || *p->pCur == '\n' ) + p->pCur++; +} +static inline int Prs_SmtIsWord( Prs_Smt_t * p, char * pWord ) +{ + Prs_SmtSkipSpaces( p ); + if ( strncmp( p->pCur, pWord, strlen(pWord) ) ) + return 0; + p->pCur += strlen(pWord); + Prs_SmtSkipSpaces( p ); + return 1; +} +static inline char * Prs_SmtFindNextPar( Prs_Smt_t * p ) +{ + char * pTemp; int Count = 1; + for ( pTemp = p->pCur; pTemp < p->pLimit; pTemp++ ) + { + if ( *pTemp == '(' ) + Count++; + else if ( *pTemp == ')' ) + Count--; + if ( Count == 0 ) + break; + } + assert( *pTemp == ')' ); + return pTemp; +} +static inline int Prs_SmtParseLet( Prs_Smt_t * p, char * pLimit, int Type ) +{ + char * pToken; + assert( *pLimit == ')' ); + *pLimit = 0; + Vec_IntPush( &p->vData, 0 ); + Vec_IntPush( &p->vData, Type ); + pToken = strtok( p->pCur, " ()" ); + while ( pToken ) + { + if ( pToken[0] != '_' && pToken[0] != '=' ) + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + } + assert( *pLimit == 0 ); + *pLimit = ')'; + p->pCur = pLimit; + return 1; +} +static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type ) +{ + char * pToken; + assert( *pLimit == ')' ); + *pLimit = 0; + Vec_IntPush( &p->vData, 0 ); + Vec_IntPush( &p->vData, Type ); + pToken = strtok( p->pCur, " ()" ); + assert( pToken != NULL ); + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + if ( pToken[0] == '_' ) + pToken = strtok( NULL, " ()" ); + if ( !strcmp(pToken, "Bool") ) + { + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "1", NULL) ); + pToken = strtok( NULL, " ()" ); + if ( !strcmp(pToken, "false") ) + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b0", NULL) ); + else if ( !strcmp(pToken, "true") ) + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b1", NULL) ); + else assert( 0 ); + } + else if ( !strcmp(pToken, "BitVec") ) + { + pToken = strtok( NULL, " ()" ); + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + if ( pToken ) + { + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + if ( pToken != NULL ) + return Prs_SmtErrorSet(p, "Trailing symbols are not recognized.", 0); + } + } + else + return Prs_SmtErrorSet(p, "Expecting either \"Bool\" or \"BitVec\".", 0); + assert( *pLimit == 0 ); + *pLimit = ')'; + p->pCur = pLimit; + return 1; +} +int Prs_SmtReadLines( Prs_Smt_t * p ) +{ + Prs_SmtSkipSpaces( p ); + while ( *p->pCur == '(' ) + { + p->pCur++; + if ( Prs_SmtIsWord(p, "let") ) + { + assert( *p->pCur == '(' ); + p->pCur++; + if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_LET ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; + } + else if ( Prs_SmtIsWord(p, "declare-fun") ) + { + if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_INPUT ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; + } + else if ( Prs_SmtIsWord(p, "define-fun") ) + { + if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_CONST ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; + } + else if ( Prs_SmtIsWord(p, "check-sat") ) + { + Vec_IntPush( &p->vData, 0 ); + return 1; + } + else if ( Prs_SmtIsWord(p, "assert") ) + {} + else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") ) + p->pCur = Prs_SmtFindNextPar(p) + 1; + else + break; + //return Prs_SmtErrorSet(p, "Unsupported directive.", 0); + Prs_SmtSkipSpaces( p ); + } + // finish parsing assert + if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) ) + return 0; + assert( *p->pCur == ')' ); + Vec_IntPush( &p->vData, 0 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prs_SmtPrintParser( Prs_Smt_t * p ) +{ + int Entry, i; + Vec_IntForEachEntry( &p->vData, Entry, i ) + { + if ( Entry == 0 ) + { + printf( "\n" ); + if ( i == Vec_IntSize(&p->vData) - 1 ) + break; + Entry = Vec_IntEntry(&p->vData, ++i); + if ( Entry == PRS_SMT_INPUT ) + printf( "declare-fun" ); + else if ( Entry == PRS_SMT_CONST ) + printf( "define-fun" ); + else if ( Entry == PRS_SMT_LET ) + printf( "let" ); + else if ( Entry == PRS_SMT_ASSERT ) + printf( "assert" ); + else assert(0); + continue; + } + printf( " %s", Abc_NamStr(p->pStrs, Entry) ); + } +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Prs_SmtReadConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins, char * pName ) +{ + char Buffer[100]; + int i, nDigits, iObj, NameId, fFound; + Vec_IntClear( vFanins ); + if ( pStr[0] != '#' ) + { + // handle decimal number + int Number = atoi( pStr ); + nBits = Abc_Base2Log( Number+1 ); + assert( nBits < 32 ); + Vec_IntPush( vFanins, Number ); + } + else if ( pStr[1] == 'b' ) + { + if ( nBits == -1 ) + nBits = strlen(pStr+2); + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + for ( i = 0; i < nBits; i++ ) + if ( pStr[2+i] == '1' ) + Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i ); + else if ( pStr[2+i] != '0' ) + return 0; + } + else if ( pStr[1] == 'x' ) + { + if ( nBits == -1 ) + nBits = strlen(pStr+2)*4; + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 ); + if ( nDigits != (nBits + 3)/4 ) + assert( 0 ); + } + else return 0; + // create constant node + iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_CONST, 0, nBits-1, 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + // add node's name + if ( pName == NULL ) + { + sprintf( Buffer, "_c%d_", iObj ); + pName = Buffer; + } + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + return NameId; +} +static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins ) +{ + if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' ) + { + Vec_Int_t * vTemp = Vec_IntAlloc(0); + int NameId = Prs_SmtReadConstant( pNtk, pStr, nBits, vTemp, NULL ); + Vec_IntFree( vTemp ); + if ( !NameId ) + return 0; + Vec_IntPush( vFanins, NameId ); + return 1; + } + else + { + // read name + int fFound, NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); + assert( fFound ); + Vec_IntPush( vFanins, NameId ); + return 1; + } +} +static inline int Prs_SmtStrToType( char * pName ) +{ + int Type = 0; + if ( !strcmp(pName, "ite") ) + Type = WLC_OBJ_MUX; // 08: multiplexer + else if ( !strcmp(pName, "bvlshr") ) + Type = WLC_OBJ_SHIFT_R; // 09: shift right + else if ( !strcmp(pName, "bvashr") ) + Type = WLC_OBJ_SHIFT_RA; // 10: shift right (arithmetic) + else if ( !strcmp(pName, "bvshl") ) + Type = WLC_OBJ_SHIFT_L; // 11: shift left +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_SHIFT_LA; // 12: shift left (arithmetic) + else if ( !strcmp(pName, "rotate_right") ) + Type = WLC_OBJ_ROTATE_R; // 13: rotate right + else if ( !strcmp(pName, "rotate_left") ) + Type = WLC_OBJ_ROTATE_L; // 14: rotate left + else if ( !strcmp(pName, "bvnot") ) + Type = WLC_OBJ_BIT_NOT; // 15: bitwise NOT + else if ( !strcmp(pName, "bvand") ) + Type = WLC_OBJ_BIT_AND; // 16: bitwise AND + else if ( !strcmp(pName, "bvor") ) + Type = WLC_OBJ_BIT_OR; // 17: bitwise OR + else if ( !strcmp(pName, "bvxor") ) + Type = WLC_OBJ_BIT_XOR; // 18: bitwise XOR + else if ( !strcmp(pName, "extract") ) + Type = WLC_OBJ_BIT_SELECT; // 19: bit selection + else if ( !strcmp(pName, "concat") ) + Type = WLC_OBJ_BIT_CONCAT; // 20: bit concatenation + else if ( !strcmp(pName, "zero_extend") ) + Type = WLC_OBJ_BIT_ZEROPAD; // 21: zero padding + else if ( !strcmp(pName, "sign_extend") ) + Type = WLC_OBJ_BIT_SIGNEXT; // 22: sign extension + else if ( !strcmp(pName, "not") ) + Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT + else if ( !strcmp(pName, "and") ) + Type = WLC_OBJ_LOGIC_AND; // 24: logic AND + else if ( !strcmp(pName, "or") ) + Type = WLC_OBJ_LOGIC_OR; // 25: logic OR + else if ( !strcmp(pName, "bvcomp") ) + Type = WLC_OBJ_COMP_EQU; // 26: compare equal +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_COMP_NOTEQU; // 27: compare not equal + else if ( !strcmp(pName, "bvult") ) + Type = WLC_OBJ_COMP_LESS; // 28: compare less + else if ( !strcmp(pName, "bvugt") ) + Type = WLC_OBJ_COMP_MORE; // 29: compare more + else if ( !strcmp(pName, "bvule") ) + Type = WLC_OBJ_COMP_LESSEQU; // 30: compare less or equal + else if ( !strcmp(pName, "bvuge") ) + Type = WLC_OBJ_COMP_MOREEQU; // 31: compare more or equal + else if ( !strcmp(pName, "bvredand") ) + Type = WLC_OBJ_REDUCT_AND; // 32: reduction AND + else if ( !strcmp(pName, "bvredor") ) + Type = WLC_OBJ_REDUCT_OR; // 33: reduction OR + else if ( !strcmp(pName, "bvredxor") ) + Type = WLC_OBJ_REDUCT_XOR; // 34: reduction XOR + else if ( !strcmp(pName, "bvadd") ) + Type = WLC_OBJ_ARI_ADD; // 35: arithmetic addition + else if ( !strcmp(pName, "bvsub") ) + Type = WLC_OBJ_ARI_SUB; // 36: arithmetic subtraction + else if ( !strcmp(pName, "bvmul") ) + Type = WLC_OBJ_ARI_MULTI; // 37: arithmetic multiplier + else if ( !strcmp(pName, "bvdiv") ) + Type = WLC_OBJ_ARI_DIVIDE; // 38: arithmetic division + else if ( !strcmp(pName, "bvurem") ) + Type = WLC_OBJ_ARI_MODULUS; // 39: arithmetic modulus +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_ARI_POWER; // 40: arithmetic power + else if ( !strcmp(pName, "bvneg") ) + Type = WLC_OBJ_ARI_MINUS; // 41: arithmetic minus +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_TABLE; // 42: bit table + else assert( 0 ); + return Type; +} +static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange ) +{ + int Type, NameId; + char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) ); + // read type + Type = Prs_SmtStrToType( pName ); + if ( Type == 0 ) + return 0; + *pRange = 0; + Vec_IntClear( vFanins ); + if ( Type == WLC_OBJ_COMP_EQU ) + { + *pRange = 1; + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + return WLC_OBJ_COMP_EQU; + } + else if ( Type == WLC_OBJ_LOGIC_NOT ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + if ( !strcmp(pName, "bvcomp") ) + { + *pRange = 1; + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + return WLC_OBJ_COMP_NOTEQU; // 26: compare equal + } + i--; + } + else if ( Type == WLC_OBJ_BIT_SELECT ) + { + int End, Beg; + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + End = atoi( pName ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + Beg = atoi( pName ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + Prs_SmtReadName( pNtk, pName, -1, vFanins ); + Vec_IntPush( vFanins, (End << 16) | Beg ); + *pRange = End - Beg + 1; + return WLC_OBJ_BIT_SELECT; + } + while ( Vec_IntEntry(vData, ++i) ) + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, i)), -1, vFanins ); + if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L ) + { + int * pArray = Vec_IntArray(vFanins); + assert( Vec_IntSize(vFanins) == 2 ); + ABC_SWAP( int, pArray[0], pArray[1] ); + } + if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR ) + *pRange = 1; + else if ( Type == WLC_OBJ_BIT_CONCAT ) + { + int k; + Vec_IntForEachEntry( vFanins, NameId, k ) + *pRange += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + else if ( Type == WLC_OBJ_MUX ) + { + int * pArray = Vec_IntArray(vFanins); + assert( Vec_IntSize(vFanins) == 3 ); + ABC_SWAP( int, pArray[1], pArray[2] ); + NameId = Vec_IntEntry(vFanins, 1); + *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + else // to determine range, look at the first argument + { + NameId = Vec_IntEntry(vFanins, 0); + *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + return Type; +} +Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) +{ + Wlc_Ntk_t * pNtk; + char * pName, * pBits, * pConst; + Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); + int i, iObj, Type, Entry, NameId, fFound, Range; + // start network and create primary inputs + pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); + pNtk->pManName = Abc_NamStart( 1000, 24 ); + for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) + { + assert( Vec_IntEntry(&p->vData, i) == 0 ); + if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, atoi(pBits)-1, 0 ); + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + } + while ( Vec_IntEntry(&p->vData, ++i) ); + } + // create logic nodes + for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) + { + assert( Vec_IntEntry(&p->vData, i) == 0 ); + Entry = Vec_IntEntry(&p->vData, ++i); + if ( Entry == PRS_SMT_INPUT ) + {} + else if ( Entry == PRS_SMT_CONST ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + pConst = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + // create new node + if ( !Prs_SmtReadConstant( pNtk, pConst, atoi(pBits), vFanins, pName ) ) + return NULL; + } + else if ( Entry == PRS_SMT_LET ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range ); + if ( Type == WLC_OBJ_NONE ) + return NULL; + assert( Range > 0 ); + // create new node + iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + // add node's name + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + } + else if ( Entry == PRS_SMT_ASSERT ) + { + Type = WLC_OBJ_BUF; + Vec_IntClear( vFanins ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + if ( !strcmp(pName, "not") ) + { + Type = WLC_OBJ_LOGIC_NOT; + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + Range = 1; + } + // add fanin + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( fFound ); + Vec_IntPush( vFanins, NameId ); + // find range + if ( Type == WLC_OBJ_BUF ) + { + // find range + iObj = Vec_IntEntry(vFanins, 0); + Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); + assert( Range == 1 ); + } + // create new node + iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 ); + // add node's name + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, "miter_output", &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + break; + } + else assert( 0 ); + while ( Vec_IntEntry(&p->vData, ++i) ); + } + Vec_IntFree( vFanins ); + // create nameIDs + vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); + Vec_IntAppend( &pNtk->vNameIds, vFanins ); + Vec_IntFree( vFanins ); + return pNtk; +} +Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) +{ + Wlc_Ntk_t * pNtk = NULL; + Prs_Smt_t * p = Prs_SmtAlloc( pFileName ); + if ( p == NULL ) + return NULL; + Prs_SmtRemoveComments( p ); + Prs_SmtReadLines( p ); + //Prs_SmtPrintParser( p ); + if ( Prs_SmtErrorPrint(p) ) + { + pNtk = Prs_SmtBuild( p ); + } + Prs_SmtFree( p ); + return pNtk; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index 8ed33909..11d14395 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -547,7 +547,7 @@ static inline char * Wlc_PrsReadConstant( Wlc_Prs_t * p, char * pStr, Vec_Int_t Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); for ( i = 0; i < nBits; i++ ) if ( pStr[2+i] == '1' ) - Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), i ); + Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i ); else if ( pStr[2+i] != '0' ) return (char *)(ABC_PTRINT_T)Wlc_PrsWriteErrorMessage( p, pStr, "Wrong digit in binary constant \"%c\".", pStr[2+i] ); *pRange = nBits; @@ -922,19 +922,22 @@ startword: Vec_Int_t * vTemp = Vec_IntStartNatural( Wlc_NtkObjNumMax(p->pNtk) ); Vec_IntAppend( &p->pNtk->vNameIds, vTemp ); Vec_IntFree( vTemp ); - // move FO/FI to be part of CI/CO - assert( (Vec_IntSize(&p->pNtk->vFfs) & 1) == 0 ); - assert( Vec_IntSize(&p->pNtk->vFfs) == 2 * Vec_IntSize(p->pNtk->vInits) ); - Wlc_NtkForEachFf( p->pNtk, pObj, i ) - if ( i & 1 ) - Wlc_ObjSetCo( p->pNtk, pObj, 1 ); - else - Wlc_ObjSetCi( p->pNtk, pObj ); - Vec_IntClear( &p->pNtk->vFfs ); - // convert init values into binary string - //Vec_IntPrint( &p->pNtk->vInits ); - p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk ); - //printf( "%s", p->pNtk->pInits ); + if ( p->pNtk->vInits ) + { + // move FO/FI to be part of CI/CO + assert( (Vec_IntSize(&p->pNtk->vFfs) & 1) == 0 ); + assert( Vec_IntSize(&p->pNtk->vFfs) == 2 * Vec_IntSize(p->pNtk->vInits) ); + Wlc_NtkForEachFf( p->pNtk, pObj, i ) + if ( i & 1 ) + Wlc_ObjSetCo( p->pNtk, pObj, 1 ); + else + Wlc_ObjSetCi( p->pNtk, pObj ); + Vec_IntClear( &p->pNtk->vFfs ); + // convert init values into binary string + //Vec_IntPrint( &p->pNtk->vInits ); + p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk ); + //printf( "%s", p->pNtk->pInits ); + } break; } // these are read as part of the interface |