#include "ver.h"

Macros
#define	VER_PARSE_SYM_OPEN '('
	DECLARATIONS ///. More...

#define	VER_PARSE_SYM_CLOSE ')'

#define	VER_PARSE_SYM_CONST0 '0'

#define	VER_PARSE_SYM_CONST1 '1'

#define	VER_PARSE_SYM_NEGBEF1 '!'

#define	VER_PARSE_SYM_NEGBEF2 '~'

#define	VER_PARSE_SYM_AND '&'

#define	VER_PARSE_SYM_OR '\|'

#define	VER_PARSE_SYM_XOR '^'

#define	VER_PARSE_SYM_MUX1 '?'

#define	VER_PARSE_SYM_MUX2 ':'

#define	VER_PARSE_OPER_NEG 7

#define	VER_PARSE_OPER_AND 6

#define	VER_PARSE_OPER_XOR 5

#define	VER_PARSE_OPER_OR 4

#define	VER_PARSE_OPER_EQU 3

#define	VER_PARSE_OPER_MUX 2

#define	VER_PARSE_OPER_MARK 1

#define	VER_PARSE_FLAG_START 1

#define	VER_PARSE_FLAG_VAR 2

#define	VER_PARSE_FLAG_OPER 3

#define	VER_PARSE_FLAG_ERROR 4

Functions
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)

void *	Ver_FormulaParser (char pFormula, void pMan, Vec_Ptr_t vNames, Vec_Ptr_t vStackFn, Vec_Int_t vStackOp, char pErrorMessage)
	FUNCTION DEFINITIONS ///. More...

void *	Ver_FormulaReduction (char pFormula, void pMan, Vec_Ptr_t vNames, char pErrorMessage)

Macro Definition Documentation

#define VER_PARSE_FLAG_ERROR 4

Definition at line 56 of file verFormula.c.

#define VER_PARSE_FLAG_OPER 3

Definition at line 55 of file verFormula.c.

#define VER_PARSE_FLAG_START 1

Definition at line 53 of file verFormula.c.

#define VER_PARSE_FLAG_VAR 2

Definition at line 54 of file verFormula.c.

#define VER_PARSE_OPER_AND 6

Definition at line 45 of file verFormula.c.

#define VER_PARSE_OPER_EQU 3

Definition at line 48 of file verFormula.c.

#define VER_PARSE_OPER_MARK 1

Definition at line 50 of file verFormula.c.

#define VER_PARSE_OPER_MUX 2

Definition at line 49 of file verFormula.c.

#define VER_PARSE_OPER_NEG 7

Definition at line 44 of file verFormula.c.

#define VER_PARSE_OPER_OR 4

Definition at line 47 of file verFormula.c.

#define VER_PARSE_OPER_XOR 5

Definition at line 46 of file verFormula.c.

#define VER_PARSE_SYM_AND '&'

Definition at line 37 of file verFormula.c.

#define VER_PARSE_SYM_CLOSE ')'

Definition at line 32 of file verFormula.c.

#define VER_PARSE_SYM_CONST0 '0'

Definition at line 33 of file verFormula.c.

#define VER_PARSE_SYM_CONST1 '1'

Definition at line 34 of file verFormula.c.

#define VER_PARSE_SYM_MUX1 '?'

Definition at line 40 of file verFormula.c.

#define VER_PARSE_SYM_MUX2 ':'

Definition at line 41 of file verFormula.c.

#define VER_PARSE_SYM_NEGBEF1 '!'

Definition at line 35 of file verFormula.c.

#define VER_PARSE_SYM_NEGBEF2 '~'

Definition at line 36 of file verFormula.c.

#define VER_PARSE_SYM_OPEN '('

DECLARATIONS ///.

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

]

Definition at line 31 of file verFormula.c.

#define VER_PARSE_SYM_OR '|'

Definition at line 38 of file verFormula.c.

#define VER_PARSE_SYM_XOR '^'

Definition at line 39 of file verFormula.c.

Function Documentation

void* Ver_FormulaParser	(	char *	pFormula,
		void *	pMan,
		Vec_Ptr_t *	vNames,
		Vec_Ptr_t *	vStackFn,
		Vec_Int_t *	vStackOp,
		char *	pErrorMessage
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Parser of the formula encountered in assign statements.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file verFormula.c.

 {
     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 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( (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 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)(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;
 }

int Ver_FormulaParserFindVar	(	char *	pString,
		Vec_Ptr_t *	vNames
	)

static

Function*************************************************************

Synopsis [Returns the index of the new variable found.]

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file verFormula.c.

 {
     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;
 }

Hop_Obj_t * Ver_FormulaParserTopOper	(	Hop_Man_t *	pMan,
		Vec_Ptr_t *	vStackFn,
		int	Oper
	)

static

Function*************************************************************

Synopsis [Performs the operation on the top entries in the stack.]

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file verFormula.c.

 {
     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;
 }

void* Ver_FormulaReduction	(	char *	pFormula,
		void *	pMan,
		Vec_Ptr_t *	vNames,
		char *	pErrorMessage
	)

Function*************************************************************

Synopsis [Returns the AIG representation of the reduction formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 435 of file verFormula.c.

 {
     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 );
 }

Macros

Functions

Macro Definition Documentation

Function Documentation