From 44550a67fa60534cef92bfc7b2f0f07d9b18b09a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 30 Sep 2016 19:55:21 -0700 Subject: Bug fix in the SMT parser to address multi-argument operators and large constants. --- src/base/wlc/wlcReadSmt.c | 297 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 295 insertions(+), 2 deletions(-) (limited to 'src/base/wlc/wlcReadSmt.c') diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 580401df..0791154a 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -136,7 +136,7 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) 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) + Type = WLC_OBJ_SHIFT_RA , *pfSigned = 1; // 10: shift right (arithmetic) else if ( !strcmp(pName, "bvshl") ) Type = WLC_OBJ_SHIFT_L; // 11: shift left // else if ( !strcmp(pName, "") ) @@ -266,7 +266,7 @@ static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int SeeAlso [] ***********************************************************************/ -static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) +static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) { char Buffer[100]; int NameId, fFound; @@ -290,6 +290,286 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in assert( iObj == NameId ); return iObj; } +static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) +{ + char Buffer[100]; + char * pNameFanin; + int NameId, fFound, old_size, new_size; + int iObj, iFanin0, iFanin1; + Vec_Int_t * v2Fanins = Vec_IntStartFull(2); + + assert( Type > 0 ); + assert( Range >= 0 ); + assert( fSigned >= 0 ); + + // allow more than 2 fanins for specific operators + // if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX ) + // explicitely secify allowed multi operators + if (Vec_IntSize(vFanins)<=2 || + !( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND + Type == WLC_OBJ_BIT_OR || // 17: bitwise OR + Type == WLC_OBJ_BIT_XOR || // 18: bitwise XOR + Type == WLC_OBJ_BIT_NAND || // 19: bitwise AND + Type == WLC_OBJ_BIT_NOR || // 20: bitwise OR + Type == WLC_OBJ_BIT_NXOR || // 21: bitwise NXOR + + Type == WLC_OBJ_LOGIC_IMPL || // 27: logic implication + Type == WLC_OBJ_LOGIC_AND || // 28: logic AND + Type == WLC_OBJ_LOGIC_OR || // 29: logic OR + Type == WLC_OBJ_LOGIC_XOR || // 30: logic XOR + Type == WLC_OBJ_COMP_EQU || // 31: compare equal + Type == WLC_OBJ_COMP_NOTEQU || // 32: compare not equal + Type == WLC_OBJ_COMP_LESS || // 33: compare less + Type == WLC_OBJ_COMP_MORE || // 34: compare more + Type == WLC_OBJ_COMP_LESSEQU || // 35: compare less or equal + Type == WLC_OBJ_COMP_MOREEQU || // 36: compare more or equal + + Type == WLC_OBJ_ARI_ADD || // 43: arithmetic addition + Type == WLC_OBJ_ARI_SUB || // 44: arithmetic subtraction + Type == WLC_OBJ_ARI_MULTI || // 45: arithmetic multiplier + Type == WLC_OBJ_ARI_DIVIDE // 46: arithmetic division + )) + goto FINISHED_WITH_FANINS; + + // we will be creating nodes backwards. this way we can pop from vFanins easier + while (Vec_IntSize(vFanins)>2) + { + // getting 2 fanins at a time + old_size = Vec_IntSize(vFanins); + iFanin0 = Vec_IntPop(vFanins); + iFanin1 = Vec_IntPop(vFanins); + + Vec_IntWriteEntry(v2Fanins,0,iFanin0); + Vec_IntWriteEntry(v2Fanins,1,iFanin1); + + iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 ); + sprintf( Buffer, "_n%d_", iObj ); + pNameFanin = Buffer; + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); + + assert( !fFound ); + assert( iObj == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), v2Fanins ); + + // pushing the new node + Vec_IntPush(vFanins, iObj); + new_size = Vec_IntSize(vFanins); + assert(new_size=2); + if (range1>32) + { + Vec_Int_t * newFanins = Vec_IntAlloc(10); + Vec_IntPush(newFanins,iFanin1); + Vec_IntPushTwo( newFanins, 30, 0 ); + + iObj1 = Wlc_ObjAlloc( pNtk, WLC_OBJ_BIT_SELECT, 0, 30, 0 ); + sprintf( Buffer, "_n%d_", iObj1 ); + pNameFanin = Buffer; + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); + + assert( !fFound ); + assert( iObj1 == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins ); + + // bit select of larger bits + Vec_IntPop(newFanins); + Vec_IntPop(newFanins); + Vec_IntPushTwo( newFanins, range1-1, 31 ); + iObj2 = Wlc_ObjAlloc( pNtk, WLC_OBJ_BIT_SELECT, 0, range1-1, 31 ); + sprintf( Buffer, "_n%d_", iObj2 ); + pNameFanin = Buffer; + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); + + assert( !fFound ); + assert( iObj2 == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins ); + + // reduction or + Vec_IntPop( newFanins ); + Vec_IntPop( newFanins ); + Vec_IntWriteEntry( newFanins, 0, iObj2 ); + iObj3 = Wlc_ObjAlloc( pNtk, WLC_OBJ_REDUCT_OR, 0, 0, 0 ); + sprintf( Buffer, "_n%d_", iObj3 ); + pNameFanin = Buffer; + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); + + assert( !fFound ); + assert( iObj3 == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins ); + + // concat all together + Vec_IntWriteEntry( newFanins, 0, iObj3 ); + Vec_IntPush( newFanins, iObj1 ); + iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_BIT_CONCAT, 0, 31, 0 ); + sprintf( Buffer, "_n%d_", iObj ); + pNameFanin = Buffer; + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); + + assert( !fFound ); + assert( iObj == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins ); + + // pushing the new node + Vec_IntWriteEntry(vFanins, 1, iObj); + Vec_IntFree(newFanins); + } + } + + iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 ); + + // add node's name + if ( pName == NULL ) + { + sprintf( Buffer, "_n%d_", iObj ); + pName = Buffer; + } + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + if ( fSigned ) + { + Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; +// if ( Vec_IntSize(vFanins) > 0 ) +// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; +// if ( Vec_IntSize(vFanins) > 1 ) +// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned; + } + + return iObj; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline char * Smt_GetHexFromDecimalString(char * pStr) +{ + int i,k=0, nDigits = strlen(pStr); + int digit, carry = 0; + int metNonZeroBit; + int nBits; + char * hex; + + Vec_Int_t * decimal = Vec_IntAlloc(nDigits); + Vec_Int_t * rev; + + for (i=0;i=nDigits) + { + if (!metNonZeroBit) + break; + else + { + Vec_IntPush(rev,carry); + carry = 0; + k = 0; + metNonZeroBit = 0; + } + } + continue; + } + + if (!metNonZeroBit) + metNonZeroBit = 1; + + digit = carry*10 + digit; + carry = digit%2; + digit = digit / 2; + Vec_IntWriteEntry(decimal,k,digit); + + k++; + if (k>=nDigits) + { + Vec_IntPush(rev,carry); + carry = 0; + k = 0; + metNonZeroBit = 0; + } + } + + Vec_IntFree(decimal); + + if (!Vec_IntSize(rev)) + Vec_IntPush(rev,0); + + while (Vec_IntSize(rev)%4) + Vec_IntPush(rev,0); + + nBits = Vec_IntSize(rev); + hex = (char *)malloc((nBits/4+1)*sizeof(char)); + + for (k=0;k= '0' && pStr[0] <= '9' ) { + /* int w, nWords, Number = atoi( pStr ); if ( nBits == -1 ) { @@ -307,6 +588,16 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits nWords = Abc_BitWordNum( nBits ); for ( w = 0; w < nWords; w++ ) Vec_IntPush( vFanins, w ? 0 : Number ); + */ + + // convert decimal to hex to parse large constants + char * pHex = Smt_GetHexFromDecimalString(pStr); + + if ( nBits == -1 ) + nBits = strlen(pHex)*4; + + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex ); } else { @@ -836,6 +1127,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 ); if ( iObj ) return iObj; + Type0 = Smt_StrToType( pStr0, &fSigned ); if ( Type0 == 0 ) return 0; @@ -853,6 +1145,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, } Vec_IntPush( vFanins, iObj ); } + // find range Range = 0; if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR ) -- cgit v1.2.3