abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigWnd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigWnd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Sequential windowing.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigWnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.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 [Returns the array of PI/internal nodes.]
37 
38  Description [Marks all the visited nodes with the current ID.
39  Does not collect constant node and PO/LI nodes.]
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void Saig_ManWindowOutline_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Vec_Ptr_t * vNodes, int * pDists )
47 {
48  Aig_Obj_t * pMatch, * pFanout;
49  int fCollected, iFanout = -1, i;
50  if ( nDist == 0 )
51  return;
52  if ( pDists[pObj->Id] >= nDist )
53  return;
54  pDists[pObj->Id] = nDist;
55  fCollected = Aig_ObjIsTravIdCurrent( p, pObj );
56  Aig_ObjSetTravIdCurrent( p, pObj );
57  if ( Aig_ObjIsConst1(pObj) )
58  return;
59  if ( Saig_ObjIsPo(p, pObj) )
60  return;
61  if ( Saig_ObjIsLi(p, pObj) )
62  {
63  pMatch = Saig_ObjLiToLo( p, pObj );
64  if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
65  Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
66  Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
67  return;
68  }
69  if ( !fCollected )
70  Vec_PtrPush( vNodes, pObj );
71  if ( Saig_ObjIsPi(p, pObj) )
72  return;
73  if ( Saig_ObjIsLo(p, pObj) )
74  {
75  pMatch = Saig_ObjLoToLi( p, pObj );
76  if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
77  Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
78  Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
79  Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
80  return;
81  }
82  assert( Aig_ObjIsNode(pObj) );
83  Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
84  Saig_ManWindowOutline_rec( p, Aig_ObjFanin1(pObj), nDist-1, vNodes, pDists );
85  Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
86  Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
87 }
88 
89 /**Function*************************************************************
90 
91  Synopsis [Returns the array of PI/internal nodes.]
92 
93  Description [Marks all the visited nodes with the current ID.]
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
100 Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
101 {
102  Vec_Ptr_t * vNodes;
103  Aig_Obj_t * pObjLi, * pObjLo;
104  int * pDists, i;
105  pDists = ABC_CALLOC( int, Aig_ManObjNumMax(p) );
106  vNodes = Vec_PtrAlloc( 1000 );
107  Aig_ManIncrementTravId( p );
108  Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists );
109  Vec_PtrSort( vNodes, (int (*)(void))Aig_ObjCompareIdIncrease );
110  // make sure LI/LO are labeled/unlabeled mutually
111  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
112  assert( Aig_ObjIsTravIdCurrent(p, pObjLi) ==
113  Aig_ObjIsTravIdCurrent(p, pObjLo) );
114  ABC_FREE( pDists );
115  return vNodes;
116 }
117 
118 /**Function*************************************************************
119 
120  Synopsis [Returns 1 if the node has unlabeled fanout.]
121 
122  Description []
123 
124  SideEffects []
125 
126  SeeAlso []
127 
128 ***********************************************************************/
129 Aig_Obj_t * Saig_ObjHasUnlabeledFanout( Aig_Man_t * p, Aig_Obj_t * pObj )
130 {
131  Aig_Obj_t * pFanout;
132  int iFanout = -1, i;
133  Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
134  if ( Saig_ObjIsPo(p, pFanout) || !Aig_ObjIsTravIdCurrent(p, pFanout) )
135  return pFanout;
136  return NULL;
137 }
138 
139 /**Function*************************************************************
140 
141  Synopsis [Collects primary inputs.]
142 
143  Description []
144 
145  SideEffects []
146 
147  SeeAlso []
148 
149 ***********************************************************************/
150 Vec_Ptr_t * Saig_ManWindowCollectPis( Aig_Man_t * p, Vec_Ptr_t * vNodes )
151 {
152  Vec_Ptr_t * vNodesPi;
153  Aig_Obj_t * pObj, * pMatch, * pFanin;
154  int i;
155  vNodesPi = Vec_PtrAlloc( 1000 );
156  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
157  {
158  if ( Saig_ObjIsPi(p, pObj) )
159  {
160  assert( pObj->pData == NULL );
161  Vec_PtrPush( vNodesPi, pObj );
162  }
163  else if ( Saig_ObjIsLo(p, pObj) )
164  {
165  pMatch = Saig_ObjLoToLi( p, pObj );
166  pFanin = Aig_ObjFanin0(pMatch);
167  if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
168  Vec_PtrPush( vNodesPi, pFanin );
169  }
170  else
171  {
172  assert( Aig_ObjIsNode(pObj) );
173  pFanin = Aig_ObjFanin0(pObj);
174  if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
175  Vec_PtrPush( vNodesPi, pFanin );
176  pFanin = Aig_ObjFanin1(pObj);
177  if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
178  Vec_PtrPush( vNodesPi, pFanin );
179  }
180  }
181  return vNodesPi;
182 }
183 
184 /**Function*************************************************************
185 
186  Synopsis [Collects primary outputs.]
187 
188  Description []
189 
190  SideEffects []
191 
192  SeeAlso []
193 
194 ***********************************************************************/
195 Vec_Ptr_t * Saig_ManWindowCollectPos( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t ** pvPointers )
196 {
197  Vec_Ptr_t * vNodesPo;
198  Aig_Obj_t * pObj, * pPointer;
199  int i;
200  vNodesPo = Vec_PtrAlloc( 1000 );
201  if ( pvPointers )
202  *pvPointers = Vec_PtrAlloc( 1000 );
203  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
204  {
205  if ( (pPointer = Saig_ObjHasUnlabeledFanout(p, pObj)) )
206  {
207  Vec_PtrPush( vNodesPo, pObj );
208  if ( pvPointers )
209  Vec_PtrPush( *pvPointers, pPointer );
210  }
211  }
212  return vNodesPo;
213 }
214 
215 /**Function*************************************************************
216 
217  Synopsis [Extracts the window AIG from the AIG manager.]
218 
219  Description []
220 
221  SideEffects []
222 
223  SeeAlso []
224 
225 ***********************************************************************/
226 Aig_Man_t * Saig_ManWindowExtractNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes )
227 {
228  Aig_Man_t * pNew;
229  Aig_Obj_t * pObj, * pMatch;
230  Vec_Ptr_t * vNodesPi, * vNodesPo;
231  int i, nRegCount;
232  Aig_ManCleanData( p );
233  // create the new manager
234  pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
235  pNew->pName = Abc_UtilStrsav( "wnd" );
236  pNew->pSpec = NULL;
237  // map constant nodes
238  pObj = Aig_ManConst1( p );
239  pObj->pData = Aig_ManConst1( pNew );
240  // create real PIs
241  vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
242  Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i )
243  pObj->pData = Aig_ObjCreateCi(pNew);
244  Vec_PtrFree( vNodesPi );
245  // create register outputs
246  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
247  {
248  if ( Saig_ObjIsLo(p, pObj) )
249  pObj->pData = Aig_ObjCreateCi(pNew);
250  }
251  // create internal nodes
252  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
253  {
254  if ( Aig_ObjIsNode(pObj) )
255  pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
256  }
257  // create POs
258  vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
259  Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i )
260  Aig_ObjCreateCo( pNew, (Aig_Obj_t *)pObj->pData );
261  Vec_PtrFree( vNodesPo );
262  // create register inputs
263  nRegCount = 0;
264  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
265  {
266  if ( Saig_ObjIsLo(p, pObj) )
267  {
268  pMatch = Saig_ObjLoToLi( p, pObj );
269  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
270  nRegCount++;
271  }
272  }
273  Aig_ManSetRegNum( pNew, nRegCount );
274  Aig_ManCleanup( pNew );
275  return pNew;
276 }
277 
278 static void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall,
279  Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode );
280 
281 /**Function*************************************************************
282 
283  Synopsis [Adds nodes for the big manager.]
284 
285  Description []
286 
287  SideEffects []
288 
289  SeeAlso []
290 
291 ***********************************************************************/
292 void Saig_ManWindowInsertBig_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjBig,
293  Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode )
294 {
295  Aig_Obj_t * pMatch;
296  if ( pObjBig->pData )
297  return;
298  if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vBigNode2SmallPo, pObjBig->Id )) )
299  {
300  Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pMatch), vBigNode2SmallPo, vSmallPi2BigNode );
301  pObjBig->pData = Aig_ObjChild0Copy(pMatch);
302  return;
303  }
304  assert( Aig_ObjIsNode(pObjBig) );
305  Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
306  Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin1(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
307  pObjBig->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjBig), Aig_ObjChild1Copy(pObjBig) );
308 }
309 
310 /**Function*************************************************************
311 
312  Synopsis [Adds nodes for the small manager.]
313 
314  Description []
315 
316  SideEffects []
317 
318  SeeAlso []
319 
320 ***********************************************************************/
321 void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall,
322  Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode )
323 {
324  Aig_Obj_t * pMatch;
325  if ( pObjSmall->pData )
326  return;
327  if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vSmallPi2BigNode, pObjSmall->Id )) )
328  {
329  Saig_ManWindowInsertBig_rec( pNew, pMatch, vBigNode2SmallPo, vSmallPi2BigNode );
330  pObjSmall->pData = pMatch->pData;
331  return;
332  }
333  assert( Aig_ObjIsNode(pObjSmall) );
334  Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
335  Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin1(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
336  pObjSmall->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjSmall), Aig_ObjChild1Copy(pObjSmall) );
337 }
338 
339 /**Function*************************************************************
340 
341  Synopsis [Extracts the network from the AIG manager.]
342 
343  Description []
344 
345  SideEffects []
346 
347  SeeAlso []
348 
349 ***********************************************************************/
350 Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Man_t * pWnd )
351 {
352  Aig_Man_t * pNew;
353  Vec_Ptr_t * vBigNode2SmallPo, * vSmallPi2BigNode;
354  Vec_Ptr_t * vNodesPi, * vNodesPo;
355  Aig_Obj_t * pObj;
356  int i;
357 
358  // set mapping of small PIs into big nodes
359  vSmallPi2BigNode = Vec_PtrStart( Aig_ManObjNumMax(pWnd) );
360  vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
361  Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i )
362  Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManCi(pWnd, i)->Id, pObj );
363  assert( i == Saig_ManPiNum(pWnd) );
364  Vec_PtrFree( vNodesPi );
365 
366  // set mapping of big nodes into small POs
367  vBigNode2SmallPo = Vec_PtrStart( Aig_ManObjNumMax(p) );
368  vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
369  Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i )
370  Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManCo(pWnd, i) );
371  assert( i == Saig_ManPoNum(pWnd) );
372  Vec_PtrFree( vNodesPo );
373 
374  // create the new manager
375  Aig_ManCleanData( p );
376  Aig_ManCleanData( pWnd );
377  pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
378  pNew->pName = Abc_UtilStrsav( p->pName );
379  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
380  // map constant nodes
381  pObj = Aig_ManConst1( p );
382  pObj->pData = Aig_ManConst1( pNew );
383  pObj = Aig_ManConst1( pWnd );
384  pObj->pData = Aig_ManConst1( pNew );
385 
386  // create real PIs
387  Aig_ManForEachCi( p, pObj, i )
388  if ( Saig_ObjIsPi(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
389  pObj->pData = Aig_ObjCreateCi(pNew);
390  // create additional latch outputs
391  Saig_ManForEachLo( pWnd, pObj, i )
392  pObj->pData = Aig_ObjCreateCi(pNew);
393 
394  // create internal nodes starting from the big
395  Aig_ManForEachCo( p, pObj, i )
396  if ( Saig_ObjIsPo(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
397  {
398  Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
399  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
400  }
401  // create internal nodes starting from the small
402  Saig_ManForEachLi( pWnd, pObj, i )
403  {
404  Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
405  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
406  }
407  Vec_PtrFree( vBigNode2SmallPo );
408  Vec_PtrFree( vSmallPi2BigNode );
409  // set the new number of registers
410  assert( Aig_ManCiNum(pNew) - Aig_ManCiNum(p) == Aig_ManCoNum(pNew) - Aig_ManCoNum(p) );
411  Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManCiNum(pNew) - Aig_ManCiNum(p)) );
412  Aig_ManCleanup( pNew );
413  return pNew;
414 }
415 
416 /**Function*************************************************************
417 
418  Synopsis [Find a good object.]
419 
420  Description []
421 
422  SideEffects []
423 
424  SeeAlso []
425 
426 ***********************************************************************/
427 Aig_Obj_t * Saig_ManFindPivot( Aig_Man_t * p )
428 {
429  Aig_Obj_t * pObj;
430  int i, Counter;
431  if ( Aig_ManRegNum(p) > 0 )
432  {
433  if ( Aig_ManRegNum(p) == 1 )
434  return Saig_ManLo( p, 0 );
435  Saig_ManForEachLo( p, pObj, i )
436  {
437  if ( i == Aig_ManRegNum(p)/2 )
438  return pObj;
439  }
440  }
441  else
442  {
443  Counter = 0;
444  assert( Aig_ManNodeNum(p) > 1 );
445  Aig_ManForEachNode( p, pObj, i )
446  {
447  if ( Counter++ == Aig_ManNodeNum(p)/2 )
448  return pObj;
449  }
450  }
451  return NULL;
452 }
453 
454 /**Function*************************************************************
455 
456  Synopsis [Computes sequential window of the node.]
457 
458  Description []
459 
460  SideEffects []
461 
462  SeeAlso []
463 
464 ***********************************************************************/
465 Aig_Man_t * Saig_ManWindowExtract( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
466 {
467  Aig_Man_t * pWnd;
468  Vec_Ptr_t * vNodes;
469  Aig_ManFanoutStart( p );
470  vNodes = Saig_ManWindowOutline( p, pObj, nDist );
471  pWnd = Saig_ManWindowExtractNodes( p, vNodes );
472  Vec_PtrFree( vNodes );
473  Aig_ManFanoutStop( p );
474  return pWnd;
475 }
476 
477 /**Function*************************************************************
478 
479  Synopsis [Computes sequential window of the node.]
480 
481  Description []
482 
483  SideEffects []
484 
485  SeeAlso []
486 
487 ***********************************************************************/
488 Aig_Man_t * Saig_ManWindowInsert( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Aig_Man_t * pWnd )
489 {
490  Aig_Man_t * pNew, * pWndTest;
491  Vec_Ptr_t * vNodes;
492  Aig_ManFanoutStart( p );
493 
494  vNodes = Saig_ManWindowOutline( p, pObj, nDist );
495  pWndTest = Saig_ManWindowExtractNodes( p, vNodes );
496  if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) ||
497  Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) )
498  {
499  printf( "The window cannot be reinserted because PI/PO counts do not match.\n" );
500  Aig_ManStop( pWndTest );
501  Vec_PtrFree( vNodes );
502  Aig_ManFanoutStop( p );
503  return NULL;
504  }
505  Aig_ManStop( pWndTest );
506  Vec_PtrFree( vNodes );
507 
508  // insert the nodes
509  Aig_ManCleanData( p );
510  vNodes = Saig_ManWindowOutline( p, pObj, nDist );
511  pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd );
512  Vec_PtrFree( vNodes );
513  Aig_ManFanoutStop( p );
514  return pNew;
515 }
516 
517 /**Function*************************************************************
518 
519  Synopsis [Tests the above computation.]
520 
521  Description []
522 
523  SideEffects []
524 
525  SeeAlso []
526 
527 ***********************************************************************/
528 Aig_Man_t * Saig_ManWindowTest( Aig_Man_t * p )
529 {
530  int nDist = 3;
531  Aig_Man_t * pWnd, * pNew;
532  Aig_Obj_t * pPivot;
533  pPivot = Saig_ManFindPivot( p );
534  assert( pPivot != NULL );
535  pWnd = Saig_ManWindowExtract( p, pPivot, nDist );
536  pNew = Saig_ManWindowInsert( p, pPivot, nDist, pWnd );
537  Aig_ManStop( pWnd );
538  return pNew;
539 }
540 
541 /**Function*************************************************************
542 
543  Synopsis [Collects the nodes that are not linked to each other.]
544 
545  Description []
546 
547  SideEffects []
548 
549  SeeAlso []
550 
551 ***********************************************************************/
552 Vec_Ptr_t * Saig_ManCollectedDiffNodes( Aig_Man_t * p0, Aig_Man_t * p1 )
553 {
554  Vec_Ptr_t * vNodes;
555  Aig_Obj_t * pObj0, * pObj1;
556  int i;
557  // collect nodes that are not linked
558  Aig_ManIncrementTravId( p0 );
559  vNodes = Vec_PtrAlloc( 1000 );
560  Aig_ManForEachObj( p0, pObj0, i )
561  {
562  pObj1 = Aig_ObjRepr( p0, pObj0 );
563  if ( pObj1 != NULL )
564  {
565  assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
566  continue;
567  }
568  // mark and collect unmatched objects
569  Aig_ObjSetTravIdCurrent( p0, pObj0 );
570  if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsCi(pObj0) )
571  Vec_PtrPush( vNodes, pObj0 );
572  }
573  // make sure LI/LO are labeled/unlabeled mutually
574  Saig_ManForEachLiLo( p0, pObj0, pObj1, i )
575  assert( Aig_ObjIsTravIdCurrent(p0, pObj0) ==
576  Aig_ObjIsTravIdCurrent(p0, pObj1) );
577  return vNodes;
578 }
579 
580 /**Function*************************************************************
581 
582  Synopsis [Creates PIs of the miter.]
583 
584  Description []
585 
586  SideEffects []
587 
588  SeeAlso []
589 
590 ***********************************************************************/
591 void Saig_ManWindowCreatePis( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Ptr_t * vNodes0 )
592 {
593  Aig_Obj_t * pObj, * pMatch, * pFanin;
594  int i, Counter = 0;
595  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj, i )
596  {
597  if ( Saig_ObjIsLo(p0, pObj) )
598  {
599  pMatch = Saig_ObjLoToLi( p0, pObj );
600  pFanin = Aig_ObjFanin0(pMatch);
601  if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
602  {
603  pFanin->pData = Aig_ObjCreateCi(pNew);
604  pMatch = Aig_ObjRepr( p0, pFanin );
605  assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
606  assert( pMatch != NULL );
607  pMatch->pData = pFanin->pData;
608  Counter++;
609  }
610  }
611  else
612  {
613  assert( Aig_ObjIsNode(pObj) );
614  pFanin = Aig_ObjFanin0(pObj);
615  if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
616  {
617  pFanin->pData = Aig_ObjCreateCi(pNew);
618  pMatch = Aig_ObjRepr( p0, pFanin );
619  assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
620  assert( pMatch != NULL );
621  pMatch->pData = pFanin->pData;
622  Counter++;
623  }
624  pFanin = Aig_ObjFanin1(pObj);
625  if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
626  {
627  pFanin->pData = Aig_ObjCreateCi(pNew);
628  pMatch = Aig_ObjRepr( p0, pFanin );
629  assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
630  assert( pMatch != NULL );
631  pMatch->pData = pFanin->pData;
632  Counter++;
633  }
634  }
635  }
636 // printf( "Added %d primary inputs.\n", Counter );
637 }
638 
639 /**Function*************************************************************
640 
641  Synopsis [Creates POs of the miter.]
642 
643  Description []
644 
645  SideEffects []
646 
647  SeeAlso []
648 
649 ***********************************************************************/
650 void Saig_ManWindowCreatePos( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1 )
651 {
652  Aig_Obj_t * pObj0, * pObj1, * pMiter;
653  Aig_Obj_t * pFanin0, * pFanin1;
654  int i;
655  Aig_ManForEachObj( p0, pObj0, i )
656  {
657  if ( Aig_ObjIsTravIdCurrent(p0, pObj0) )
658  continue;
659  if ( Aig_ObjIsConst1(pObj0) )
660  continue;
661  if ( Aig_ObjIsCi(pObj0) )
662  continue;
663  pObj1 = Aig_ObjRepr( p0, pObj0 );
664  assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
665  if ( Aig_ObjIsCo(pObj0) )
666  {
667  pFanin0 = Aig_ObjFanin0(pObj0);
668  pFanin1 = Aig_ObjFanin0(pObj1);
669  assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
670  Aig_ObjIsTravIdCurrent(p1, pFanin1) );
671  if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
672  {
673  pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
674  Aig_ObjCreateCo( pNew, pMiter );
675  }
676  }
677  else
678  {
679  assert( Aig_ObjIsNode(pObj0) );
680 
681  pFanin0 = Aig_ObjFanin0(pObj0);
682  pFanin1 = Aig_ObjFanin0(pObj1);
683  assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
684  Aig_ObjIsTravIdCurrent(p1, pFanin1) );
685  if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
686  {
687  pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
688  Aig_ObjCreateCo( pNew, pMiter );
689  }
690 
691  pFanin0 = Aig_ObjFanin1(pObj0);
692  pFanin1 = Aig_ObjFanin1(pObj1);
693  assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
694  Aig_ObjIsTravIdCurrent(p1, pFanin1) );
695  if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
696  {
697  pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
698  Aig_ObjCreateCo( pNew, pMiter );
699  }
700  }
701  }
702 }
703 
704 
705 /**Function*************************************************************
706 
707  Synopsis [Extracts the window AIG from the AIG manager.]
708 
709  Description []
710 
711  SideEffects []
712 
713  SeeAlso []
714 
715 ***********************************************************************/
716 Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 )
717 {
718  Aig_Man_t * pNew;
719  Aig_Obj_t * pObj0, * pObj1, * pMatch0, * pMatch1;
720  Vec_Ptr_t * vNodes0, * vNodes1;
721  int i, nRegCount;
722  // add matching of POs and LIs
723  Saig_ManForEachPo( p0, pObj0, i )
724  {
725  pObj1 = Aig_ManCo( p1, i );
726  Aig_ObjSetRepr( p0, pObj0, pObj1 );
727  Aig_ObjSetRepr( p1, pObj1, pObj0 );
728  }
729  Saig_ManForEachLi( p0, pObj0, i )
730  {
731  pMatch0 = Saig_ObjLiToLo( p0, pObj0 );
732  pMatch1 = Aig_ObjRepr( p0, pMatch0 );
733  if ( pMatch1 == NULL )
734  continue;
735  assert( pMatch0 == Aig_ObjRepr( p1, pMatch1 ) );
736  pObj1 = Saig_ObjLoToLi( p1, pMatch1 );
737  Aig_ObjSetRepr( p0, pObj0, pObj1 );
738  Aig_ObjSetRepr( p1, pObj1, pObj0 );
739  }
740  // clean the markings
741  Aig_ManCleanData( p0 );
742  Aig_ManCleanData( p1 );
743  // collect nodes that are not linked
744  vNodes0 = Saig_ManCollectedDiffNodes( p0, p1 );
745  vNodes1 = Saig_ManCollectedDiffNodes( p1, p0 );
746  // create the new manager
747  pNew = Aig_ManStart( Vec_PtrSize(vNodes0) + Vec_PtrSize(vNodes1) );
748  pNew->pName = Abc_UtilStrsav( "wnd" );
749  pNew->pSpec = NULL;
750  // map constant nodes
751  pObj0 = Aig_ManConst1( p0 );
752  pObj0->pData = Aig_ManConst1( pNew );
753  pObj1 = Aig_ManConst1( p1 );
754  pObj1->pData = Aig_ManConst1( pNew );
755  // create real PIs
756  Saig_ManWindowCreatePis( pNew, p0, p1, vNodes0 );
757  Saig_ManWindowCreatePis( pNew, p1, p0, vNodes1 );
758  // create register outputs
759  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
760  {
761  if ( Saig_ObjIsLo(p0, pObj0) )
762  pObj0->pData = Aig_ObjCreateCi(pNew);
763  }
764  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
765  {
766  if ( Saig_ObjIsLo(p1, pObj1) )
767  pObj1->pData = Aig_ObjCreateCi(pNew);
768  }
769  // create internal nodes
770  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
771  {
772  if ( Aig_ObjIsNode(pObj0) )
773  pObj0->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
774  }
775  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
776  {
777  if ( Aig_ObjIsNode(pObj1) )
778  pObj1->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj1), Aig_ObjChild1Copy(pObj1) );
779  }
780  // create POs
781  Saig_ManWindowCreatePos( pNew, p0, p1 );
782 // Saig_ManWindowCreatePos( pNew, p1, p0 );
783  // create register inputs
784  nRegCount = 0;
785  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
786  {
787  if ( Saig_ObjIsLo(p0, pObj0) )
788  {
789  pMatch0 = Saig_ObjLoToLi( p0, pObj0 );
790  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch0) );
791  nRegCount++;
792  }
793  }
794  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
795  {
796  if ( Saig_ObjIsLo(p1, pObj1) )
797  {
798  pMatch1 = Saig_ObjLoToLi( p1, pObj1 );
799  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch1) );
800  nRegCount++;
801  }
802  }
803  Aig_ManSetRegNum( pNew, nRegCount );
804  Aig_ManCleanup( pNew );
805  Vec_PtrFree( vNodes0 );
806  Vec_PtrFree( vNodes1 );
807  return pNew;
808 }
809 
810 ////////////////////////////////////////////////////////////////////////
811 /// END OF FILE ///
812 ////////////////////////////////////////////////////////////////////////
813 
814 
815 ABC_NAMESPACE_IMPL_END
816 
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Aig_ObjCompareIdIncrease
int Aig_ObjCompareIdIncrease(Aig_Obj_t **pp1, Aig_Obj_t **pp2)
Definition: aigUtil.c:496
Saig_ManWindowCollectPis
Vec_Ptr_t * Saig_ManWindowCollectPis(Aig_Man_t *p, Vec_Ptr_t *vNodes)
Definition: saigWnd.c:150
Aig_ObjForEachFanout
#define Aig_ObjForEachFanout(p, pObj, pFanout, iFan, i)
Definition: aig.h:427
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Saig_ManFindPivot
Aig_Obj_t * Saig_ManFindPivot(Aig_Man_t *p)
Definition: saigWnd.c:427
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_ObjRepr
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
Saig_ManWindowCollectPos
Vec_Ptr_t * Saig_ManWindowCollectPos(Aig_Man_t *p, Vec_Ptr_t *vNodes, Vec_Ptr_t **pvPointers)
Definition: saigWnd.c:195
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Saig_ManLo
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Saig_ManWindowOutline
Vec_Ptr_t * Saig_ManWindowOutline(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
Definition: saigWnd.c:100
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Saig_ManWindowTest
Aig_Man_t * Saig_ManWindowTest(Aig_Man_t *p)
Definition: saigWnd.c:528
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Vec_PtrSort
static void Vec_PtrSort(Vec_Ptr_t *p, int(*Vec_PtrSortCompare)()) ___unused
Definition: vecPtr.h:851
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Saig_ManWindowExtractMiter
Aig_Man_t * Saig_ManWindowExtractMiter(Aig_Man_t *p0, Aig_Man_t *p1)
Definition: saigWnd.c:716
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_ManFanoutStart
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: aigFanout.c:56
Aig_ManFanoutStop
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition: aigFanout.c:89
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Saig_ManCollectedDiffNodes
Vec_Ptr_t * Saig_ManCollectedDiffNodes(Aig_Man_t *p0, Aig_Man_t *p1)
Definition: saigWnd.c:552
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Aig_ObjSetRepr
static void Aig_ObjSetRepr(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
Definition: aig.h:331
Saig_ManWindowInsert
Aig_Man_t * Saig_ManWindowInsert(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Aig_Man_t *pWnd)
Definition: saigWnd.c:488
Saig_ManWindowInsertNodes
Aig_Man_t * Saig_ManWindowInsertNodes(Aig_Man_t *p, Vec_Ptr_t *vNodes, Aig_Man_t *pWnd)
Definition: saigWnd.c:350
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Saig_ManWindowCreatePis
void Saig_ManWindowCreatePis(Aig_Man_t *pNew, Aig_Man_t *p0, Aig_Man_t *p1, Vec_Ptr_t *vNodes0)
Definition: saigWnd.c:591
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Saig_ObjIsPo
static int Saig_ObjIsPo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:83
Saig_ObjLiToLo
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Saig_ObjHasUnlabeledFanout
Aig_Obj_t * Saig_ObjHasUnlabeledFanout(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saigWnd.c:129
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Saig_ManWindowInsertBig_rec
void Saig_ManWindowInsertBig_rec(Aig_Man_t *pNew, Aig_Obj_t *pObjBig, Vec_Ptr_t *vBigNode2SmallPo, Vec_Ptr_t *vSmallPi2BigNode)
Definition: saigWnd.c:292
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Saig_ManWindowOutline_rec
ABC_NAMESPACE_IMPL_START void Saig_ManWindowOutline_rec(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Vec_Ptr_t *vNodes, int *pDists)
DECLARATIONS ///.
Definition: saigWnd.c:46
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Saig_ManWindowExtractNodes
Aig_Man_t * Saig_ManWindowExtractNodes(Aig_Man_t *p, Vec_Ptr_t *vNodes)
Definition: saigWnd.c:226
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Saig_ManWindowCreatePos
void Saig_ManWindowCreatePos(Aig_Man_t *pNew, Aig_Man_t *p0, Aig_Man_t *p1)
Definition: saigWnd.c:650
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Saig_ManWindowExtract
Aig_Man_t * Saig_ManWindowExtract(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
Definition: saigWnd.c:465
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Saig_ManWindowInsertSmall_rec
static void Saig_ManWindowInsertSmall_rec(Aig_Man_t *pNew, Aig_Obj_t *pObjSmall, Vec_Ptr_t *vBigNode2SmallPo, Vec_Ptr_t *vSmallPi2BigNode)
Definition: saigWnd.c:321
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223