abcBridge-0.14: abc-build/src/base/ver/verFormula.c
/**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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// the list of operation symbols to be used in expressions
#define VER_PARSE_SYM_OPEN '(' // opening parenthesis
#define VER_PARSE_SYM_CLOSE ')' // closing parenthesis
#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 parenthesis
// 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((Hop_Man_t *)pMan);
if ( !strcmp(pFormula, "1") || !strcmp(pFormula, "1\'b1") )
return Hop_ManConst1((Hop_Man_t *)pMan);
// make sure that the number of opening and closing parentheses 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 parentheses ()." );
return NULL;
}
// add parentheses
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 parenthesis." );
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 parenthesis\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( (Hop_Man_t *)pMan, vStackFn, Oper ) == NULL )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
return NULL;
}
}
}
else
{
sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening parenthesis\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)(ABC_PTRUINT_T)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( (Hop_Man_t *)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((Hop_Obj_t *)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( (Hop_Man_t *)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 = (Hop_Obj_t *)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 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
bArg1 = (Hop_Obj_t *)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 = (Hop_Obj_t *)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)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*i + 0 );
if ( nLength2 != nLength )
continue;
pTemp2 = (char *)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 *)(ABC_PTRUINT_T)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 = NULL;
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)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*v );
while ( *pFormula == ' ' || *pFormula == ',' )
pFormula++;
}
// compute the function
if ( Symbol == '&' )
pRes = Hop_CreateAnd( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
else if ( Symbol == '|' )
pRes = Hop_CreateOr( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
else if ( Symbol == '^' )
pRes = Hop_CreateExor( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
return Hop_NotCond( pRes, fCompl );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END