ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
verFormula.c File Reference
#include "ver.h"
Include dependency graph for verFormula.c:

Go to the source code of this file.

Macros

#define VER_PARSE_SYM_OPEN   '('
 DECLARATIONS ///.
 
#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

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

Macro Definition Documentation

◆ VER_PARSE_FLAG_ERROR

#define VER_PARSE_FLAG_ERROR   4

Definition at line 56 of file verFormula.c.

◆ VER_PARSE_FLAG_OPER

#define VER_PARSE_FLAG_OPER   3

Definition at line 55 of file verFormula.c.

◆ VER_PARSE_FLAG_START

#define VER_PARSE_FLAG_START   1

Definition at line 53 of file verFormula.c.

◆ VER_PARSE_FLAG_VAR

#define VER_PARSE_FLAG_VAR   2

Definition at line 54 of file verFormula.c.

◆ VER_PARSE_OPER_AND

#define VER_PARSE_OPER_AND   6

Definition at line 45 of file verFormula.c.

◆ VER_PARSE_OPER_EQU

#define VER_PARSE_OPER_EQU   3

Definition at line 48 of file verFormula.c.

◆ VER_PARSE_OPER_MARK

#define VER_PARSE_OPER_MARK   1

Definition at line 50 of file verFormula.c.

◆ VER_PARSE_OPER_MUX

#define VER_PARSE_OPER_MUX   2

Definition at line 49 of file verFormula.c.

◆ VER_PARSE_OPER_NEG

#define VER_PARSE_OPER_NEG   7

Definition at line 44 of file verFormula.c.

◆ VER_PARSE_OPER_OR

#define VER_PARSE_OPER_OR   4

Definition at line 47 of file verFormula.c.

◆ VER_PARSE_OPER_XOR

#define VER_PARSE_OPER_XOR   5

Definition at line 46 of file verFormula.c.

◆ VER_PARSE_SYM_AND

#define VER_PARSE_SYM_AND   '&'

Definition at line 37 of file verFormula.c.

◆ VER_PARSE_SYM_CLOSE

#define VER_PARSE_SYM_CLOSE   ')'

Definition at line 32 of file verFormula.c.

◆ VER_PARSE_SYM_CONST0

#define VER_PARSE_SYM_CONST0   '0'

Definition at line 33 of file verFormula.c.

◆ VER_PARSE_SYM_CONST1

#define VER_PARSE_SYM_CONST1   '1'

Definition at line 34 of file verFormula.c.

◆ VER_PARSE_SYM_MUX1

#define VER_PARSE_SYM_MUX1   '?'

Definition at line 40 of file verFormula.c.

◆ VER_PARSE_SYM_MUX2

#define VER_PARSE_SYM_MUX2   ':'

Definition at line 41 of file verFormula.c.

◆ VER_PARSE_SYM_NEGBEF1

#define VER_PARSE_SYM_NEGBEF1   '!'

Definition at line 35 of file verFormula.c.

◆ VER_PARSE_SYM_NEGBEF2

#define VER_PARSE_SYM_NEGBEF2   '~'

Definition at line 36 of file verFormula.c.

◆ VER_PARSE_SYM_OPEN

#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.

◆ VER_PARSE_SYM_OR

#define VER_PARSE_SYM_OR   '|'

Definition at line 38 of file verFormula.c.

◆ VER_PARSE_SYM_XOR

#define VER_PARSE_SYM_XOR   '^'

Definition at line 39 of file verFormula.c.

Function Documentation

◆ Ver_FormulaParser()

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.

77{
78 char * pTemp;
79 Hop_Obj_t * bFunc, * bTemp;
80 int nParans, Flag;
81 int Oper, Oper1, Oper2;
82 int v;
83
84 // clear the stacks and the names
85 Vec_PtrClear( vNames );
86 Vec_PtrClear( vStackFn );
87 Vec_IntClear( vStackOp );
88
89 if ( !strcmp(pFormula, "0") || !strcmp(pFormula, "1\'b0") )
90 return Hop_ManConst0((Hop_Man_t *)pMan);
91 if ( !strcmp(pFormula, "1") || !strcmp(pFormula, "1\'b1") )
92 return Hop_ManConst1((Hop_Man_t *)pMan);
93
94 // make sure that the number of opening and closing parentheses is the same
95 nParans = 0;
96 for ( pTemp = pFormula; *pTemp; pTemp++ )
97 if ( *pTemp == '(' )
98 nParans++;
99 else if ( *pTemp == ')' )
100 nParans--;
101 if ( nParans != 0 )
102 {
103 sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parentheses ()." );
104 return NULL;
105 }
106
107 // add parentheses
108 pTemp = pFormula + strlen(pFormula) + 2;
109 *pTemp-- = 0; *pTemp = ')';
110 while ( --pTemp != pFormula )
111 *pTemp = *(pTemp - 1);
112 *pTemp = '(';
113
114 // perform parsing
115 Flag = VER_PARSE_FLAG_START;
116 for ( pTemp = pFormula; *pTemp; pTemp++ )
117 {
118 switch ( *pTemp )
119 {
120 // skip all spaces, tabs, and end-of-lines
121 case ' ':
122 case '\t':
123 case '\r':
124 case '\n':
125 continue;
126/*
127 // treat Constant 0 as a variable
128 case VER_PARSE_SYM_CONST0:
129 Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) ); // Cudd_Ref( Hop_ManConst0(pMan) );
130 if ( Flag == VER_PARSE_FLAG_VAR )
131 {
132 sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." );
133 Flag = VER_PARSE_FLAG_ERROR;
134 break;
135 }
136 Flag = VER_PARSE_FLAG_VAR;
137 break;
138
139 // the same for Constant 1
140 case VER_PARSE_SYM_CONST1:
141 Vec_PtrPush( vStackFn, Hop_ManConst1(pMan) ); // Cudd_Ref( Hop_ManConst1(pMan) );
142 if ( Flag == VER_PARSE_FLAG_VAR )
143 {
144 sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." );
145 Flag = VER_PARSE_FLAG_ERROR;
146 break;
147 }
148 Flag = VER_PARSE_FLAG_VAR;
149 break;
150*/
151 case VER_PARSE_SYM_NEGBEF1:
152 case VER_PARSE_SYM_NEGBEF2:
153 if ( Flag == VER_PARSE_FLAG_VAR )
154 {// if NEGBEF follows a variable, AND is assumed
155 sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." );
156 Flag = VER_PARSE_FLAG_ERROR;
157 break;
158 }
159 Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG );
160 break;
161
162 case VER_PARSE_SYM_AND:
163 case VER_PARSE_SYM_OR:
164 case VER_PARSE_SYM_XOR:
165 case VER_PARSE_SYM_MUX1:
166 case VER_PARSE_SYM_MUX2:
167 if ( Flag != VER_PARSE_FLAG_VAR )
168 {
169 sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." );
170 Flag = VER_PARSE_FLAG_ERROR;
171 break;
172 }
173 if ( *pTemp == VER_PARSE_SYM_AND )
174 Vec_IntPush( vStackOp, VER_PARSE_OPER_AND );
175 else if ( *pTemp == VER_PARSE_SYM_OR )
176 Vec_IntPush( vStackOp, VER_PARSE_OPER_OR );
177 else if ( *pTemp == VER_PARSE_SYM_XOR )
178 Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR );
179 else if ( *pTemp == VER_PARSE_SYM_MUX1 )
180 Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
181// else if ( *pTemp == VER_PARSE_SYM_MUX2 )
182// Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
183 Flag = VER_PARSE_FLAG_OPER;
184 break;
185
186 case VER_PARSE_SYM_OPEN:
187 if ( Flag == VER_PARSE_FLAG_VAR )
188 {
189 sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a parenthesis." );
190 Flag = VER_PARSE_FLAG_ERROR;
191 break;
192 }
193 Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK );
194 // after an opening bracket, it feels like starting over again
195 Flag = VER_PARSE_FLAG_START;
196 break;
197
198 case VER_PARSE_SYM_CLOSE:
199 if ( Vec_IntSize( vStackOp ) )
200 {
201 while ( 1 )
202 {
203 if ( !Vec_IntSize( vStackOp ) )
204 {
205 sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening parenthesis\n" );
206 Flag = VER_PARSE_FLAG_ERROR;
207 break;
208 }
209 Oper = Vec_IntPop( vStackOp );
210 if ( Oper == VER_PARSE_OPER_MARK )
211 break;
212 // skip the second MUX operation
213// if ( Oper == VER_PARSE_OPER_MUX2 )
214// {
215// Oper = Vec_IntPop( vStackOp );
216// assert( Oper == VER_PARSE_OPER_MUX1 );
217// }
218
219 // perform the given operation
220 if ( Ver_FormulaParserTopOper( (Hop_Man_t *)pMan, vStackFn, Oper ) == NULL )
221 {
222 sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
223 return NULL;
224 }
225 }
226 }
227 else
228 {
229 sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening parenthesis\n" );
230 Flag = VER_PARSE_FLAG_ERROR;
231 break;
232 }
233 if ( Flag != VER_PARSE_FLAG_ERROR )
234 Flag = VER_PARSE_FLAG_VAR;
235 break;
236
237
238 default:
239 // scan the next name
240 v = Ver_FormulaParserFindVar( pTemp, vNames );
241 if ( *pTemp == '\\' )
242 pTemp++;
243 pTemp += (int)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*v ) - 1;
244
245 // assume operation AND, if vars follow one another
246 if ( Flag == VER_PARSE_FLAG_VAR )
247 {
248 sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." );
249 return NULL;
250 }
251 bTemp = Hop_IthVar( (Hop_Man_t *)pMan, v );
252 Vec_PtrPush( vStackFn, bTemp ); // Cudd_Ref( bTemp );
253 Flag = VER_PARSE_FLAG_VAR;
254 break;
255 }
256
257 if ( Flag == VER_PARSE_FLAG_ERROR )
258 break; // error exit
259 else if ( Flag == VER_PARSE_FLAG_START )
260 continue; // go on parsing
261 else if ( Flag == VER_PARSE_FLAG_VAR )
262 while ( 1 )
263 { // check if there are negations in the OpStack
264 if ( !Vec_IntSize(vStackOp) )
265 break;
266 Oper = Vec_IntPop( vStackOp );
267 if ( Oper != VER_PARSE_OPER_NEG )
268 {
269 Vec_IntPush( vStackOp, Oper );
270 break;
271 }
272 else
273 {
274// Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) );
275 Vec_PtrPush( vStackFn, Hop_Not((Hop_Obj_t *)Vec_PtrPop(vStackFn)) );
276 }
277 }
278 else // if ( Flag == VER_PARSE_FLAG_OPER )
279 while ( 1 )
280 { // execute all the operations in the OpStack
281 // with precedence higher or equal than the last one
282 Oper1 = Vec_IntPop( vStackOp ); // the last operation
283 if ( !Vec_IntSize(vStackOp) )
284 { // if it is the only operation, push it back
285 Vec_IntPush( vStackOp, Oper1 );
286 break;
287 }
288 Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
289 if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) )
290 { // if Oper2 precedence is higher or equal, execute it
291 if ( Ver_FormulaParserTopOper( (Hop_Man_t *)pMan, vStackFn, Oper2 ) == NULL )
292 {
293 sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
294 return NULL;
295 }
296 Vec_IntPush( vStackOp, Oper1 ); // push the last operation back
297 }
298 else
299 { // if Oper2 precedence is lower, push them back and done
300 Vec_IntPush( vStackOp, Oper2 );
301 Vec_IntPush( vStackOp, Oper1 );
302 break;
303 }
304 }
305 }
306
307 if ( Flag != VER_PARSE_FLAG_ERROR )
308 {
309 if ( Vec_PtrSize(vStackFn) )
310 {
311 bFunc = (Hop_Obj_t *)Vec_PtrPop(vStackFn);
312 if ( !Vec_PtrSize(vStackFn) )
313 if ( !Vec_IntSize(vStackOp) )
314 {
315// Cudd_Deref( bFunc );
316 return bFunc;
317 }
318 else
319 sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" );
320 else
321 sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" );
322 }
323 else
324 sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" );
325 }
326// Cudd_Ref( bFunc );
327// Cudd_RecursiveDeref( dd, bFunc );
328 return NULL;
329}
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_IthVar
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition hopOper.c:63
Hop_Obj_t
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
VER_PARSE_SYM_NEGBEF1
#define VER_PARSE_SYM_NEGBEF1
Definition verFormula.c:35
VER_PARSE_OPER_XOR
#define VER_PARSE_OPER_XOR
Definition verFormula.c:46
VER_PARSE_SYM_OPEN
#define VER_PARSE_SYM_OPEN
DECLARATIONS ///.
Definition verFormula.c:31
VER_PARSE_OPER_OR
#define VER_PARSE_OPER_OR
Definition verFormula.c:47
VER_PARSE_SYM_MUX1
#define VER_PARSE_SYM_MUX1
Definition verFormula.c:40
VER_PARSE_OPER_MUX
#define VER_PARSE_OPER_MUX
Definition verFormula.c:49
VER_PARSE_OPER_AND
#define VER_PARSE_OPER_AND
Definition verFormula.c:45
VER_PARSE_OPER_NEG
#define VER_PARSE_OPER_NEG
Definition verFormula.c:44
VER_PARSE_SYM_MUX2
#define VER_PARSE_SYM_MUX2
Definition verFormula.c:41
VER_PARSE_SYM_CLOSE
#define VER_PARSE_SYM_CLOSE
Definition verFormula.c:32
VER_PARSE_FLAG_START
#define VER_PARSE_FLAG_START
Definition verFormula.c:53
VER_PARSE_SYM_AND
#define VER_PARSE_SYM_AND
Definition verFormula.c:37
VER_PARSE_SYM_NEGBEF2
#define VER_PARSE_SYM_NEGBEF2
Definition verFormula.c:36
VER_PARSE_FLAG_ERROR
#define VER_PARSE_FLAG_ERROR
Definition verFormula.c:56
VER_PARSE_SYM_XOR
#define VER_PARSE_SYM_XOR
Definition verFormula.c:39
VER_PARSE_SYM_OR
#define VER_PARSE_SYM_OR
Definition verFormula.c:38
VER_PARSE_FLAG_OPER
#define VER_PARSE_FLAG_OPER
Definition verFormula.c:55
VER_PARSE_FLAG_VAR
#define VER_PARSE_FLAG_VAR
Definition verFormula.c:54
VER_PARSE_OPER_MARK
#define VER_PARSE_OPER_MARK
Definition verFormula.c:50
Here is the call graph for this function:

◆ Ver_FormulaReduction()

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.

436{
437 Hop_Obj_t * pRes = NULL;
438 int v, fCompl;
439 char Symbol;
440
441 // get the operation
442 Symbol = *pFormula++;
443 fCompl = ( Symbol == '~' );
444 if ( fCompl )
445 Symbol = *pFormula++;
446 // check the operation
447 if ( Symbol != '&' && Symbol != '|' && Symbol != '^' )
448 {
449 sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol );
450 return NULL;
451 }
452 // skip the brace
453 while ( *pFormula++ != '{' );
454 // parse the names
455 Vec_PtrClear( vNames );
456 while ( *pFormula != '}' )
457 {
458 v = Ver_FormulaParserFindVar( pFormula, vNames );
459 pFormula += (int)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*v );
460 while ( *pFormula == ' ' || *pFormula == ',' )
461 pFormula++;
462 }
463 // compute the function
464 if ( Symbol == '&' )
465 pRes = Hop_CreateAnd( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
466 else if ( Symbol == '|' )
467 pRes = Hop_CreateOr( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
468 else if ( Symbol == '^' )
469 pRes = Hop_CreateExor( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
470 return Hop_NotCond( pRes, fCompl );
471}
Hop_CreateOr
Hop_Obj_t * Hop_CreateOr(Hop_Man_t *p, int nVars)
Definition hopOper.c:341
Hop_CreateAnd
Hop_Obj_t * Hop_CreateAnd(Hop_Man_t *p, int nVars)
Definition hopOper.c:320
Hop_CreateExor
Hop_Obj_t * Hop_CreateExor(Hop_Man_t *p, int nVars)
Definition hopOper.c:362
Here is the call graph for this function: