diff options
Diffstat (limited to 'src/base/ver/verFormula.c')
| -rw-r--r-- | src/base/ver/verFormula.c | 474 |
1 files changed, 0 insertions, 474 deletions
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c deleted file mode 100644 index 19a2c523..00000000 --- a/src/base/ver/verFormula.c +++ /dev/null @@ -1,474 +0,0 @@ -/**CFile**************************************************************** - - FileName [verFormula.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Verilog parser.] - - Synopsis [Formula parser to read Verilog assign statements.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - August 19, 2006.] - - Revision [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ver.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// the list of operation symbols to be used in expressions -#define VER_PARSE_SYM_OPEN '(' // opening paranthesis -#define VER_PARSE_SYM_CLOSE ')' // closing paranthesis -#define VER_PARSE_SYM_CONST0 '0' // constant 0 -#define VER_PARSE_SYM_CONST1 '1' // constant 1 -#define VER_PARSE_SYM_NEGBEF1 '!' // negation before the variable -#define VER_PARSE_SYM_NEGBEF2 '~' // negation before the variable -#define VER_PARSE_SYM_AND '&' // logic AND -#define VER_PARSE_SYM_OR '|' // logic OR -#define VER_PARSE_SYM_XOR '^' // logic XOR -#define VER_PARSE_SYM_MUX1 '?' // first symbol of MUX -#define VER_PARSE_SYM_MUX2 ':' // second symbol of MUX - -// the list of opcodes (also specifying operation precedence) -#define VER_PARSE_OPER_NEG 7 // negation (highest precedence) -#define VER_PARSE_OPER_AND 6 // logic AND -#define VER_PARSE_OPER_XOR 5 // logic EXOR (a'b | ab') -#define VER_PARSE_OPER_OR 4 // logic OR -#define VER_PARSE_OPER_EQU 3 // equvalence (a'b'| ab ) -#define VER_PARSE_OPER_MUX 2 // MUX(a,b,c) (ab | a'c ) -#define VER_PARSE_OPER_MARK 1 // OpStack token standing for an opening paranthesis - -// these are values of the internal Flag -#define VER_PARSE_FLAG_START 1 // after the opening parenthesis -#define VER_PARSE_FLAG_VAR 2 // after operation is received -#define VER_PARSE_FLAG_OPER 3 // after operation symbol is received -#define VER_PARSE_FLAG_ERROR 4 // when error is detected - -static Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper ); -static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Parser of the formula encountered in assign statements.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ) -{ - char * pTemp; - Hop_Obj_t * bFunc, * bTemp; - int nParans, Flag; - int Oper, Oper1, Oper2; - int v; - - // clear the stacks and the names - Vec_PtrClear( vNames ); - Vec_PtrClear( vStackFn ); - Vec_IntClear( vStackOp ); - - if ( !strcmp(pFormula, "0") || !strcmp(pFormula, "1\'b0") ) - return Hop_ManConst0(pMan); - if ( !strcmp(pFormula, "1") || !strcmp(pFormula, "1\'b1") ) - return Hop_ManConst1(pMan); - - // make sure that the number of opening and closing parantheses is the same - nParans = 0; - for ( pTemp = pFormula; *pTemp; pTemp++ ) - if ( *pTemp == '(' ) - nParans++; - else if ( *pTemp == ')' ) - nParans--; - if ( nParans != 0 ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parantheses ()." ); - return NULL; - } - - // add parantheses - pTemp = pFormula + strlen(pFormula) + 2; - *pTemp-- = 0; *pTemp = ')'; - while ( --pTemp != pFormula ) - *pTemp = *(pTemp - 1); - *pTemp = '('; - - // perform parsing - Flag = VER_PARSE_FLAG_START; - for ( pTemp = pFormula; *pTemp; pTemp++ ) - { - switch ( *pTemp ) - { - // skip all spaces, tabs, and end-of-lines - case ' ': - case '\t': - case '\r': - case '\n': - continue; -/* - // treat Constant 0 as a variable - case VER_PARSE_SYM_CONST0: - Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) ); // Cudd_Ref( Hop_ManConst0(pMan) ); - if ( Flag == VER_PARSE_FLAG_VAR ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - Flag = VER_PARSE_FLAG_VAR; - break; - - // the same for Constant 1 - case VER_PARSE_SYM_CONST1: - Vec_PtrPush( vStackFn, Hop_ManConst1(pMan) ); // Cudd_Ref( Hop_ManConst1(pMan) ); - if ( Flag == VER_PARSE_FLAG_VAR ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - Flag = VER_PARSE_FLAG_VAR; - break; -*/ - case VER_PARSE_SYM_NEGBEF1: - case VER_PARSE_SYM_NEGBEF2: - if ( Flag == VER_PARSE_FLAG_VAR ) - {// if NEGBEF follows a variable, AND is assumed - sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG ); - break; - - case VER_PARSE_SYM_AND: - case VER_PARSE_SYM_OR: - case VER_PARSE_SYM_XOR: - case VER_PARSE_SYM_MUX1: - case VER_PARSE_SYM_MUX2: - if ( Flag != VER_PARSE_FLAG_VAR ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - if ( *pTemp == VER_PARSE_SYM_AND ) - Vec_IntPush( vStackOp, VER_PARSE_OPER_AND ); - else if ( *pTemp == VER_PARSE_SYM_OR ) - Vec_IntPush( vStackOp, VER_PARSE_OPER_OR ); - else if ( *pTemp == VER_PARSE_SYM_XOR ) - Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR ); - else if ( *pTemp == VER_PARSE_SYM_MUX1 ) - Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX ); -// else if ( *pTemp == VER_PARSE_SYM_MUX2 ) -// Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX ); - Flag = VER_PARSE_FLAG_OPER; - break; - - case VER_PARSE_SYM_OPEN: - if ( Flag == VER_PARSE_FLAG_VAR ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a paranthesis." ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK ); - // after an opening bracket, it feels like starting over again - Flag = VER_PARSE_FLAG_START; - break; - - case VER_PARSE_SYM_CLOSE: - if ( Vec_IntSize( vStackOp ) ) - { - while ( 1 ) - { - if ( !Vec_IntSize( vStackOp ) ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - Oper = Vec_IntPop( vStackOp ); - if ( Oper == VER_PARSE_OPER_MARK ) - break; - // skip the second MUX operation -// if ( Oper == VER_PARSE_OPER_MUX2 ) -// { -// Oper = Vec_IntPop( vStackOp ); -// assert( Oper == VER_PARSE_OPER_MUX1 ); -// } - - // perform the given operation - if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper ) == NULL ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" ); - return NULL; - } - } - } - else - { - sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" ); - Flag = VER_PARSE_FLAG_ERROR; - break; - } - if ( Flag != VER_PARSE_FLAG_ERROR ) - Flag = VER_PARSE_FLAG_VAR; - break; - - - default: - // scan the next name - v = Ver_FormulaParserFindVar( pTemp, vNames ); - if ( *pTemp == '\\' ) - pTemp++; - pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1; - - // assume operation AND, if vars follow one another - if ( Flag == VER_PARSE_FLAG_VAR ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." ); - return NULL; - } - bTemp = Hop_IthVar( pMan, v ); - Vec_PtrPush( vStackFn, bTemp ); // Cudd_Ref( bTemp ); - Flag = VER_PARSE_FLAG_VAR; - break; - } - - if ( Flag == VER_PARSE_FLAG_ERROR ) - break; // error exit - else if ( Flag == VER_PARSE_FLAG_START ) - continue; // go on parsing - else if ( Flag == VER_PARSE_FLAG_VAR ) - while ( 1 ) - { // check if there are negations in the OpStack - if ( !Vec_IntSize(vStackOp) ) - break; - Oper = Vec_IntPop( vStackOp ); - if ( Oper != VER_PARSE_OPER_NEG ) - { - Vec_IntPush( vStackOp, Oper ); - break; - } - else - { -// Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) ); - Vec_PtrPush( vStackFn, Hop_Not(Vec_PtrPop(vStackFn)) ); - } - } - else // if ( Flag == VER_PARSE_FLAG_OPER ) - while ( 1 ) - { // execute all the operations in the OpStack - // with precedence higher or equal than the last one - Oper1 = Vec_IntPop( vStackOp ); // the last operation - if ( !Vec_IntSize(vStackOp) ) - { // if it is the only operation, push it back - Vec_IntPush( vStackOp, Oper1 ); - break; - } - Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one - if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) ) - { // if Oper2 precedence is higher or equal, execute it - if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL ) - { - sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" ); - return NULL; - } - Vec_IntPush( vStackOp, Oper1 ); // push the last operation back - } - else - { // if Oper2 precedence is lower, push them back and done - Vec_IntPush( vStackOp, Oper2 ); - Vec_IntPush( vStackOp, Oper1 ); - break; - } - } - } - - if ( Flag != VER_PARSE_FLAG_ERROR ) - { - if ( Vec_PtrSize(vStackFn) ) - { - bFunc = Vec_PtrPop(vStackFn); - if ( !Vec_PtrSize(vStackFn) ) - if ( !Vec_IntSize(vStackOp) ) - { -// Cudd_Deref( bFunc ); - return bFunc; - } - else - sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" ); - else - sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" ); - } - else - sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" ); - } -// Cudd_Ref( bFunc ); -// Cudd_RecursiveDeref( dd, bFunc ); - return NULL; -} - -/**Function************************************************************* - - Synopsis [Performs the operation on the top entries in the stack.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper ) -{ - Hop_Obj_t * bArg0, * bArg1, * bArg2, * bFunc; - // perform the given operation - bArg2 = Vec_PtrPop( vStackFn ); - bArg1 = Vec_PtrPop( vStackFn ); - if ( Oper == VER_PARSE_OPER_AND ) - bFunc = Hop_And( pMan, bArg1, bArg2 ); - else if ( Oper == VER_PARSE_OPER_XOR ) - bFunc = Hop_Exor( pMan, bArg1, bArg2 ); - else if ( Oper == VER_PARSE_OPER_OR ) - bFunc = Hop_Or( pMan, bArg1, bArg2 ); - else if ( Oper == VER_PARSE_OPER_EQU ) - bFunc = Hop_Not( Hop_Exor( pMan, bArg1, bArg2 ) ); - else if ( Oper == VER_PARSE_OPER_MUX ) - { - bArg0 = Vec_PtrPop( vStackFn ); -// bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 ); Cudd_Ref( bFunc ); - bFunc = Hop_Mux( pMan, bArg0, bArg1, bArg2 ); -// Cudd_RecursiveDeref( dd, bArg0 ); -// Cudd_Deref( bFunc ); - } - else - return NULL; -// Cudd_Ref( bFunc ); -// Cudd_RecursiveDeref( dd, bArg1 ); -// Cudd_RecursiveDeref( dd, bArg2 ); - Vec_PtrPush( vStackFn, bFunc ); - return bFunc; -} - -/**Function************************************************************* - - Synopsis [Returns the index of the new variable found.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ) -{ - char * pTemp, * pTemp2; - int nLength, nLength2, i; - // start the string - pTemp = pString; - // find the end of the string delimited by other characters - if ( *pTemp == '\\' ) - { - pString++; - while ( *pTemp && *pTemp != ' ' ) - pTemp++; - } - else - { - while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && - *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && - *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && - *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && - *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 ) - pTemp++; - } - // look for this string in the array - nLength = pTemp - pString; - for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ ) - { - nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 ); - if ( nLength2 != nLength ) - continue; - pTemp2 = Vec_PtrEntry( vNames, 2*i + 1 ); - if ( strncmp( pString, pTemp2, nLength ) ) - continue; - return i; - } - // could not find - add and return the number - Vec_PtrPush( vNames, (void *)nLength ); - Vec_PtrPush( vNames, pString ); - return i; -} - -/**Function************************************************************* - - Synopsis [Returns the AIG representation of the reduction formula.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage ) -{ - Hop_Obj_t * pRes; - int v, fCompl; - char Symbol; - - // get the operation - Symbol = *pFormula++; - fCompl = ( Symbol == '~' ); - if ( fCompl ) - Symbol = *pFormula++; - // check the operation - if ( Symbol != '&' && Symbol != '|' && Symbol != '^' ) - { - sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol ); - return NULL; - } - // skip the brace - while ( *pFormula++ != '{' ); - // parse the names - Vec_PtrClear( vNames ); - while ( *pFormula != '}' ) - { - v = Ver_FormulaParserFindVar( pFormula, vNames ); - pFormula += (int)Vec_PtrEntry( vNames, 2*v ); - while ( *pFormula == ' ' || *pFormula == ',' ) - pFormula++; - } - // compute the function - if ( Symbol == '&' ) - pRes = Hop_CreateAnd( pMan, Vec_PtrSize(vNames)/2 ); - else if ( Symbol == '|' ) - pRes = Hop_CreateOr( pMan, Vec_PtrSize(vNames)/2 ); - else if ( Symbol == '^' ) - pRes = Hop_CreateExor( pMan, Vec_PtrSize(vNames)/2 ); - return Hop_NotCond( pRes, fCompl ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |