1 /**CFile****************************************************************
2
3 FileName [aigUtil.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [AIG package.]
8
9 Synopsis [Various procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - April 28, 2007.]
16
17 Revision [$Id: aigUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "aig.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28
29 ////////////////////////////////////////////////////////////////////////
30 /// FUNCTION DEFINITIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 /**Function*************************************************************
34
35 Synopsis [Increments the current traversal ID of the network.]
36
37 Description []
38
39 SideEffects []
40
41 SeeAlso []
42
43 ***********************************************************************/
Aig_ManIncrementTravId(Aig_Man_t * p)44 void Aig_ManIncrementTravId( Aig_Man_t * p )
45 {
46 if ( p->nTravIds >= (1<<30)-1 )
47 Aig_ManCleanData( p );
48 p->nTravIds++;
49 }
50
51 /**Function*************************************************************
52
53 Synopsis [Returns the time stamp.]
54
55 Description [The file should be closed.]
56
57 SideEffects []
58
59 SeeAlso []
60
61 ***********************************************************************/
Aig_TimeStamp()62 char * Aig_TimeStamp()
63 {
64 static char Buffer[100];
65 char * TimeStamp;
66 time_t ltime;
67 // get the current time
68 time( <ime );
69 TimeStamp = asctime( localtime( <ime ) );
70 TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
71 strcpy( Buffer, TimeStamp );
72 return Buffer;
73 }
74
75 /**Function*************************************************************
76
77 Synopsis [Make sure AIG has not gaps in the numeric order.]
78
79 Description []
80
81 SideEffects []
82
83 SeeAlso []
84
85 ***********************************************************************/
Aig_ManHasNoGaps(Aig_Man_t * p)86 int Aig_ManHasNoGaps( Aig_Man_t * p )
87 {
88 return (int)(Aig_ManObjNum(p) == Aig_ManCiNum(p) + Aig_ManCoNum(p) + Aig_ManNodeNum(p) + 1);
89 }
90
91 /**Function*************************************************************
92
93 Synopsis [Collect the latches.]
94
95 Description []
96
97 SideEffects []
98
99 SeeAlso []
100
101 ***********************************************************************/
Aig_ManLevels(Aig_Man_t * p)102 int Aig_ManLevels( Aig_Man_t * p )
103 {
104 Aig_Obj_t * pObj;
105 int i, LevelMax = 0;
106 Aig_ManForEachCo( p, pObj, i )
107 LevelMax = Abc_MaxInt( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
108 return LevelMax;
109 }
110
111 /**Function*************************************************************
112
113 Synopsis [Reset reference counters.]
114
115 Description []
116
117 SideEffects []
118
119 SeeAlso []
120
121 ***********************************************************************/
Aig_ManResetRefs(Aig_Man_t * p)122 void Aig_ManResetRefs( Aig_Man_t * p )
123 {
124 Aig_Obj_t * pObj;
125 int i;
126 Aig_ManForEachObj( p, pObj, i )
127 pObj->nRefs = 0;
128 Aig_ManForEachObj( p, pObj, i )
129 {
130 if ( Aig_ObjFanin0(pObj) )
131 Aig_ObjFanin0(pObj)->nRefs++;
132 if ( Aig_ObjFanin1(pObj) )
133 Aig_ObjFanin1(pObj)->nRefs++;
134 }
135 }
136
137 /**Function*************************************************************
138
139 Synopsis [Cleans fMarkA.]
140
141 Description []
142
143 SideEffects []
144
145 SeeAlso []
146
147 ***********************************************************************/
Aig_ManCleanMarkA(Aig_Man_t * p)148 void Aig_ManCleanMarkA( Aig_Man_t * p )
149 {
150 Aig_Obj_t * pObj;
151 int i;
152 Aig_ManForEachObj( p, pObj, i )
153 pObj->fMarkA = 0;
154 }
155
156 /**Function*************************************************************
157
158 Synopsis [Cleans fMarkB.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ***********************************************************************/
Aig_ManCleanMarkB(Aig_Man_t * p)167 void Aig_ManCleanMarkB( Aig_Man_t * p )
168 {
169 Aig_Obj_t * pObj;
170 int i;
171 Aig_ManForEachObj( p, pObj, i )
172 pObj->fMarkB = 0;
173 }
174
175 /**Function*************************************************************
176
177 Synopsis [Cleans fMarkB.]
178
179 Description []
180
181 SideEffects []
182
183 SeeAlso []
184
185 ***********************************************************************/
Aig_ManCleanMarkAB(Aig_Man_t * p)186 void Aig_ManCleanMarkAB( Aig_Man_t * p )
187 {
188 Aig_Obj_t * pObj;
189 int i;
190 Aig_ManForEachObj( p, pObj, i )
191 pObj->fMarkA = pObj->fMarkB = 0;
192 }
193
194 /**Function*************************************************************
195
196 Synopsis [Cleans the data pointers for the nodes.]
197
198 Description []
199
200 SideEffects []
201
202 SeeAlso []
203
204 ***********************************************************************/
Aig_ManCleanData(Aig_Man_t * p)205 void Aig_ManCleanData( Aig_Man_t * p )
206 {
207 Aig_Obj_t * pObj;
208 int i;
209 Aig_ManForEachObj( p, pObj, i )
210 pObj->pData = NULL;
211 }
212
213 /**Function*************************************************************
214
215 Synopsis [Cleans the data pointers for the nodes.]
216
217 Description []
218
219 SideEffects []
220
221 SeeAlso []
222
223 ***********************************************************************/
Aig_ManCleanNext(Aig_Man_t * p)224 void Aig_ManCleanNext( Aig_Man_t * p )
225 {
226 Aig_Obj_t * pObj;
227 int i;
228 Aig_ManForEachObj( p, pObj, i )
229 pObj->pNext = NULL;
230 }
231
232 /**Function*************************************************************
233
234 Synopsis [Recursively cleans the data pointers in the cone of the node.]
235
236 Description [Applicable to small AIGs only because no caching is performed.]
237
238 SideEffects []
239
240 SeeAlso []
241
242 ***********************************************************************/
Aig_ObjCleanData_rec(Aig_Obj_t * pObj)243 void Aig_ObjCleanData_rec( Aig_Obj_t * pObj )
244 {
245 assert( !Aig_IsComplement(pObj) );
246 assert( !Aig_ObjIsCo(pObj) );
247 if ( Aig_ObjIsAnd(pObj) )
248 {
249 Aig_ObjCleanData_rec( Aig_ObjFanin0(pObj) );
250 Aig_ObjCleanData_rec( Aig_ObjFanin1(pObj) );
251 }
252 pObj->pData = NULL;
253 }
254
255
256 /**Function*************************************************************
257
258 Synopsis [Detects multi-input gate rooted at this node.]
259
260 Description []
261
262 SideEffects []
263
264 SeeAlso []
265
266 ***********************************************************************/
Aig_ObjCollectMulti_rec(Aig_Obj_t * pRoot,Aig_Obj_t * pObj,Vec_Ptr_t * vSuper)267 void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
268 {
269 if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
270 {
271 Vec_PtrPushUnique(vSuper, pObj);
272 return;
273 }
274 Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
275 Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
276 }
277
278 /**Function*************************************************************
279
280 Synopsis [Detects multi-input gate rooted at this node.]
281
282 Description []
283
284 SideEffects []
285
286 SeeAlso []
287
288 ***********************************************************************/
Aig_ObjCollectMulti(Aig_Obj_t * pRoot,Vec_Ptr_t * vSuper)289 void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper )
290 {
291 assert( !Aig_IsComplement(pRoot) );
292 Vec_PtrClear( vSuper );
293 Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
294 }
295
296 /**Function*************************************************************
297
298 Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
299
300 Description []
301
302 SideEffects []
303
304 SeeAlso []
305
306 ***********************************************************************/
Aig_ObjIsMuxType(Aig_Obj_t * pNode)307 int Aig_ObjIsMuxType( Aig_Obj_t * pNode )
308 {
309 Aig_Obj_t * pNode0, * pNode1;
310 // check that the node is regular
311 assert( !Aig_IsComplement(pNode) );
312 // if the node is not AND, this is not MUX
313 if ( !Aig_ObjIsAnd(pNode) )
314 return 0;
315 // if the children are not complemented, this is not MUX
316 if ( !Aig_ObjFaninC0(pNode) || !Aig_ObjFaninC1(pNode) )
317 return 0;
318 // get children
319 pNode0 = Aig_ObjFanin0(pNode);
320 pNode1 = Aig_ObjFanin1(pNode);
321 // if the children are not ANDs, this is not MUX
322 if ( !Aig_ObjIsAnd(pNode0) || !Aig_ObjIsAnd(pNode1) )
323 return 0;
324 // otherwise the node is MUX iff it has a pair of equal grandchildren
325 return (Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
326 (Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1))) ||
327 (Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
328 (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
329 }
330
331
332 /**Function*************************************************************
333
334 Synopsis [Recognizes what nodes are inputs of the EXOR.]
335
336 Description []
337
338 SideEffects []
339
340 SeeAlso []
341
342 ***********************************************************************/
Aig_ObjRecognizeExor(Aig_Obj_t * pObj,Aig_Obj_t ** ppFan0,Aig_Obj_t ** ppFan1)343 int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
344 {
345 Aig_Obj_t * p0, * p1;
346 assert( !Aig_IsComplement(pObj) );
347 if ( !Aig_ObjIsNode(pObj) )
348 return 0;
349 if ( Aig_ObjIsExor(pObj) )
350 {
351 *ppFan0 = Aig_ObjChild0(pObj);
352 *ppFan1 = Aig_ObjChild1(pObj);
353 return 1;
354 }
355 assert( Aig_ObjIsAnd(pObj) );
356 p0 = Aig_ObjChild0(pObj);
357 p1 = Aig_ObjChild1(pObj);
358 if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
359 return 0;
360 p0 = Aig_Regular(p0);
361 p1 = Aig_Regular(p1);
362 if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
363 return 0;
364 if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
365 return 0;
366 if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
367 return 0;
368 *ppFan0 = Aig_ObjChild0(p0);
369 *ppFan1 = Aig_ObjChild1(p0);
370 return 1;
371 }
372
373 /**Function*************************************************************
374
375 Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
376
377 Description [If the node is a MUX, returns the control variable C.
378 Assigns nodes T and E to be the then and else variables of the MUX.
379 Node C is never complemented. Nodes T and E can be complemented.
380 This function also recognizes EXOR/NEXOR gates as MUXes.]
381
382 SideEffects []
383
384 SeeAlso []
385
386 ***********************************************************************/
Aig_ObjRecognizeMux(Aig_Obj_t * pNode,Aig_Obj_t ** ppNodeT,Aig_Obj_t ** ppNodeE)387 Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Obj_t ** ppNodeE )
388 {
389 Aig_Obj_t * pNode0, * pNode1;
390 assert( !Aig_IsComplement(pNode) );
391 assert( Aig_ObjIsMuxType(pNode) );
392 // get children
393 pNode0 = Aig_ObjFanin0(pNode);
394 pNode1 = Aig_ObjFanin1(pNode);
395
396 // find the control variable
397 if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
398 {
399 // if ( Fraig_IsComplement(pNode1->p2) )
400 if ( Aig_ObjFaninC1(pNode0) )
401 { // pNode2->p2 is positive phase of C
402 *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
403 *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
404 return Aig_ObjChild1(pNode1);//pNode2->p2;
405 }
406 else
407 { // pNode1->p2 is positive phase of C
408 *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
409 *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
410 return Aig_ObjChild1(pNode0);//pNode1->p2;
411 }
412 }
413 else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
414 {
415 // if ( Fraig_IsComplement(pNode1->p1) )
416 if ( Aig_ObjFaninC0(pNode0) )
417 { // pNode2->p1 is positive phase of C
418 *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
419 *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
420 return Aig_ObjChild0(pNode1);//pNode2->p1;
421 }
422 else
423 { // pNode1->p1 is positive phase of C
424 *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
425 *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
426 return Aig_ObjChild0(pNode0);//pNode1->p1;
427 }
428 }
429 else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
430 {
431 // if ( Fraig_IsComplement(pNode1->p1) )
432 if ( Aig_ObjFaninC0(pNode0) )
433 { // pNode2->p2 is positive phase of C
434 *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
435 *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
436 return Aig_ObjChild1(pNode1);//pNode2->p2;
437 }
438 else
439 { // pNode1->p1 is positive phase of C
440 *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
441 *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
442 return Aig_ObjChild0(pNode0);//pNode1->p1;
443 }
444 }
445 else if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
446 {
447 // if ( Fraig_IsComplement(pNode1->p2) )
448 if ( Aig_ObjFaninC1(pNode0) )
449 { // pNode2->p1 is positive phase of C
450 *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
451 *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
452 return Aig_ObjChild0(pNode1);//pNode2->p1;
453 }
454 else
455 { // pNode1->p2 is positive phase of C
456 *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
457 *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
458 return Aig_ObjChild1(pNode0);//pNode1->p2;
459 }
460 }
461 assert( 0 ); // this is not MUX
462 return NULL;
463 }
464
465 /**Function*************************************************************
466
467 Synopsis []
468
469 Description []
470
471 SideEffects []
472
473 SeeAlso []
474
475 ***********************************************************************/
Aig_ObjReal_rec(Aig_Obj_t * pObj)476 Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj )
477 {
478 Aig_Obj_t * pObjNew, * pObjR = Aig_Regular(pObj);
479 if ( !Aig_ObjIsBuf(pObjR) )
480 return pObj;
481 pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObjR) );
482 return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) );
483 }
484
485 /**Function*************************************************************
486
487 Synopsis [Procedure used for sorting the nodes in increasing order of IDs.]
488
489 Description []
490
491 SideEffects []
492
493 SeeAlso []
494
495 ***********************************************************************/
Aig_ObjCompareIdIncrease(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)496 int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
497 {
498 int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
499 if ( Diff < 0 )
500 return -1;
501 if ( Diff > 0 )
502 return 1;
503 return 0;
504 }
505
506
507 /**Function*************************************************************
508
509 Synopsis [Prints Eqn formula for the AIG rooted at this node.]
510
511 Description [The formula is in terms of PIs, which should have
512 their names assigned in pObj->pData fields.]
513
514 SideEffects []
515
516 SeeAlso []
517
518 ***********************************************************************/
Aig_ObjPrintEqn(FILE * pFile,Aig_Obj_t * pObj,Vec_Vec_t * vLevels,int Level)519 void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
520 {
521 Vec_Ptr_t * vSuper;
522 Aig_Obj_t * pFanin;
523 int fCompl, i;
524 // store the complemented attribute
525 fCompl = Aig_IsComplement(pObj);
526 pObj = Aig_Regular(pObj);
527 // constant case
528 if ( Aig_ObjIsConst1(pObj) )
529 {
530 fprintf( pFile, "%d", !fCompl );
531 return;
532 }
533 // PI case
534 if ( Aig_ObjIsCi(pObj) )
535 {
536 fprintf( pFile, "%s%s", fCompl? "!" : "", (char*)pObj->pData );
537 return;
538 }
539 // AND case
540 Vec_VecExpand( vLevels, Level );
541 vSuper = Vec_VecEntry(vLevels, Level);
542 Aig_ObjCollectMulti( pObj, vSuper );
543 fprintf( pFile, "%s", (Level==0? "" : "(") );
544 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
545 {
546 Aig_ObjPrintEqn( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
547 if ( i < Vec_PtrSize(vSuper) - 1 )
548 fprintf( pFile, " %s ", fCompl? "+" : "*" );
549 }
550 fprintf( pFile, "%s", (Level==0? "" : ")") );
551 return;
552 }
553
554 /**Function*************************************************************
555
556 Synopsis [Prints Verilog formula for the AIG rooted at this node.]
557
558 Description [The formula is in terms of PIs, which should have
559 their names assigned in pObj->pData fields.]
560
561 SideEffects []
562
563 SeeAlso []
564
565 ***********************************************************************/
Aig_ObjPrintVerilog(FILE * pFile,Aig_Obj_t * pObj,Vec_Vec_t * vLevels,int Level)566 void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
567 {
568 Vec_Ptr_t * vSuper;
569 Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
570 int fCompl, i;
571 // store the complemented attribute
572 fCompl = Aig_IsComplement(pObj);
573 pObj = Aig_Regular(pObj);
574 // constant case
575 if ( Aig_ObjIsConst1(pObj) )
576 {
577 fprintf( pFile, "1\'b%d", !fCompl );
578 return;
579 }
580 // PI case
581 if ( Aig_ObjIsCi(pObj) )
582 {
583 fprintf( pFile, "%s%s", fCompl? "~" : "", (char*)pObj->pData );
584 return;
585 }
586 // EXOR case
587 if ( Aig_ObjIsExor(pObj) )
588 {
589 Vec_VecExpand( vLevels, Level );
590 vSuper = Vec_VecEntry( vLevels, Level );
591 Aig_ObjCollectMulti( pObj, vSuper );
592 fprintf( pFile, "%s", (Level==0? "" : "(") );
593 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
594 {
595 Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
596 if ( i < Vec_PtrSize(vSuper) - 1 )
597 fprintf( pFile, " ^ " );
598 }
599 fprintf( pFile, "%s", (Level==0? "" : ")") );
600 return;
601 }
602 // MUX case
603 if ( Aig_ObjIsMuxType(pObj) )
604 {
605 if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
606 {
607 fprintf( pFile, "%s", (Level==0? "" : "(") );
608 Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
609 fprintf( pFile, " ^ " );
610 Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
611 fprintf( pFile, "%s", (Level==0? "" : ")") );
612 }
613 else
614 {
615 pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
616 fprintf( pFile, "%s", (Level==0? "" : "(") );
617 Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
618 fprintf( pFile, " ? " );
619 Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
620 fprintf( pFile, " : " );
621 Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
622 fprintf( pFile, "%s", (Level==0? "" : ")") );
623 }
624 return;
625 }
626 // AND case
627 Vec_VecExpand( vLevels, Level );
628 vSuper = Vec_VecEntry(vLevels, Level);
629 Aig_ObjCollectMulti( pObj, vSuper );
630 fprintf( pFile, "%s", (Level==0? "" : "(") );
631 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
632 {
633 Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
634 if ( i < Vec_PtrSize(vSuper) - 1 )
635 fprintf( pFile, " %s ", fCompl? "|" : "&" );
636 }
637 fprintf( pFile, "%s", (Level==0? "" : ")") );
638 return;
639 }
640
641
642 /**Function*************************************************************
643
644 Synopsis [Prints node in HAIG.]
645
646 Description []
647
648 SideEffects []
649
650 SeeAlso []
651
652 ***********************************************************************/
Aig_ObjPrintVerbose(Aig_Obj_t * pObj,int fHaig)653 void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
654 {
655 assert( !Aig_IsComplement(pObj) );
656 printf( "Node %d : ", pObj->Id );
657 if ( Aig_ObjIsConst1(pObj) )
658 printf( "constant 1" );
659 else if ( Aig_ObjIsCi(pObj) )
660 printf( "CI" );
661 else if ( Aig_ObjIsCo(pObj) )
662 {
663 printf( "CO( " );
664 printf( "%d%s )",
665 Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
666 }
667 else
668 printf( "AND( %d%s, %d%s )",
669 Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "),
670 Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") );
671 printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
672 }
Aig_ObjPrintVerboseCone(Aig_Man_t * p,Aig_Obj_t * pRoot,int fHaig)673 void Aig_ObjPrintVerboseCone( Aig_Man_t * p, Aig_Obj_t * pRoot, int fHaig )
674 {
675 extern Vec_Ptr_t * Aig_ManDfsArray( Aig_Man_t * p, Aig_Obj_t ** pNodes, int nNodes );
676 Vec_Ptr_t * vNodes;
677 Aig_Obj_t * pObj;
678 int i;
679 vNodes = Aig_ManDfsArray( p, &pRoot, 1 );
680 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
681 Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
682 printf( "\n" );
683 Vec_PtrFree( vNodes );
684
685 }
686
687 /**Function*************************************************************
688
689 Synopsis [Prints node in HAIG.]
690
691 Description []
692
693 SideEffects []
694
695 SeeAlso []
696
697 ***********************************************************************/
Aig_ManPrintVerbose(Aig_Man_t * p,int fHaig)698 void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
699 {
700 Vec_Ptr_t * vNodes;
701 Aig_Obj_t * pObj;
702 int i;
703 printf( "PIs: " );
704 Aig_ManForEachCi( p, pObj, i )
705 printf( " %p", pObj );
706 printf( "\n" );
707 vNodes = Aig_ManDfs( p, 0 );
708 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
709 Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
710 printf( "\n" );
711 Vec_PtrFree( vNodes );
712 }
713
714 /**Function*************************************************************
715
716 Synopsis [Write speculative miter for one node.]
717
718 Description []
719
720 SideEffects []
721
722 SeeAlso []
723
724 ***********************************************************************/
Aig_ManDump(Aig_Man_t * p)725 void Aig_ManDump( Aig_Man_t * p )
726 {
727 static int Counter = 0;
728 char FileName[200];
729 // dump the logic into a file
730 sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
731 Aig_ManDumpBlif( p, FileName, NULL, NULL );
732 printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName );
733 }
734
735 /**Function*************************************************************
736
737 Synopsis [Writes the AIG into a BLIF file.]
738
739 Description []
740
741 SideEffects []
742
743 SeeAlso []
744
745 ***********************************************************************/
Aig_ManDumpBlif(Aig_Man_t * p,char * pFileName,Vec_Ptr_t * vPiNames,Vec_Ptr_t * vPoNames)746 void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
747 {
748 FILE * pFile;
749 Vec_Ptr_t * vNodes;
750 Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
751 int i, nDigits, Counter = 0;
752 if ( Aig_ManCoNum(p) == 0 )
753 {
754 printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
755 return;
756 }
757 // check if constant is used
758 Aig_ManForEachCo( p, pObj, i )
759 if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
760 pConst1 = Aig_ManConst1(p);
761 // collect nodes in the DFS order
762 vNodes = Aig_ManDfs( p, 1 );
763 // assign IDs to objects
764 Aig_ManConst1(p)->iData = Counter++;
765 Aig_ManForEachCi( p, pObj, i )
766 pObj->iData = Counter++;
767 Aig_ManForEachCo( p, pObj, i )
768 pObj->iData = Counter++;
769 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
770 pObj->iData = Counter++;
771 nDigits = Abc_Base10Log( Counter );
772 // write the file
773 pFile = fopen( pFileName, "w" );
774 fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
775 // fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
776 fprintf( pFile, ".model %s\n", p->pName );
777 // write PIs
778 fprintf( pFile, ".inputs" );
779 Aig_ManForEachPiSeq( p, pObj, i )
780 if ( vPiNames )
781 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) );
782 else
783 fprintf( pFile, " n%0*d", nDigits, pObj->iData );
784 fprintf( pFile, "\n" );
785 // write POs
786 fprintf( pFile, ".outputs" );
787 Aig_ManForEachPoSeq( p, pObj, i )
788 if ( vPoNames )
789 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) );
790 else
791 fprintf( pFile, " n%0*d", nDigits, pObj->iData );
792 fprintf( pFile, "\n" );
793 // write latches
794 if ( Aig_ManRegNum(p) )
795 {
796 fprintf( pFile, "\n" );
797 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
798 {
799 fprintf( pFile, ".latch" );
800 if ( vPoNames )
801 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i) );
802 else
803 fprintf( pFile, " n%0*d", nDigits, pObjLi->iData );
804 if ( vPiNames )
805 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i) );
806 else
807 fprintf( pFile, " n%0*d", nDigits, pObjLo->iData );
808 fprintf( pFile, " 0\n" );
809 }
810 fprintf( pFile, "\n" );
811 }
812 // write nodes
813 if ( pConst1 )
814 fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
815 Aig_ManSetCioIds( p );
816 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
817 {
818 fprintf( pFile, ".names" );
819 if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
820 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
821 else
822 fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
823 if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) )
824 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) );
825 else
826 fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
827 fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
828 fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
829 }
830 // write POs
831 Aig_ManForEachCo( p, pObj, i )
832 {
833 fprintf( pFile, ".names" );
834 if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
835 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
836 else
837 fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
838 if ( vPoNames )
839 fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) );
840 else
841 fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
842 fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
843 }
844 Aig_ManCleanCioIds( p );
845 fprintf( pFile, ".end\n\n" );
846 fclose( pFile );
847 Vec_PtrFree( vNodes );
848 }
849
850 /**Function*************************************************************
851
852 Synopsis [Writes the AIG into a Verilog file.]
853
854 Description []
855
856 SideEffects []
857
858 SeeAlso []
859
860 ***********************************************************************/
Aig_ManDumpVerilog(Aig_Man_t * p,char * pFileName)861 void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
862 {
863 FILE * pFile;
864 Vec_Ptr_t * vNodes;
865 Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
866 int i, nDigits, Counter = 0;
867 if ( Aig_ManCoNum(p) == 0 )
868 {
869 printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
870 return;
871 }
872 // check if constant is used
873 Aig_ManForEachCo( p, pObj, i )
874 if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
875 pConst1 = Aig_ManConst1(p);
876 // collect nodes in the DFS order
877 vNodes = Aig_ManDfs( p, 1 );
878 // assign IDs to objects
879 Aig_ManConst1(p)->iData = Counter++;
880 Aig_ManForEachCi( p, pObj, i )
881 pObj->iData = Counter++;
882 Aig_ManForEachCo( p, pObj, i )
883 pObj->iData = Counter++;
884 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
885 pObj->iData = Counter++;
886 nDigits = Abc_Base10Log( Counter );
887 // write the file
888 pFile = fopen( pFileName, "w" );
889 fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" );
890 // fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
891 if ( Aig_ManRegNum(p) )
892 fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" );
893 else
894 fprintf( pFile, "module %s (", p->pName? p->pName: "test" );
895 Aig_ManForEachPiSeq( p, pObj, i )
896 fprintf( pFile, "%s n%0*d", ((Aig_ManRegNum(p) || i)? ",":""), nDigits, pObj->iData );
897 Aig_ManForEachPoSeq( p, pObj, i )
898 fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
899 fprintf( pFile, " );\n" );
900
901 // write PIs
902 if ( Aig_ManRegNum(p) )
903 fprintf( pFile, "input clock;\n" );
904 Aig_ManForEachPiSeq( p, pObj, i )
905 fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData );
906 // write POs
907 Aig_ManForEachPoSeq( p, pObj, i )
908 fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData );
909 // write latches
910 if ( Aig_ManRegNum(p) )
911 {
912 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
913 fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData );
914 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
915 fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
916 }
917 // write nodes
918 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
919 fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
920 if ( pConst1 )
921 fprintf( pFile, "wire n%0*d;\n", nDigits, pConst1->iData );
922 // write nodes
923 if ( pConst1 )
924 fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
925 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
926 {
927 fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n",
928 nDigits, pObj->iData,
929 !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData,
930 !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData
931 );
932 }
933 // write POs
934 Aig_ManForEachPoSeq( p, pObj, i )
935 {
936 fprintf( pFile, "assign n%0*d = %sn%0*d;\n",
937 nDigits, pObj->iData,
938 !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData );
939 }
940 if ( Aig_ManRegNum(p) )
941 {
942 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
943 {
944 fprintf( pFile, "assign n%0*d = %sn%0*d;\n",
945 nDigits, pObjLi->iData,
946 !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData );
947 }
948 }
949
950 // write initial state
951 if ( Aig_ManRegNum(p) )
952 {
953 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
954 fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n",
955 nDigits, pObjLo->iData,
956 nDigits, pObjLi->iData );
957 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
958 fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n",
959 nDigits, pObjLo->iData );
960 }
961
962 fprintf( pFile, "endmodule\n\n" );
963 fclose( pFile );
964 Vec_PtrFree( vNodes );
965 }
966
967 /**Function*************************************************************
968
969 Synopsis [Sets the PI/PO numbers.]
970
971 Description []
972
973 SideEffects []
974
975 SeeAlso []
976
977 ***********************************************************************/
Aig_ManSetCioIds(Aig_Man_t * p)978 void Aig_ManSetCioIds( Aig_Man_t * p )
979 {
980 Aig_Obj_t * pObj;
981 int i;
982 Aig_ManForEachCi( p, pObj, i )
983 pObj->CioId = i;
984 Aig_ManForEachCo( p, pObj, i )
985 pObj->CioId = i;
986 }
987
988 /**Function*************************************************************
989
990 Synopsis [Sets the PI/PO numbers.]
991
992 Description []
993
994 SideEffects []
995
996 SeeAlso []
997
998 ***********************************************************************/
Aig_ManCleanCioIds(Aig_Man_t * p)999 void Aig_ManCleanCioIds( Aig_Man_t * p )
1000 {
1001 Aig_Obj_t * pObj;
1002 int i;
1003 Aig_ManForEachCi( p, pObj, i )
1004 pObj->pNext = NULL;
1005 Aig_ManForEachCo( p, pObj, i )
1006 pObj->pNext = NULL;
1007 }
1008
1009 /**Function*************************************************************
1010
1011 Synopsis [Sets the PI/PO numbers.]
1012
1013 Description []
1014
1015 SideEffects []
1016
1017 SeeAlso []
1018
1019 ***********************************************************************/
Aig_ManChoiceNum(Aig_Man_t * p)1020 int Aig_ManChoiceNum( Aig_Man_t * p )
1021 {
1022 Aig_Obj_t * pObj;
1023 int i, Counter = 0;
1024 Aig_ManForEachNode( p, pObj, i )
1025 Counter += Aig_ObjIsChoice( p, pObj );
1026 return Counter;
1027 }
1028
1029 /**Function*************************************************************
1030
1031 Synopsis [Prints the fanouts of the control register.]
1032
1033 Description [Useful only for Intel MC benchmarks.]
1034
1035 SideEffects []
1036
1037 SeeAlso []
1038
1039 ***********************************************************************/
Aig_ManPrintControlFanouts(Aig_Man_t * p)1040 void Aig_ManPrintControlFanouts( Aig_Man_t * p )
1041 {
1042 Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;
1043 int i;
1044
1045 pCtrl = Aig_ManCi( p, Aig_ManCiNum(p) - 1 );
1046
1047 printf( "Control signal:\n" );
1048 Aig_ObjPrint( p, pCtrl ); printf( "\n\n" );
1049
1050 Aig_ManForEachObj( p, pObj, i )
1051 {
1052 if ( !Aig_ObjIsNode(pObj) )
1053 continue;
1054 assert( pObj != pCtrl );
1055 pFanin0 = Aig_ObjFanin0(pObj);
1056 pFanin1 = Aig_ObjFanin1(pObj);
1057 if ( pFanin0 == pCtrl && Aig_ObjIsCi(pFanin1) )
1058 {
1059 Aig_ObjPrint( p, pObj ); printf( "\n" );
1060 Aig_ObjPrint( p, pFanin1 ); printf( "\n" );
1061 printf( "\n" );
1062 }
1063 if ( pFanin1 == pCtrl && Aig_ObjIsCi(pFanin0) )
1064 {
1065 Aig_ObjPrint( p, pObj ); printf( "\n" );
1066 Aig_ObjPrint( p, pFanin0 ); printf( "\n" );
1067 printf( "\n" );
1068 }
1069 }
1070 }
1071
1072 /**Function*************************************************************
1073
1074 Synopsis [Returns the composite name of the file.]
1075
1076 Description []
1077
1078 SideEffects []
1079
1080 SeeAlso []
1081
1082 ***********************************************************************/
Aig_FileNameGenericAppend(char * pBase,char * pSuffix)1083 char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix )
1084 {
1085 static char Buffer[1000];
1086 char * pDot;
1087 strcpy( Buffer, pBase );
1088 if ( (pDot = strrchr( Buffer, '.' )) )
1089 *pDot = 0;
1090 strcat( Buffer, pSuffix );
1091 if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
1092 return pDot+1;
1093 return Buffer;
1094 }
1095
1096 /**Function*************************************************************
1097
1098 Synopsis [Creates a sequence of random numbers.]
1099
1100 Description []
1101
1102 SideEffects []
1103
1104 SeeAlso [http://en.wikipedia.org/wiki/LFSR]
1105
1106 ***********************************************************************/
Aig_ManRandomTest2()1107 void Aig_ManRandomTest2()
1108 {
1109 FILE * pFile;
1110 unsigned int lfsr = 1;
1111 unsigned int period = 0;
1112 pFile = fopen( "rand.txt", "w" );
1113 do {
1114 // lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1
1115 lfsr = 1; // to prevent the warning
1116 ++period;
1117 fprintf( pFile, "%10d : %10d ", period, lfsr );
1118 // Extra_PrintBinary( pFile, &lfsr, 32 );
1119 fprintf( pFile, "\n" );
1120 if ( period == 20000 )
1121 break;
1122 } while(lfsr != 1u);
1123 fclose( pFile );
1124 }
1125
1126 /**Function*************************************************************
1127
1128 Synopsis [Creates a sequence of random numbers.]
1129
1130 Description []
1131
1132 SideEffects []
1133
1134 SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
1135
1136 ***********************************************************************/
Aig_ManRandomTest1()1137 void Aig_ManRandomTest1()
1138 {
1139 FILE * pFile;
1140 unsigned int lfsr;
1141 unsigned int period = 0;
1142 pFile = fopen( "rand.txt", "w" );
1143 do {
1144 lfsr = Aig_ManRandom( 0 );
1145 ++period;
1146 fprintf( pFile, "%10d : %10d ", period, lfsr );
1147 // Extra_PrintBinary( pFile, &lfsr, 32 );
1148 fprintf( pFile, "\n" );
1149 if ( period == 20000 )
1150 break;
1151 } while(lfsr != 1u);
1152 fclose( pFile );
1153 }
1154
1155
1156 #define NUMBER1 3716960521u
1157 #define NUMBER2 2174103536u
1158
1159 /**Function*************************************************************
1160
1161 Synopsis [Creates a sequence of random numbers.]
1162
1163 Description []
1164
1165 SideEffects []
1166
1167 SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
1168
1169 ***********************************************************************/
Aig_ManRandom(int fReset)1170 unsigned Aig_ManRandom( int fReset )
1171 {
1172 static unsigned int m_z = NUMBER1;
1173 static unsigned int m_w = NUMBER2;
1174 if ( fReset )
1175 {
1176 m_z = NUMBER1;
1177 m_w = NUMBER2;
1178 }
1179 m_z = 36969 * (m_z & 65535) + (m_z >> 16);
1180 m_w = 18000 * (m_w & 65535) + (m_w >> 16);
1181 return (m_z << 16) + m_w;
1182 }
1183
1184 /**Function*************************************************************
1185
1186 Synopsis [Creates a sequence of random numbers.]
1187
1188 Description []
1189
1190 SideEffects []
1191
1192 SeeAlso []
1193
1194 ***********************************************************************/
Aig_ManRandom64(int fReset)1195 word Aig_ManRandom64( int fReset )
1196 {
1197 word Res = (word)Aig_ManRandom(fReset);
1198 return Res | ((word)Aig_ManRandom(0) << 32);
1199 }
1200
1201
1202 /**Function*************************************************************
1203
1204 Synopsis [Creates random info for the primary inputs.]
1205
1206 Description []
1207
1208 SideEffects []
1209
1210 SeeAlso []
1211
1212 ***********************************************************************/
Aig_ManRandomInfo(Vec_Ptr_t * vInfo,int iInputStart,int iWordStart,int iWordStop)1213 void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
1214 {
1215 unsigned * pInfo;
1216 int i, w;
1217 Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart )
1218 for ( w = iWordStart; w < iWordStop; w++ )
1219 pInfo[w] = Aig_ManRandom(0);
1220 }
1221
1222 /**Function*************************************************************
1223
1224 Synopsis [Returns the result of merging the two vectors.]
1225
1226 Description [Assumes that the vectors are sorted in the increasing order.]
1227
1228 SideEffects []
1229
1230 SeeAlso []
1231
1232 ***********************************************************************/
Aig_NodeUnionLists(Vec_Ptr_t * vArr1,Vec_Ptr_t * vArr2,Vec_Ptr_t * vArr)1233 void Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
1234 {
1235 Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
1236 Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
1237 Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
1238 Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
1239 Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
1240 Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
1241 pBeg = (Aig_Obj_t **)vArr->pArray;
1242 while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
1243 {
1244 if ( (*pBeg1)->Id == (*pBeg2)->Id )
1245 *pBeg++ = *pBeg1++, pBeg2++;
1246 else if ( (*pBeg1)->Id < (*pBeg2)->Id )
1247 *pBeg++ = *pBeg1++;
1248 else
1249 *pBeg++ = *pBeg2++;
1250 }
1251 while ( pBeg1 < pEnd1 )
1252 *pBeg++ = *pBeg1++;
1253 while ( pBeg2 < pEnd2 )
1254 *pBeg++ = *pBeg2++;
1255 vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
1256 assert( vArr->nSize <= vArr->nCap );
1257 assert( vArr->nSize >= vArr1->nSize );
1258 assert( vArr->nSize >= vArr2->nSize );
1259 }
1260
1261 /**Function*************************************************************
1262
1263 Synopsis [Returns the result of intersecting the two vectors.]
1264
1265 Description [Assumes that the vectors are sorted in the increasing order.]
1266
1267 SideEffects []
1268
1269 SeeAlso []
1270
1271 ***********************************************************************/
Aig_NodeIntersectLists(Vec_Ptr_t * vArr1,Vec_Ptr_t * vArr2,Vec_Ptr_t * vArr)1272 void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
1273 {
1274 Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
1275 Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
1276 Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
1277 Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
1278 Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
1279 Vec_PtrGrow( vArr, Abc_MaxInt( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
1280 pBeg = (Aig_Obj_t **)vArr->pArray;
1281 while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
1282 {
1283 if ( (*pBeg1)->Id == (*pBeg2)->Id )
1284 *pBeg++ = *pBeg1++, pBeg2++;
1285 else if ( (*pBeg1)->Id < (*pBeg2)->Id )
1286 // *pBeg++ = *pBeg1++;
1287 pBeg1++;
1288 else
1289 // *pBeg++ = *pBeg2++;
1290 pBeg2++;
1291 }
1292 // while ( pBeg1 < pEnd1 )
1293 // *pBeg++ = *pBeg1++;
1294 // while ( pBeg2 < pEnd2 )
1295 // *pBeg++ = *pBeg2++;
1296 vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
1297 assert( vArr->nSize <= vArr->nCap );
1298 assert( vArr->nSize <= vArr1->nSize );
1299 assert( vArr->nSize <= vArr2->nSize );
1300 }
1301
1302 ABC_NAMESPACE_IMPL_END
1303
1304 #include "proof/fra/fra.h"
1305 #include "aig/saig/saig.h"
1306
1307 ABC_NAMESPACE_IMPL_START
1308
1309
1310 extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex );
1311 extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig );
1312 extern int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame );
1313
1314 /**Function*************************************************************
1315
1316 Synopsis [Starts the process of retuning values for internal nodes.]
1317
1318 Description [Should be called when pCex is available, before probing
1319 any object for its value using Aig_ManCounterExampleValueLookup().]
1320
1321 SideEffects []
1322
1323 SeeAlso []
1324
1325 ***********************************************************************/
Aig_ManCounterExampleValueStart(Aig_Man_t * pAig,Abc_Cex_t * pCex)1326 void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
1327 {
1328 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
1329 int Val0, Val1, nObjs, i, k, iBit = 0;
1330 assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
1331 assert( pAig->pData2 == NULL ); // if this fail, there may be a memory leak
1332 // allocate memory to store simulation bits for internal nodes
1333 pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) );
1334 // the register values in the counter-example should be zero
1335 Saig_ManForEachLo( pAig, pObj, k )
1336 assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
1337 // iterate through the timeframes
1338 nObjs = Aig_ManObjNumMax(pAig);
1339 for ( i = 0; i <= pCex->iFrame; i++ )
1340 {
1341 // set constant 1 node
1342 Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
1343 // set primary inputs according to the counter-example
1344 Saig_ManForEachPi( pAig, pObj, k )
1345 if ( Abc_InfoHasBit(pCex->pData, iBit++) )
1346 Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
1347 // compute values for each node
1348 Aig_ManForEachNode( pAig, pObj, k )
1349 {
1350 Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
1351 Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
1352 if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
1353 Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
1354 }
1355 // derive values for combinational outputs
1356 Aig_ManForEachCo( pAig, pObj, k )
1357 {
1358 Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
1359 if ( Val0 ^ Aig_ObjFaninC0(pObj) )
1360 Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
1361 }
1362 if ( i == pCex->iFrame )
1363 continue;
1364 // transfer values to the register output of the next frame
1365 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
1366 if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
1367 Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
1368 }
1369 assert( iBit == pCex->nBits );
1370 // check that the counter-example is correct, that is, the corresponding output is asserted
1371 assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManCo(pAig, pCex->iPo)) ) );
1372 }
1373
1374 /**Function*************************************************************
1375
1376 Synopsis [Stops the process of retuning values for internal nodes.]
1377
1378 Description [Should be called when probing is no longer needed]
1379
1380 SideEffects []
1381
1382 SeeAlso []
1383
1384 ***********************************************************************/
Aig_ManCounterExampleValueStop(Aig_Man_t * pAig)1385 void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
1386 {
1387 assert( pAig->pData2 != NULL ); // if this fail, we try to call this procedure more than once
1388 free( pAig->pData2 );
1389 pAig->pData2 = NULL;
1390 }
1391
1392 /**Function*************************************************************
1393
1394 Synopsis [Returns the value of the given object in the given timeframe.]
1395
1396 Description [Should be called to probe the value of an object with
1397 the given ID (iFrame is a 0-based number of a time frame - should not
1398 exceed the number of timeframes in the original counter-example).]
1399
1400 SideEffects []
1401
1402 SeeAlso []
1403
1404 ***********************************************************************/
Aig_ManCounterExampleValueLookup(Aig_Man_t * pAig,int Id,int iFrame)1405 int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame )
1406 {
1407 assert( Id >= 0 && Id < Aig_ManObjNumMax(pAig) );
1408 return Abc_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNumMax(pAig) * iFrame + Id );
1409 }
1410
1411 /**Function*************************************************************
1412
1413 Synopsis [Procedure to test the above code.]
1414
1415 Description []
1416
1417 SideEffects []
1418
1419 SeeAlso []
1420
1421 ***********************************************************************/
Aig_ManCounterExampleValueTest(Aig_Man_t * pAig,Abc_Cex_t * pCex)1422 void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex )
1423 {
1424 Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNumMax(pAig)/2 );
1425 int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
1426 printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
1427 Aig_ManCounterExampleValueStart( pAig, pCex );
1428 printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,
1429 Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) );
1430 Aig_ManCounterExampleValueStop( pAig );
1431 }
1432
1433 /**Function*************************************************************
1434
1435 Synopsis [Handle the counter-example.]
1436
1437 Description []
1438
1439 SideEffects []
1440
1441 SeeAlso []
1442
1443 ***********************************************************************/
Aig_ManSetPhase(Aig_Man_t * pAig)1444 void Aig_ManSetPhase( Aig_Man_t * pAig )
1445 {
1446 Aig_Obj_t * pObj;
1447 int i;
1448 // set the PI simulation information
1449 Aig_ManConst1( pAig )->fPhase = 1;
1450 Aig_ManForEachCi( pAig, pObj, i )
1451 pObj->fPhase = 0;
1452 // simulate internal nodes
1453 Aig_ManForEachNode( pAig, pObj, i )
1454 pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
1455 & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
1456 // simulate PO nodes
1457 Aig_ManForEachCo( pAig, pObj, i )
1458 pObj->fPhase = Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj);
1459 }
1460
1461
1462 /**Function*************************************************************
1463
1464 Synopsis [Collects muxes.]
1465
1466 Description []
1467
1468 SideEffects []
1469
1470 SeeAlso []
1471
1472 ***********************************************************************/
Aig_ManMuxesCollect(Aig_Man_t * pAig)1473 Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig )
1474 {
1475 Vec_Ptr_t * vMuxes;
1476 Aig_Obj_t * pObj;
1477 int i;
1478 vMuxes = Vec_PtrAlloc( 100 );
1479 Aig_ManForEachNode( pAig, pObj, i )
1480 if ( Aig_ObjIsMuxType(pObj) )
1481 Vec_PtrPush( vMuxes, pObj );
1482 return vMuxes;
1483 }
1484
1485 /**Function*************************************************************
1486
1487 Synopsis [Dereferences muxes.]
1488
1489 Description []
1490
1491 SideEffects []
1492
1493 SeeAlso []
1494
1495 ***********************************************************************/
Aig_ManMuxesDeref(Aig_Man_t * pAig,Vec_Ptr_t * vMuxes)1496 void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
1497 {
1498 Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
1499 int i;
1500 Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
1501 {
1502 if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
1503 {
1504 pNodeT->nRefs--;
1505 pNodeE->nRefs--;
1506 }
1507 else
1508 {
1509 pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
1510 pNodeC->nRefs--;
1511 }
1512 }
1513 }
1514
1515 /**Function*************************************************************
1516
1517 Synopsis [References muxes.]
1518
1519 Description []
1520
1521 SideEffects []
1522
1523 SeeAlso []
1524
1525 ***********************************************************************/
Aig_ManMuxesRef(Aig_Man_t * pAig,Vec_Ptr_t * vMuxes)1526 void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
1527 {
1528 Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
1529 int i;
1530 Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
1531 {
1532 if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
1533 {
1534 pNodeT->nRefs++;
1535 pNodeE->nRefs++;
1536 }
1537 else
1538 {
1539 pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
1540 pNodeC->nRefs++;
1541 }
1542 }
1543 }
1544
1545 /**Function*************************************************************
1546
1547 Synopsis [Complements the constraint outputs.]
1548
1549 Description []
1550
1551 SideEffects []
1552
1553 SeeAlso []
1554
1555 ***********************************************************************/
Aig_ManInvertConstraints(Aig_Man_t * pAig)1556 void Aig_ManInvertConstraints( Aig_Man_t * pAig )
1557 {
1558 Aig_Obj_t * pObj;
1559 int i;
1560 if ( Aig_ManConstrNum(pAig) == 0 )
1561 return;
1562 Saig_ManForEachPo( pAig, pObj, i )
1563 {
1564 if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) )
1565 Aig_ObjChild0Flip( pObj );
1566 }
1567 }
1568
1569 ////////////////////////////////////////////////////////////////////////
1570 /// END OF FILE ///
1571 ////////////////////////////////////////////////////////////////////////
1572
1573
1574 ABC_NAMESPACE_IMPL_END
1575
1576