abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ivyUtil.c
Go to the documentation of this file.
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 
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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) );
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 ***********************************************************************/
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 )
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 
824 
int TravId
Definition: ivy.h:76
static int Ivy_IsComplement(Ivy_Obj_t *p)
Definition: ivy.h:196
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
unsigned Level
Definition: ivy.h:84
unsigned * Ivy_ObjGetTruthStore(int ObjNum, Vec_Int_t *vTruth)
Definition: ivyUtil.c:134
unsigned * Ivy_ManCutTruth(Ivy_Man_t *p, Ivy_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vNodes, Vec_Int_t *vTruth)
Definition: ivyUtil.c:186
#define IVY_MAX(a, b)
Definition: ivy.h:183
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ivy_Obj_t * Ivy_ObjRecognizeMux(Ivy_Obj_t *pNode, Ivy_Obj_t **ppNodeT, Ivy_Obj_t **ppNodeE)
Definition: ivyUtil.c:517
static int Ivy_ObjLevelNew(Ivy_Obj_t *pObj)
Definition: ivy.h:279
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Ivy_ObjPrintVerbose(Ivy_Man_t *p, Ivy_Obj_t *pObj, int fHaig)
Definition: ivyUtil.c:629
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define Ivy_ManForEachPi(p, pObj, i)
ITERATORS ///.
Definition: ivy.h:387
int Ivy_ObjMffcLabel(Ivy_Man_t *p, Ivy_Obj_t *pNode)
Definition: ivyUtil.c:359
void Ivy_ManCleanTravId(Ivy_Man_t *p)
Definition: ivyUtil.c:63
#define Ivy_ObjForEachFanout(p, pObj, vArray, pFanout, i)
Definition: ivy.h:411
static int Ivy_ObjFaninId1(Ivy_Obj_t *pObj)
Definition: ivy.h:268
static int Ivy_ObjIsPi(Ivy_Obj_t *pObj)
Definition: ivy.h:236
#define Ivy_ManForEachPo(p, pObj, i)
Definition: ivy.h:390
#define Ivy_ManForEachLatch(p, pObj, i)
Definition: ivy.h:405
static int Ivy_LeafId(int Leaf)
Definition: ivy.h:215
char * memcpy()
static int Ivy_ManLatchNum(Ivy_Man_t *p)
Definition: ivy.h:221
int Id
Definition: ivy.h:75
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
void Ivy_ObjUpdateLevelR_rec(Ivy_Man_t *p, Ivy_Obj_t *pObj, int ReqNew)
Definition: ivyUtil.c:444
int nWords
Definition: abcNpn.c:127
static int Ivy_ObjIsLatch(Ivy_Obj_t *pObj)
Definition: ivy.h:241
static Ivy_Obj_t * Ivy_ObjFanin1(Ivy_Obj_t *pObj)
Definition: ivy.h:272
Vec_Int_t * Ivy_ManDfsSeq(Ivy_Man_t *p, Vec_Int_t **pvLatches)
Definition: ivyDfs.c:121
#define IVY_MIN(a, b)
MACRO DEFINITIONS ///.
Definition: ivy.h:182
static void Vec_IntGrow(Vec_Int_t *p, int nCapMin)
Definition: bblif.c:336
static Ivy_Obj_t * Ivy_ObjFanin0(Ivy_Obj_t *pObj)
Definition: ivy.h:271
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Ivy_ObjFaninId0(Ivy_Obj_t *pObj)
Definition: ivy.h:267
void Ivy_ObjUpdateLevel_rec(Ivy_Man_t *p, Ivy_Obj_t *pObj)
Definition: ivyUtil.c:382
#define Ivy_ManForEachCo(p, pObj, i)
Definition: ivy.h:399
void Ivy_ManCutTruthOne(Ivy_Man_t *p, Ivy_Obj_t *pNode, Vec_Int_t *vTruth, int nWords)
Definition: ivyUtil.c:150
int Ivy_ObjRefDeref(Ivy_Man_t *p, Ivy_Obj_t *pNode, int fReference, int fLabel)
Definition: ivyUtil.c:313
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
ABC_NAMESPACE_IMPL_START void Ivy_ManIncrementTravId(Ivy_Man_t *p)
DECLARATIONS ///.
Definition: ivyUtil.c:45
static int Ivy_ObjFaninC1(Ivy_Obj_t *pObj)
Definition: ivy.h:270
static Ivy_Obj_t * Ivy_ManObj(Ivy_Man_t *p, int i)
Definition: ivy.h:203
short nSize
Definition: ivy.h:159
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int Ivy_CutTruthPrint(Ivy_Man_t *p, Ivy_Cut_t *pCut, unsigned uTruth)
Definition: ivyUtil.c:771
static int Ivy_ObjRefs(Ivy_Obj_t *pObj)
Definition: ivy.h:264
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
void Ivy_ManCollectCut_rec(Ivy_Man_t *p, Ivy_Obj_t *pNode, Vec_Int_t *vNodes)
Definition: ivyUtil.c:83
int pArray[IVY_CUT_INPUT]
Definition: ivy.h:161
Vec_Int_t * Ivy_ManLatches(Ivy_Man_t *p)
Definition: ivyUtil.c:227
Definition: ivy.h:73
static Ivy_Obj_t * Ivy_Regular(Ivy_Obj_t *p)
Definition: ivy.h:193
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Ivy_ObjIsCo(Ivy_Obj_t *pObj)
Definition: ivy.h:239
static int Counter
static int Ivy_ObjIsNode(Ivy_Obj_t *pObj)
Definition: ivy.h:245
int Ivy_ObjIsMuxType(Ivy_Obj_t *pNode)
Definition: ivyUtil.c:479
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
static Ivy_Obj_t * Ivy_ObjChild0(Ivy_Obj_t *pObj)
Definition: ivy.h:273
void Ivy_ManPrintVerbose(Ivy_Man_t *p, int fHaig)
Definition: ivyUtil.c:714
unsigned fMarkA
Definition: ivy.h:78
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition: ivy.h:46
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static int Ivy_ObjIsAnd(Ivy_Obj_t *pObj)
Definition: ivy.h:242
static int Ivy_ObjIsExor(Ivy_Obj_t *pObj)
Definition: ivy.h:243
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Ivy_ObjIsConst1(Ivy_Obj_t *pObj)
Definition: ivy.h:233
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
void Ivy_ManCollectCut(Ivy_Man_t *p, Ivy_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vNodes)
Definition: ivyUtil.c:106
static Ivy_Obj_t * Ivy_Not(Ivy_Obj_t *p)
Definition: ivy.h:194
static Ivy_Obj_t * Ivy_NotCond(Ivy_Obj_t *p, int c)
Definition: ivy.h:195
#define Ivy_ManForEachNodeVec(p, vIds, pObj, i)
Definition: ivy.h:408
static int Ivy_ObjIsBuf(Ivy_Obj_t *pObj)
Definition: ivy.h:244
int Ivy_ManResetLevels_rec(Ivy_Obj_t *pObj)
Definition: ivyUtil.c:269
static Ivy_Obj_t * Ivy_ObjChild1(Ivy_Obj_t *pObj)
Definition: ivy.h:274
static int Ivy_ObjIsPo(Ivy_Obj_t *pObj)
Definition: ivy.h:237
int Ivy_ManLevels(Ivy_Man_t *p)
Definition: ivyUtil.c:249
#define assert(ex)
Definition: util_old.h:213
static int Ivy_ObjIsCi(Ivy_Obj_t *pObj)
Definition: ivy.h:238
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int Ivy_CutTruthPrint2(Ivy_Man_t *p, Ivy_Cut_t *pCut, unsigned uTruth)
Definition: ivyUtil.c:749
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Ivy_Obj_t * Ivy_ObjReal(Ivy_Obj_t *pObj)
Definition: ivyUtil.c:609
void Ivy_ManResetLevels(Ivy_Man_t *p)
Definition: ivyUtil.c:292
static int Ivy_LeafLat(int Leaf)
Definition: ivy.h:216
static int Ivy_ObjFaninC0(Ivy_Obj_t *pObj)
Definition: ivy.h:269
int nRefs
Definition: ivy.h:85
static int Ivy_ObjId(Ivy_Obj_t *pObj)
Definition: ivy.h:260
int Ivy_ObjLevelRNew(Ivy_Man_t *p, Ivy_Obj_t *pObj)
Definition: ivyUtil.c:417
static void Ivy_ObjSetTravIdCurrent(Ivy_Man_t *p, Ivy_Obj_t *pObj)
Definition: ivy.h:255
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Ivy_Obj_t * pEquiv
Definition: ivy.h:93