1 /**CFile****************************************************************
2
3 FileName [ivyUtil.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [And-Inverter Graph package.]
8
9 Synopsis [Various procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - May 11, 2006.]
16
17 Revision [$Id: ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "ivy.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Increments the current traversal ID of the network.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Ivy_ManIncrementTravId(Ivy_Man_t * p)45 void Ivy_ManIncrementTravId( Ivy_Man_t * p )
46 {
47 if ( p->nTravIds >= (1<<30)-1 - 1000 )
48 Ivy_ManCleanTravId( p );
49 p->nTravIds++;
50 }
51
52 /**Function*************************************************************
53
54 Synopsis [Sets the DFS ordering of the nodes.]
55
56 Description []
57
58 SideEffects []
59
60 SeeAlso []
61
62 ***********************************************************************/
Ivy_ManCleanTravId(Ivy_Man_t * p)63 void Ivy_ManCleanTravId( Ivy_Man_t * p )
64 {
65 Ivy_Obj_t * pObj;
66 int i;
67 p->nTravIds = 1;
68 Ivy_ManForEachObj( p, pObj, i )
69 pObj->TravId = 0;
70 }
71
72 /**Function*************************************************************
73
74 Synopsis [Computes truth table of the cut.]
75
76 Description []
77
78 SideEffects []
79
80 SeeAlso []
81
82 ***********************************************************************/
Ivy_ManCollectCut_rec(Ivy_Man_t * p,Ivy_Obj_t * pNode,Vec_Int_t * vNodes)83 void Ivy_ManCollectCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
84 {
85 if ( pNode->fMarkA )
86 return;
87 pNode->fMarkA = 1;
88 assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) );
89 Ivy_ManCollectCut_rec( p, Ivy_ObjFanin0(pNode), vNodes );
90 Ivy_ManCollectCut_rec( p, Ivy_ObjFanin1(pNode), vNodes );
91 Vec_IntPush( vNodes, pNode->Id );
92 }
93
94 /**Function*************************************************************
95
96 Synopsis [Computes truth table of the cut.]
97
98 Description [Does not modify the array of leaves. Uses array vTruth to store
99 temporary truth tables. The returned pointer should be used immediately.]
100
101 SideEffects []
102
103 SeeAlso []
104
105 ***********************************************************************/
Ivy_ManCollectCut(Ivy_Man_t * p,Ivy_Obj_t * pRoot,Vec_Int_t * vLeaves,Vec_Int_t * vNodes)106 void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
107 {
108 int i, Leaf;
109 // collect and mark the leaves
110 Vec_IntClear( vNodes );
111 Vec_IntForEachEntry( vLeaves, Leaf, i )
112 {
113 Vec_IntPush( vNodes, Leaf );
114 Ivy_ManObj(p, Leaf)->fMarkA = 1;
115 }
116 // collect and mark the nodes
117 Ivy_ManCollectCut_rec( p, pRoot, vNodes );
118 // clean the nodes
119 Vec_IntForEachEntry( vNodes, Leaf, i )
120 Ivy_ManObj(p, Leaf)->fMarkA = 0;
121 }
122
123 /**Function*************************************************************
124
125 Synopsis [Returns the pointer to the truth table.]
126
127 Description []
128
129 SideEffects []
130
131 SeeAlso []
132
133 ***********************************************************************/
Ivy_ObjGetTruthStore(int ObjNum,Vec_Int_t * vTruth)134 unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth )
135 {
136 return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum;
137 }
138
139 /**Function*************************************************************
140
141 Synopsis [Computes truth table of the cut.]
142
143 Description []
144
145 SideEffects []
146
147 SeeAlso []
148
149 ***********************************************************************/
Ivy_ManCutTruthOne(Ivy_Man_t * p,Ivy_Obj_t * pNode,Vec_Int_t * vTruth,int nWords)150 void Ivy_ManCutTruthOne( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
151 {
152 unsigned * pTruth, * pTruth0, * pTruth1;
153 int i;
154 pTruth = Ivy_ObjGetTruthStore( pNode->TravId, vTruth );
155 pTruth0 = Ivy_ObjGetTruthStore( Ivy_ObjFanin0(pNode)->TravId, vTruth );
156 pTruth1 = Ivy_ObjGetTruthStore( Ivy_ObjFanin1(pNode)->TravId, vTruth );
157 if ( Ivy_ObjIsExor(pNode) )
158 for ( i = 0; i < nWords; i++ )
159 pTruth[i] = pTruth0[i] ^ pTruth1[i];
160 else if ( !Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) )
161 for ( i = 0; i < nWords; i++ )
162 pTruth[i] = pTruth0[i] & pTruth1[i];
163 else if ( !Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) )
164 for ( i = 0; i < nWords; i++ )
165 pTruth[i] = pTruth0[i] & ~pTruth1[i];
166 else if ( Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) )
167 for ( i = 0; i < nWords; i++ )
168 pTruth[i] = ~pTruth0[i] & pTruth1[i];
169 else // if ( Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) )
170 for ( i = 0; i < nWords; i++ )
171 pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
172 }
173
174 /**Function*************************************************************
175
176 Synopsis [Computes truth table of the cut.]
177
178 Description [Does not modify the array of leaves. Uses array vTruth to store
179 temporary truth tables. The returned pointer should be used immediately.]
180
181 SideEffects []
182
183 SeeAlso []
184
185 ***********************************************************************/
Ivy_ManCutTruth(Ivy_Man_t * p,Ivy_Obj_t * pRoot,Vec_Int_t * vLeaves,Vec_Int_t * vNodes,Vec_Int_t * vTruth)186 unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
187 {
188 static unsigned uTruths[8][8] = { // elementary truth tables
189 { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
190 { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
191 { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
192 { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
193 { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
194 { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
195 { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
196 { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
197 };
198 int i, Leaf;
199 // collect the cut
200 Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes );
201 // set the node numbers
202 Vec_IntForEachEntry( vNodes, Leaf, i )
203 Ivy_ManObj(p, Leaf)->TravId = i;
204 // alloc enough memory
205 Vec_IntClear( vTruth );
206 Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
207 // set the elementary truth tables
208 Vec_IntForEachEntry( vLeaves, Leaf, i )
209 memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
210 // compute truths for other nodes
211 Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
212 Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 );
213 return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth );
214 }
215
216 /**Function*************************************************************
217
218 Synopsis [Collect the latches.]
219
220 Description []
221
222 SideEffects []
223
224 SeeAlso []
225
226 ***********************************************************************/
Ivy_ManLatches(Ivy_Man_t * p)227 Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
228 {
229 Vec_Int_t * vLatches;
230 Ivy_Obj_t * pObj;
231 int i;
232 vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
233 Ivy_ManForEachLatch( p, pObj, i )
234 Vec_IntPush( vLatches, pObj->Id );
235 return vLatches;
236 }
237
238 /**Function*************************************************************
239
240 Synopsis [Collect the latches.]
241
242 Description []
243
244 SideEffects []
245
246 SeeAlso []
247
248 ***********************************************************************/
Ivy_ManLevels(Ivy_Man_t * p)249 int Ivy_ManLevels( Ivy_Man_t * p )
250 {
251 Ivy_Obj_t * pObj;
252 int i, LevelMax = 0;
253 Ivy_ManForEachPo( p, pObj, i )
254 LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
255 return LevelMax;
256 }
257
258 /**Function*************************************************************
259
260 Synopsis [Collect the latches.]
261
262 Description []
263
264 SideEffects []
265
266 SeeAlso []
267
268 ***********************************************************************/
Ivy_ManResetLevels_rec(Ivy_Obj_t * pObj)269 int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj )
270 {
271 if ( pObj->Level || Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
272 return pObj->Level;
273 if ( Ivy_ObjIsBuf(pObj) )
274 return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
275 assert( Ivy_ObjIsNode(pObj) );
276 Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
277 Ivy_ManResetLevels_rec( Ivy_ObjFanin1(pObj) );
278 return pObj->Level = Ivy_ObjLevelNew( pObj );
279 }
280
281 /**Function*************************************************************
282
283 Synopsis [Collect the latches.]
284
285 Description []
286
287 SideEffects []
288
289 SeeAlso []
290
291 ***********************************************************************/
Ivy_ManResetLevels(Ivy_Man_t * p)292 void Ivy_ManResetLevels( Ivy_Man_t * p )
293 {
294 Ivy_Obj_t * pObj;
295 int i;
296 Ivy_ManForEachObj( p, pObj, i )
297 pObj->Level = 0;
298 Ivy_ManForEachCo( p, pObj, i )
299 Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
300 }
301
302 /**Function*************************************************************
303
304 Synopsis [References/references the node and returns MFFC size.]
305
306 Description []
307
308 SideEffects []
309
310 SeeAlso []
311
312 ***********************************************************************/
Ivy_ObjRefDeref(Ivy_Man_t * p,Ivy_Obj_t * pNode,int fReference,int fLabel)313 int Ivy_ObjRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
314 {
315 Ivy_Obj_t * pNode0, * pNode1;
316 int Counter;
317 // label visited nodes
318 if ( fLabel )
319 Ivy_ObjSetTravIdCurrent( p, pNode );
320 // skip the CI
321 if ( Ivy_ObjIsPi(pNode) )
322 return 0;
323 assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) || Ivy_ObjIsLatch(pNode) );
324 // process the internal node
325 pNode0 = Ivy_ObjFanin0(pNode);
326 pNode1 = Ivy_ObjFanin1(pNode);
327 Counter = Ivy_ObjIsNode(pNode);
328 if ( fReference )
329 {
330 if ( pNode0->nRefs++ == 0 )
331 Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
332 if ( pNode1 && pNode1->nRefs++ == 0 )
333 Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
334 }
335 else
336 {
337 assert( pNode0->nRefs > 0 );
338 assert( pNode1 == NULL || pNode1->nRefs > 0 );
339 if ( --pNode0->nRefs == 0 )
340 Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
341 if ( pNode1 && --pNode1->nRefs == 0 )
342 Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
343 }
344 return Counter;
345 }
346
347
348 /**Function*************************************************************
349
350 Synopsis [Labels MFFC with the current label.]
351
352 Description []
353
354 SideEffects []
355
356 SeeAlso []
357
358 ***********************************************************************/
Ivy_ObjMffcLabel(Ivy_Man_t * p,Ivy_Obj_t * pNode)359 int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
360 {
361 int nConeSize1, nConeSize2;
362 assert( !Ivy_IsComplement( pNode ) );
363 assert( Ivy_ObjIsNode( pNode ) );
364 nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference
365 nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference
366 assert( nConeSize1 == nConeSize2 );
367 assert( nConeSize1 > 0 );
368 return nConeSize1;
369 }
370
371 /**Function*************************************************************
372
373 Synopsis [Recursively updates fanout levels.]
374
375 Description []
376
377 SideEffects []
378
379 SeeAlso []
380
381 ***********************************************************************/
Ivy_ObjUpdateLevel_rec(Ivy_Man_t * p,Ivy_Obj_t * pObj)382 void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
383 {
384 Ivy_Obj_t * pFanout;
385 Vec_Ptr_t * vFanouts;
386 int i, LevelNew;
387 assert( p->fFanout );
388 assert( Ivy_ObjIsNode(pObj) );
389 vFanouts = Vec_PtrAlloc( 10 );
390 Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
391 {
392 if ( Ivy_ObjIsCo(pFanout) )
393 {
394 // assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax );
395 continue;
396 }
397 LevelNew = Ivy_ObjLevelNew( pFanout );
398 if ( (int)pFanout->Level == LevelNew )
399 continue;
400 pFanout->Level = LevelNew;
401 Ivy_ObjUpdateLevel_rec( p, pFanout );
402 }
403 Vec_PtrFree( vFanouts );
404 }
405
406 /**Function*************************************************************
407
408 Synopsis [Compute the new required level.]
409
410 Description []
411
412 SideEffects []
413
414 SeeAlso []
415
416 ***********************************************************************/
Ivy_ObjLevelRNew(Ivy_Man_t * p,Ivy_Obj_t * pObj)417 int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj )
418 {
419 Ivy_Obj_t * pFanout;
420 Vec_Ptr_t * vFanouts;
421 int i, Required, LevelNew = 1000000;
422 assert( p->fFanout && p->vRequired );
423 vFanouts = Vec_PtrAlloc( 10 );
424 Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
425 {
426 Required = Vec_IntEntry(p->vRequired, pFanout->Id);
427 LevelNew = IVY_MIN( LevelNew, Required );
428 }
429 Vec_PtrFree( vFanouts );
430 return LevelNew - 1;
431 }
432
433 /**Function*************************************************************
434
435 Synopsis [Recursively updates fanout levels.]
436
437 Description []
438
439 SideEffects []
440
441 SeeAlso []
442
443 ***********************************************************************/
Ivy_ObjUpdateLevelR_rec(Ivy_Man_t * p,Ivy_Obj_t * pObj,int ReqNew)444 void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew )
445 {
446 Ivy_Obj_t * pFanin;
447 if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
448 return;
449 assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
450 // process the first fanin
451 pFanin = Ivy_ObjFanin0(pObj);
452 if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
453 {
454 Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
455 Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
456 }
457 if ( Ivy_ObjIsBuf(pObj) )
458 return;
459 // process the second fanin
460 pFanin = Ivy_ObjFanin1(pObj);
461 if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
462 {
463 Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
464 Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
465 }
466 }
467
468 /**Function*************************************************************
469
470 Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
471
472 Description []
473
474 SideEffects []
475
476 SeeAlso []
477
478 ***********************************************************************/
Ivy_ObjIsMuxType(Ivy_Obj_t * pNode)479 int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
480 {
481 Ivy_Obj_t * pNode0, * pNode1;
482 // check that the node is regular
483 assert( !Ivy_IsComplement(pNode) );
484 // if the node is not AND, this is not MUX
485 if ( !Ivy_ObjIsAnd(pNode) )
486 return 0;
487 // if the children are not complemented, this is not MUX
488 if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
489 return 0;
490 // get children
491 pNode0 = Ivy_ObjFanin0(pNode);
492 pNode1 = Ivy_ObjFanin1(pNode);
493 // if the children are not ANDs, this is not MUX
494 if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
495 return 0;
496 // otherwise the node is MUX iff it has a pair of equal grandchildren
497 return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
498 (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
499 (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
500 (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
501 }
502
503 /**Function*************************************************************
504
505 Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
506
507 Description [If the node is a MUX, returns the control variable C.
508 Assigns nodes T and E to be the then and else variables of the MUX.
509 Node C is never complemented. Nodes T and E can be complemented.
510 This function also recognizes EXOR/NEXOR gates as MUXes.]
511
512 SideEffects []
513
514 SeeAlso []
515
516 ***********************************************************************/
Ivy_ObjRecognizeMux(Ivy_Obj_t * pNode,Ivy_Obj_t ** ppNodeT,Ivy_Obj_t ** ppNodeE)517 Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
518 {
519 Ivy_Obj_t * pNode0, * pNode1;
520 assert( !Ivy_IsComplement(pNode) );
521 assert( Ivy_ObjIsMuxType(pNode) );
522 // get children
523 pNode0 = Ivy_ObjFanin0(pNode);
524 pNode1 = Ivy_ObjFanin1(pNode);
525 // find the control variable
526 // if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
527 if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
528 {
529 // if ( Fraig_IsComplement(pNode1->p1) )
530 if ( Ivy_ObjFaninC0(pNode0) )
531 { // pNode2->p1 is positive phase of C
532 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
533 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
534 return Ivy_ObjChild0(pNode1);//pNode2->p1;
535 }
536 else
537 { // pNode1->p1 is positive phase of C
538 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
539 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
540 return Ivy_ObjChild0(pNode0);//pNode1->p1;
541 }
542 }
543 // else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
544 else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
545 {
546 // if ( Fraig_IsComplement(pNode1->p1) )
547 if ( Ivy_ObjFaninC0(pNode0) )
548 { // pNode2->p2 is positive phase of C
549 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
550 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
551 return Ivy_ObjChild1(pNode1);//pNode2->p2;
552 }
553 else
554 { // pNode1->p1 is positive phase of C
555 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
556 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
557 return Ivy_ObjChild0(pNode0);//pNode1->p1;
558 }
559 }
560 // else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
561 else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
562 {
563 // if ( Fraig_IsComplement(pNode1->p2) )
564 if ( Ivy_ObjFaninC1(pNode0) )
565 { // pNode2->p1 is positive phase of C
566 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
567 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
568 return Ivy_ObjChild0(pNode1);//pNode2->p1;
569 }
570 else
571 { // pNode1->p2 is positive phase of C
572 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
573 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
574 return Ivy_ObjChild1(pNode0);//pNode1->p2;
575 }
576 }
577 // else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
578 else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
579 {
580 // if ( Fraig_IsComplement(pNode1->p2) )
581 if ( Ivy_ObjFaninC1(pNode0) )
582 { // pNode2->p2 is positive phase of C
583 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
584 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
585 return Ivy_ObjChild1(pNode1);//pNode2->p2;
586 }
587 else
588 { // pNode1->p2 is positive phase of C
589 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
590 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
591 return Ivy_ObjChild1(pNode0);//pNode1->p2;
592 }
593 }
594 assert( 0 ); // this is not MUX
595 return NULL;
596 }
597
598 /**Function*************************************************************
599
600 Synopsis [Returns the real fanin.]
601
602 Description []
603
604 SideEffects []
605
606 SeeAlso []
607
608 ***********************************************************************/
Ivy_ObjReal(Ivy_Obj_t * pObj)609 Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
610 {
611 Ivy_Obj_t * pFanin;
612 if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
613 return pObj;
614 pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
615 return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
616 }
617
618 /**Function*************************************************************
619
620 Synopsis [Prints node in HAIG.]
621
622 Description []
623
624 SideEffects []
625
626 SeeAlso []
627
628 ***********************************************************************/
Ivy_ObjPrintVerbose(Ivy_Man_t * p,Ivy_Obj_t * pObj,int fHaig)629 void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig )
630 {
631 Ivy_Obj_t * pTemp;
632 int fShowFanouts = 0;
633 assert( !Ivy_IsComplement(pObj) );
634 printf( "Node %5d : ", Ivy_ObjId(pObj) );
635 if ( Ivy_ObjIsConst1(pObj) )
636 printf( "constant 1" );
637 else if ( Ivy_ObjIsPi(pObj) )
638 printf( "PI" );
639 else if ( Ivy_ObjIsPo(pObj) )
640 printf( "PO" );
641 else if ( Ivy_ObjIsLatch(pObj) )
642 printf( "latch (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
643 else if ( Ivy_ObjIsBuf(pObj) )
644 printf( "buffer (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
645 else
646 printf( "AND( %5d%s, %5d%s )",
647 Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "),
648 Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") );
649 printf( " (refs = %3d)", Ivy_ObjRefs(pObj) );
650 if ( fShowFanouts )
651 {
652 Vec_Ptr_t * vFanouts;
653 Ivy_Obj_t * pFanout;
654 int i;
655 vFanouts = Vec_PtrAlloc( 10 );
656 printf( "\nFanouts:\n" );
657 Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
658 {
659 printf( " " );
660 printf( "Node %5d : ", Ivy_ObjId(pFanout) );
661 if ( Ivy_ObjIsPo(pFanout) )
662 printf( "PO" );
663 else if ( Ivy_ObjIsLatch(pFanout) )
664 printf( "latch (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
665 else if ( Ivy_ObjIsBuf(pFanout) )
666 printf( "buffer (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
667 else
668 printf( "AND( %5d%s, %5d%s )",
669 Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " "),
670 Ivy_ObjFanin1(pFanout)->Id, (Ivy_ObjFaninC1(pFanout)? "\'" : " ") );
671 printf( "\n" );
672 }
673 Vec_PtrFree( vFanouts );
674 return;
675 }
676 if ( !fHaig )
677 {
678 if ( pObj->pEquiv == NULL )
679 printf( " HAIG node not given" );
680 else
681 printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") );
682 return;
683 }
684 if ( pObj->pEquiv == NULL )
685 return;
686 // there are choices
687 if ( Ivy_ObjRefs(pObj) > 0 )
688 {
689 // print equivalence class
690 printf( " { %5d ", pObj->Id );
691 assert( !Ivy_IsComplement(pObj->pEquiv) );
692 for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
693 printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") );
694 printf( " }" );
695 return;
696 }
697 // this is a secondary node
698 for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) );
699 assert( Ivy_ObjRefs(pTemp) > 0 );
700 printf( " class of %d", pTemp->Id );
701 }
702
703 /**Function*************************************************************
704
705 Synopsis [Prints node in HAIG.]
706
707 Description []
708
709 SideEffects []
710
711 SeeAlso []
712
713 ***********************************************************************/
Ivy_ManPrintVerbose(Ivy_Man_t * p,int fHaig)714 void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
715 {
716 Vec_Int_t * vNodes;
717 Ivy_Obj_t * pObj;
718 int i;
719 printf( "PIs: " );
720 Ivy_ManForEachPi( p, pObj, i )
721 printf( " %d", pObj->Id );
722 printf( "\n" );
723 printf( "POs: " );
724 Ivy_ManForEachPo( p, pObj, i )
725 printf( " %d", pObj->Id );
726 printf( "\n" );
727 printf( "Latches: " );
728 Ivy_ManForEachLatch( p, pObj, i )
729 printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
730 printf( "\n" );
731 vNodes = Ivy_ManDfsSeq( p, NULL );
732 Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
733 Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" );
734 printf( "\n" );
735 Vec_IntFree( vNodes );
736 }
737
738 /**Function*************************************************************
739
740 Synopsis [Performs incremental rewriting of the AIG.]
741
742 Description []
743
744 SideEffects []
745
746 SeeAlso []
747
748 ***********************************************************************/
Ivy_CutTruthPrint2(Ivy_Man_t * p,Ivy_Cut_t * pCut,unsigned uTruth)749 int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
750 {
751 int i;
752 printf( "Trying cut : {" );
753 for ( i = 0; i < pCut->nSize; i++ )
754 printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
755 printf( " } " );
756 Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
757 return 0;
758 }
759
760 /**Function*************************************************************
761
762 Synopsis [Performs incremental rewriting of the AIG.]
763
764 Description []
765
766 SideEffects []
767
768 SeeAlso []
769
770 ***********************************************************************/
Ivy_CutTruthPrint(Ivy_Man_t * p,Ivy_Cut_t * pCut,unsigned uTruth)771 int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
772 {
773 Vec_Ptr_t * vArray;
774 Ivy_Obj_t * pObj, * pFanout;
775 int nLatches = 0;
776 int nPresent = 0;
777 int i, k;
778 int fVerbose = 0;
779
780 if ( fVerbose )
781 printf( "Trying cut : {" );
782 for ( i = 0; i < pCut->nSize; i++ )
783 {
784 if ( fVerbose )
785 printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
786 nLatches += Ivy_LeafLat(pCut->pArray[i]);
787 }
788 if ( fVerbose )
789 printf( " } " );
790 if ( fVerbose )
791 printf( "Latches = %d. ", nLatches );
792
793 // check if there are latches on the fanout edges
794 vArray = Vec_PtrAlloc( 100 );
795 for ( i = 0; i < pCut->nSize; i++ )
796 {
797 pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) );
798 Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k )
799 {
800 if ( Ivy_ObjIsLatch(pFanout) )
801 {
802 nPresent++;
803 break;
804 }
805 }
806 }
807 Vec_PtrSize( vArray );
808 if ( fVerbose )
809 {
810 printf( "Present = %d. ", nPresent );
811 if ( nLatches > nPresent )
812 printf( "Clauses = %d. ", 2*(nLatches - nPresent) );
813 printf( "\n" );
814 }
815 return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0;
816 }
817
818 ////////////////////////////////////////////////////////////////////////
819 /// END OF FILE ///
820 ////////////////////////////////////////////////////////////////////////
821
822
823 ABC_NAMESPACE_IMPL_END
824
825