1 /**CFile****************************************************************
2
3 FileName [verFormula.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Verilog parser.]
8
9 Synopsis [Formula parser to read Verilog assign statements.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - August 19, 2006.]
16
17 Revision [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "ver.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 // the list of operation symbols to be used in expressions
31 #define VER_PARSE_SYM_OPEN '(' // opening parenthesis
32 #define VER_PARSE_SYM_CLOSE ')' // closing parenthesis
33 #define VER_PARSE_SYM_CONST0 '0' // constant 0
34 #define VER_PARSE_SYM_CONST1 '1' // constant 1
35 #define VER_PARSE_SYM_NEGBEF1 '!' // negation before the variable
36 #define VER_PARSE_SYM_NEGBEF2 '~' // negation before the variable
37 #define VER_PARSE_SYM_AND '&' // logic AND
38 #define VER_PARSE_SYM_OR '|' // logic OR
39 #define VER_PARSE_SYM_XOR '^' // logic XOR
40 #define VER_PARSE_SYM_MUX1 '?' // first symbol of MUX
41 #define VER_PARSE_SYM_MUX2 ':' // second symbol of MUX
42
43 // the list of opcodes (also specifying operation precedence)
44 #define VER_PARSE_OPER_NEG 7 // negation (highest precedence)
45 #define VER_PARSE_OPER_AND 6 // logic AND
46 #define VER_PARSE_OPER_XOR 5 // logic EXOR (a'b | ab')
47 #define VER_PARSE_OPER_OR 4 // logic OR
48 #define VER_PARSE_OPER_EQU 3 // equvalence (a'b'| ab )
49 #define VER_PARSE_OPER_MUX 2 // MUX(a,b,c) (ab | a'c )
50 #define VER_PARSE_OPER_MARK 1 // OpStack token standing for an opening parenthesis
51
52 // these are values of the internal Flag
53 #define VER_PARSE_FLAG_START 1 // after the opening parenthesis
54 #define VER_PARSE_FLAG_VAR 2 // after operation is received
55 #define VER_PARSE_FLAG_OPER 3 // after operation symbol is received
56 #define VER_PARSE_FLAG_ERROR 4 // when error is detected
57
58 static Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper );
59 static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames );
60
61 ////////////////////////////////////////////////////////////////////////
62 /// FUNCTION DEFINITIONS ///
63 ////////////////////////////////////////////////////////////////////////
64
65 /**Function*************************************************************
66
67 Synopsis [Parser of the formula encountered in assign statements.]
68
69 Description []
70
71 SideEffects []
72
73 SeeAlso []
74
75 ***********************************************************************/
Ver_FormulaParser(char * pFormula,void * pMan,Vec_Ptr_t * vNames,Vec_Ptr_t * vStackFn,Vec_Int_t * vStackOp,char * pErrorMessage)76 void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
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 }
330
331 /**Function*************************************************************
332
333 Synopsis [Performs the operation on the top entries in the stack.]
334
335 Description []
336
337 SideEffects []
338
339 SeeAlso []
340
341 ***********************************************************************/
Ver_FormulaParserTopOper(Hop_Man_t * pMan,Vec_Ptr_t * vStackFn,int Oper)342 Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper )
343 {
344 Hop_Obj_t * bArg0, * bArg1, * bArg2, * bFunc;
345 // perform the given operation
346 bArg2 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
347 bArg1 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
348 if ( Oper == VER_PARSE_OPER_AND )
349 bFunc = Hop_And( pMan, bArg1, bArg2 );
350 else if ( Oper == VER_PARSE_OPER_XOR )
351 bFunc = Hop_Exor( pMan, bArg1, bArg2 );
352 else if ( Oper == VER_PARSE_OPER_OR )
353 bFunc = Hop_Or( pMan, bArg1, bArg2 );
354 else if ( Oper == VER_PARSE_OPER_EQU )
355 bFunc = Hop_Not( Hop_Exor( pMan, bArg1, bArg2 ) );
356 else if ( Oper == VER_PARSE_OPER_MUX )
357 {
358 bArg0 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
359 // bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 ); Cudd_Ref( bFunc );
360 bFunc = Hop_Mux( pMan, bArg0, bArg1, bArg2 );
361 // Cudd_RecursiveDeref( dd, bArg0 );
362 // Cudd_Deref( bFunc );
363 }
364 else
365 return NULL;
366 // Cudd_Ref( bFunc );
367 // Cudd_RecursiveDeref( dd, bArg1 );
368 // Cudd_RecursiveDeref( dd, bArg2 );
369 Vec_PtrPush( vStackFn, bFunc );
370 return bFunc;
371 }
372
373 /**Function*************************************************************
374
375 Synopsis [Returns the index of the new variable found.]
376
377 Description []
378
379 SideEffects []
380
381 SeeAlso []
382
383 ***********************************************************************/
Ver_FormulaParserFindVar(char * pString,Vec_Ptr_t * vNames)384 int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
385 {
386 char * pTemp, * pTemp2;
387 int nLength, nLength2, i;
388 // start the string
389 pTemp = pString;
390 // find the end of the string delimited by other characters
391 if ( *pTemp == '\\' )
392 {
393 pString++;
394 while ( *pTemp && *pTemp != ' ' )
395 pTemp++;
396 }
397 else
398 {
399 while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' &&
400 *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE &&
401 *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 &&
402 *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR &&
403 *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
404 pTemp++;
405 }
406 // look for this string in the array
407 nLength = pTemp - pString;
408 for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
409 {
410 nLength2 = (int)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*i + 0 );
411 if ( nLength2 != nLength )
412 continue;
413 pTemp2 = (char *)Vec_PtrEntry( vNames, 2*i + 1 );
414 if ( strncmp( pString, pTemp2, nLength ) )
415 continue;
416 return i;
417 }
418 // could not find - add and return the number
419 Vec_PtrPush( vNames, (void *)(ABC_PTRUINT_T)nLength );
420 Vec_PtrPush( vNames, pString );
421 return i;
422 }
423
424 /**Function*************************************************************
425
426 Synopsis [Returns the AIG representation of the reduction formula.]
427
428 Description []
429
430 SideEffects []
431
432 SeeAlso []
433
434 ***********************************************************************/
Ver_FormulaReduction(char * pFormula,void * pMan,Vec_Ptr_t * vNames,char * pErrorMessage)435 void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
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 }
472
473 ////////////////////////////////////////////////////////////////////////
474 /// END OF FILE ///
475 ////////////////////////////////////////////////////////////////////////
476
477
478 ABC_NAMESPACE_IMPL_END
479
480