abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcRr.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcRr.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Redundancy removal.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcRr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "proof/fraig/fraig.h"
23 #include "opt/sim/sim.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Abc_RRMan_t_ Abc_RRMan_t;
33 struct Abc_RRMan_t_
34 {
35  // the parameters
36  Abc_Ntk_t * pNtk; // the network
37  int nFaninLevels; // the number of fanin levels
38  int nFanoutLevels; // the number of fanout levels
39  // the node/fanin/fanout
40  Abc_Obj_t * pNode; // the node
41  Abc_Obj_t * pFanin; // the fanin
42  Abc_Obj_t * pFanout; // the fanout
43  // the intermediate cones
44  Vec_Ptr_t * vFaninLeaves; // the leaves of the fanin cone
45  Vec_Ptr_t * vFanoutRoots; // the roots of the fanout cone
46  // the window
47  Vec_Ptr_t * vLeaves; // the leaves of the window
48  Vec_Ptr_t * vCone; // the internal nodes of the window
49  Vec_Ptr_t * vRoots; // the roots of the window
50  Abc_Ntk_t * pWnd; // the window derived for the edge
51  // the miter
52  Abc_Ntk_t * pMiter; // the miter derived from the window
53  Prove_Params_t * pParams; // the miter proving parameters
54  // statistical variables
55  int nNodesOld; // the old number of nodes
56  int nLevelsOld; // the old number of levels
57  int nEdgesTried; // the number of nodes tried
58  int nEdgesRemoved; // the number of nodes proved
59  abctime timeWindow; // the time to construct the window
60  abctime timeMiter; // the time to construct the miter
61  abctime timeProve; // the time to prove the miter
62  abctime timeUpdate; // the network update time
63  abctime timeTotal; // the total runtime
64 };
65 
66 static Abc_RRMan_t * Abc_RRManStart();
67 static void Abc_RRManStop( Abc_RRMan_t * p );
68 static void Abc_RRManPrintStats( Abc_RRMan_t * p );
69 static void Abc_RRManClean( Abc_RRMan_t * p );
70 static int Abc_NtkRRProve( Abc_RRMan_t * p );
71 static int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout );
72 static int Abc_NtkRRWindow( Abc_RRMan_t * p );
73 
74 static int Abc_NtkRRTfi_int( Vec_Ptr_t * vLeaves, int LevelLimit );
75 static int Abc_NtkRRTfo_int( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout );
76 static int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit );
77 static void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, int LevelLimit );
78 static Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots );
79 
80 static void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk );
81 static void Abc_NtkRRSimulateStop( Abc_Ntk_t * pNtk );
82 
83 ////////////////////////////////////////////////////////////////////////
84 /// FUNCTION DEFINITIONS ///
85 ////////////////////////////////////////////////////////////////////////
86 
87 /**Function*************************************************************
88 
89  Synopsis [Removes stuck-at redundancies.]
90 
91  Description []
92 
93  SideEffects []
94 
95  SeeAlso []
96 
97 ***********************************************************************/
98 int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose )
99 {
100  ProgressBar * pProgress;
101  Abc_RRMan_t * p;
102  Abc_Obj_t * pNode, * pFanin, * pFanout;
103  int i, k, m, nNodes, RetValue;
104  abctime clk, clkTotal = Abc_Clock();
105  // start the manager
106  p = Abc_RRManStart();
107  p->pNtk = pNtk;
108  p->nFaninLevels = nFaninLevels;
109  p->nFanoutLevels = nFanoutLevels;
110  p->nNodesOld = Abc_NtkNodeNum(pNtk);
111  p->nLevelsOld = Abc_AigLevel(pNtk);
112  // remember latch values
113 // Abc_NtkForEachLatch( pNtk, pNode, i )
114 // pNode->pNext = pNode->pData;
115  // go through the nodes
116  Abc_NtkCleanCopy(pNtk);
117  nNodes = Abc_NtkObjNumMax(pNtk);
118  Abc_NtkRRSimulateStart(pNtk);
119  pProgress = Extra_ProgressBarStart( stdout, nNodes );
120  Abc_NtkForEachNode( pNtk, pNode, i )
121  {
122  Extra_ProgressBarUpdate( pProgress, i, NULL );
123  // stop if all nodes have been tried once
124  if ( i >= nNodes )
125  break;
126  // skip the constant node
127 // if ( Abc_NodeIsConst(pNode) )
128 // continue;
129  // skip persistant nodes
130  if ( Abc_NodeIsPersistant(pNode) )
131  continue;
132  // skip the nodes with many fanouts
133  if ( Abc_ObjFanoutNum(pNode) > 1000 )
134  continue;
135  // construct the window
136  if ( !fUseFanouts )
137  {
138  Abc_ObjForEachFanin( pNode, pFanin, k )
139  {
140  // skip the nodes with only one fanout (tree nodes)
141  if ( Abc_ObjFanoutNum(pFanin) == 1 )
142  continue;
143 /*
144  if ( pFanin->Id == 228 && pNode->Id == 2649 )
145  {
146  int k = 0;
147  }
148 */
149  p->nEdgesTried++;
150  Abc_RRManClean( p );
151  p->pNode = pNode;
152  p->pFanin = pFanin;
153  p->pFanout = NULL;
154 
155  clk = Abc_Clock();
156  RetValue = Abc_NtkRRWindow( p );
157  p->timeWindow += Abc_Clock() - clk;
158  if ( !RetValue )
159  continue;
160 /*
161  if ( pFanin->Id == 228 && pNode->Id == 2649 )
162  {
163  Abc_NtkShowAig( p->pWnd, 0 );
164  }
165 */
166  clk = Abc_Clock();
167  RetValue = Abc_NtkRRProve( p );
168  p->timeMiter += Abc_Clock() - clk;
169  if ( !RetValue )
170  continue;
171 //printf( "%d -> %d (%d)\n", pFanin->Id, pNode->Id, k );
172 
173  clk = Abc_Clock();
174  Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
175  p->timeUpdate += Abc_Clock() - clk;
176 
177  p->nEdgesRemoved++;
178  break;
179  }
180  continue;
181  }
182  // use the fanouts
183  Abc_ObjForEachFanin( pNode, pFanin, k )
184  Abc_ObjForEachFanout( pNode, pFanout, m )
185  {
186  // skip the nodes with only one fanout (tree nodes)
187 // if ( Abc_ObjFanoutNum(pFanin) == 1 && Abc_ObjFanoutNum(pNode) == 1 )
188 // continue;
189 
190  p->nEdgesTried++;
191  Abc_RRManClean( p );
192  p->pNode = pNode;
193  p->pFanin = pFanin;
194  p->pFanout = pFanout;
195 
196  clk = Abc_Clock();
197  RetValue = Abc_NtkRRWindow( p );
198  p->timeWindow += Abc_Clock() - clk;
199  if ( !RetValue )
200  continue;
201 
202  clk = Abc_Clock();
203  RetValue = Abc_NtkRRProve( p );
204  p->timeMiter += Abc_Clock() - clk;
205  if ( !RetValue )
206  continue;
207 
208  clk = Abc_Clock();
209  Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
210  p->timeUpdate += Abc_Clock() - clk;
211 
212  p->nEdgesRemoved++;
213  break;
214  }
215  }
216  Abc_NtkRRSimulateStop(pNtk);
217  Extra_ProgressBarStop( pProgress );
218  p->timeTotal = Abc_Clock() - clkTotal;
219  if ( fVerbose )
220  Abc_RRManPrintStats( p );
221  Abc_RRManStop( p );
222  // restore latch values
223 // Abc_NtkForEachLatch( pNtk, pNode, i )
224 // pNode->pData = pNode->pNext, pNode->pNext = NULL;
225  // put the nodes into the DFS order and reassign their IDs
226  Abc_NtkReassignIds( pNtk );
227  Abc_NtkLevel( pNtk );
228  // check
229  if ( !Abc_NtkCheck( pNtk ) )
230  {
231  printf( "Abc_NtkRR: The network check has failed.\n" );
232  return 0;
233  }
234  return 1;
235 }
236 
237 /**Function*************************************************************
238 
239  Synopsis [Start the manager.]
240 
241  Description []
242 
243  SideEffects []
244 
245  SeeAlso []
246 
247 ***********************************************************************/
248 Abc_RRMan_t * Abc_RRManStart()
249 {
250  Abc_RRMan_t * p;
251  p = ABC_ALLOC( Abc_RRMan_t, 1 );
252  memset( p, 0, sizeof(Abc_RRMan_t) );
253  p->vFaninLeaves = Vec_PtrAlloc( 100 ); // the leaves of the fanin cone
254  p->vFanoutRoots = Vec_PtrAlloc( 100 ); // the roots of the fanout cone
255  p->vLeaves = Vec_PtrAlloc( 100 ); // the leaves of the window
256  p->vCone = Vec_PtrAlloc( 100 ); // the internal nodes of the window
257  p->vRoots = Vec_PtrAlloc( 100 ); // the roots of the window
258  p->pParams = ABC_ALLOC( Prove_Params_t, 1 );
259  memset( p->pParams, 0, sizeof(Prove_Params_t) );
260  Prove_ParamsSetDefault( p->pParams );
261  return p;
262 }
263 
264 /**Function*************************************************************
265 
266  Synopsis [Stop the manager.]
267 
268  Description []
269 
270  SideEffects []
271 
272  SeeAlso []
273 
274 ***********************************************************************/
275 void Abc_RRManStop( Abc_RRMan_t * p )
276 {
277  Abc_RRManClean( p );
278  Vec_PtrFree( p->vFaninLeaves );
279  Vec_PtrFree( p->vFanoutRoots );
280  Vec_PtrFree( p->vLeaves );
281  Vec_PtrFree( p->vCone );
282  Vec_PtrFree( p->vRoots );
283  ABC_FREE( p->pParams );
284  ABC_FREE( p );
285 }
286 
287 /**Function*************************************************************
288 
289  Synopsis [Stop the manager.]
290 
291  Description []
292 
293  SideEffects []
294 
295  SeeAlso []
296 
297 ***********************************************************************/
298 void Abc_RRManPrintStats( Abc_RRMan_t * p )
299 {
300  double Ratio = 100.0*(p->nNodesOld - Abc_NtkNodeNum(p->pNtk))/p->nNodesOld;
301  printf( "Redundancy removal statistics:\n" );
302  printf( "Edges tried = %6d.\n", p->nEdgesTried );
303  printf( "Edges removed = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried );
304  printf( "Node gain = %6d. (%5.2f %%)\n", p->nNodesOld - Abc_NtkNodeNum(p->pNtk), Ratio );
305  printf( "Level gain = %6d.\n", p->nLevelsOld - Abc_AigLevel(p->pNtk) );
306  ABC_PRT( "Windowing ", p->timeWindow );
307  ABC_PRT( "Miter ", p->timeMiter );
308  ABC_PRT( " Construct ", p->timeMiter - p->timeProve );
309  ABC_PRT( " Prove ", p->timeProve );
310  ABC_PRT( "Update ", p->timeUpdate );
311  ABC_PRT( "TOTAL ", p->timeTotal );
312 }
313 
314 /**Function*************************************************************
315 
316  Synopsis [Clean the manager.]
317 
318  Description []
319 
320  SideEffects []
321 
322  SeeAlso []
323 
324 ***********************************************************************/
325 void Abc_RRManClean( Abc_RRMan_t * p )
326 {
327  p->pNode = NULL;
328  p->pFanin = NULL;
329  p->pFanout = NULL;
330  Vec_PtrClear( p->vFaninLeaves );
331  Vec_PtrClear( p->vFanoutRoots );
332  Vec_PtrClear( p->vLeaves );
333  Vec_PtrClear( p->vCone );
334  Vec_PtrClear( p->vRoots );
335  if ( p->pWnd ) Abc_NtkDelete( p->pWnd );
336  if ( p->pMiter ) Abc_NtkDelete( p->pMiter );
337  p->pWnd = NULL;
338  p->pMiter = NULL;
339 }
340 
341 /**Function*************************************************************
342 
343  Synopsis [Returns 1 if the miter is constant 0.]
344 
345  Description []
346 
347  SideEffects []
348 
349  SeeAlso []
350 
351 ***********************************************************************/
352 int Abc_NtkRRProve( Abc_RRMan_t * p )
353 {
354  Abc_Ntk_t * pWndCopy;
355  int RetValue;
356  abctime clk;
357 // Abc_NtkShowAig( p->pWnd, 0 );
358  pWndCopy = Abc_NtkDup( p->pWnd );
359  Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
360  if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
361  Abc_NtkReassignIds(pWndCopy);
362  p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0, 0 );
363  Abc_NtkDelete( pWndCopy );
364 clk = Abc_Clock();
365  RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams );
366 p->timeProve += Abc_Clock() - clk;
367  if ( RetValue == 1 )
368  return 1;
369  return 0;
370 }
371 
372 /**Function*************************************************************
373 
374  Synopsis [Updates the network after redundancy removal.]
375 
376  Description [This procedure assumes that non-control value of the fanin
377  was proved redundant. It is okay to concentrate on non-control values
378  because the control values can be seen as redundancy of the fanout edge.]
379 
380  SideEffects []
381 
382  SeeAlso []
383 
384 ***********************************************************************/
385 int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout )
386 {
387  Abc_Obj_t * pNodeNew, * pFanoutNew;
388  assert( pFanout == NULL );
389  assert( !Abc_ObjIsComplement(pNode) );
390  assert( !Abc_ObjIsComplement(pFanin) );
391  assert( !Abc_ObjIsComplement(pFanout) );
392  // find the node after redundancy removal
393  if ( pFanin == Abc_ObjFanin0(pNode) )
394  pNodeNew = Abc_ObjChild1(pNode);
395  else if ( pFanin == Abc_ObjFanin1(pNode) )
396  pNodeNew = Abc_ObjChild0(pNode);
397  else assert( 0 );
398  // replace
399  if ( pFanout == NULL )
400  {
401  Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
402  return 1;
403  }
404  // find the fanout after redundancy removal
405  if ( pNode == Abc_ObjFanin0(pFanout) )
406  pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );
407  else if ( pNode == Abc_ObjFanin1(pFanout) )
408  pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) );
409  else assert( 0 );
410  // replace
411  Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pFanout, pFanoutNew, 1 );
412  return 1;
413 }
414 
415 /**Function*************************************************************
416 
417  Synopsis [Constructs window for checking RR.]
418 
419  Description [If the window (p->pWnd) with the given scope (p->nFaninLevels,
420  p->nFanoutLevels) cannot be constructed, returns 0. Otherwise, returns 1.
421  The levels are measured from the fanin node (pFanin) and the fanout node
422  (pEdgeFanout), respectively.]
423 
424  SideEffects []
425 
426  SeeAlso []
427 
428 ***********************************************************************/
429 int Abc_NtkRRWindow( Abc_RRMan_t * p )
430 {
431  Abc_Obj_t * pObj, * pEdgeFanin, * pEdgeFanout;
432  int i, LevelMin, LevelMax, RetValue;
433 
434  // get the edge
435  pEdgeFanout = p->pFanout? p->pFanout : p->pNode;
436  pEdgeFanin = p->pFanout? p->pNode : p->pFanin;
437  // get the minimum and maximum levels of the window
438  LevelMin = Abc_MaxInt( 0, ((int)p->pFanin->Level) - p->nFaninLevels );
439  LevelMax = (int)pEdgeFanout->Level + p->nFanoutLevels;
440 
441  // start the TFI leaves with the fanin
442  Abc_NtkIncrementTravId( p->pNtk );
443  Abc_NodeSetTravIdCurrent( p->pFanin );
444  Vec_PtrPush( p->vFaninLeaves, p->pFanin );
445  // mark the TFI cone and collect the leaves down to the given level
446  while ( Abc_NtkRRTfi_int(p->vFaninLeaves, LevelMin) );
447 
448  // mark the leaves with the new TravId
449  Abc_NtkIncrementTravId( p->pNtk );
450  Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninLeaves, pObj, i )
451  Abc_NodeSetTravIdCurrent( pObj );
452  // traverse the TFO cone of the leaves (while skipping the edge)
453  // (a) mark the nodes in the cone using the current TravId
454  // (b) collect the nodes that have external fanouts into p->vFanoutRoots
455  while ( Abc_NtkRRTfo_int(p->vFaninLeaves, p->vFanoutRoots, LevelMax, pEdgeFanin, pEdgeFanout) );
456 
457  // mark the fanout roots
458  Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanoutRoots, pObj, i )
459  pObj->fMarkA = 1;
460  // collect roots reachable from the fanout (p->vRoots)
461  RetValue = Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, LevelMax + 1 );
462  // unmark the fanout roots
463  Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanoutRoots, pObj, i )
464  pObj->fMarkA = 0;
465 
466  // return if the window is infeasible
467  if ( RetValue == 0 )
468  return 0;
469 
470  // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves)
471  // using the previous marks coming from the TFO cone
472  Abc_NtkIncrementTravId( p->pNtk );
473  Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
474  Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone, LevelMin );
475 
476  // create a new network
477  p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots );
478  return 1;
479 }
480 
481 /**Function*************************************************************
482 
483  Synopsis [Marks the nodes in the TFI and collects their leaves.]
484 
485  Description []
486 
487  SideEffects []
488 
489  SeeAlso []
490 
491 ***********************************************************************/
492 int Abc_NtkRRTfi_int( Vec_Ptr_t * vLeaves, int LevelLimit )
493 {
494  Abc_Obj_t * pObj, * pNext;
495  int i, k, LevelMax, nSize;
496  assert( LevelLimit >= 0 );
497  // find the maximum level of leaves
498  LevelMax = 0;
499  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
500  if ( LevelMax < (int)pObj->Level )
501  LevelMax = pObj->Level;
502  // if the nodes are all PIs, LevelMax == 0
503  if ( LevelMax <= LevelLimit )
504  return 0;
505  // expand the nodes with the minimum level
506  nSize = Vec_PtrSize(vLeaves);
507  Vec_PtrForEachEntryStop( Abc_Obj_t *, vLeaves, pObj, i, nSize )
508  {
509  if ( LevelMax != (int)pObj->Level )
510  continue;
511  Abc_ObjForEachFanin( pObj, pNext, k )
512  {
513  if ( Abc_NodeIsTravIdCurrent(pNext) )
514  continue;
515  Abc_NodeSetTravIdCurrent( pNext );
516  Vec_PtrPush( vLeaves, pNext );
517  }
518  }
519  // remove old nodes (cannot remove a PI)
520  k = 0;
521  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
522  {
523  if ( LevelMax == (int)pObj->Level )
524  continue;
525  Vec_PtrWriteEntry( vLeaves, k++, pObj );
526  }
527  Vec_PtrShrink( vLeaves, k );
528  if ( Vec_PtrSize(vLeaves) > 2000 )
529  return 0;
530  return 1;
531 }
532 
533 /**Function*************************************************************
534 
535  Synopsis [Marks the nodes in the TFO and collects their roots.]
536 
537  Description []
538 
539  SideEffects []
540 
541  SeeAlso []
542 
543 ***********************************************************************/
544 int Abc_NtkRRTfo_int( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout )
545 {
546  Abc_Obj_t * pObj, * pNext;
547  int i, k, LevelMin, nSize, fObjIsRoot;
548  // find the minimum level of leaves
549  LevelMin = ABC_INFINITY;
550  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
551  if ( LevelMin > (int)pObj->Level )
552  LevelMin = pObj->Level;
553  // if the minimum level exceed the limit, we are done
554  if ( LevelMin > LevelLimit )
555  return 0;
556  // expand the nodes with the minimum level
557  nSize = Vec_PtrSize(vLeaves);
558  Vec_PtrForEachEntryStop( Abc_Obj_t *, vLeaves, pObj, i, nSize )
559  {
560  if ( LevelMin != (int)pObj->Level )
561  continue;
562  fObjIsRoot = 0;
563  Abc_ObjForEachFanout( pObj, pNext, k )
564  {
565  // check if the fanout is outside of the cone
566  if ( Abc_ObjIsCo(pNext) || pNext->Level > (unsigned)LevelLimit )
567  {
568  fObjIsRoot = 1;
569  continue;
570  }
571  // skip the edge under check
572  if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
573  continue;
574  // skip the visited fanouts
575  if ( Abc_NodeIsTravIdCurrent(pNext) )
576  continue;
577  Abc_NodeSetTravIdCurrent( pNext );
578  Vec_PtrPush( vLeaves, pNext );
579  }
580  if ( fObjIsRoot )
581  Vec_PtrPush( vRoots, pObj );
582  }
583  // remove old nodes
584  k = 0;
585  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
586  {
587  if ( LevelMin == (int)pObj->Level )
588  continue;
589  Vec_PtrWriteEntry( vLeaves, k++, pObj );
590  }
591  Vec_PtrShrink( vLeaves, k );
592  if ( Vec_PtrSize(vLeaves) > 2000 )
593  return 0;
594  return 1;
595 }
596 
597 /**Function*************************************************************
598 
599  Synopsis [Collects the roots in the TFO of the node.]
600 
601  Description [Note that this procedure can be improved by
602  marking and skipping the visited nodes.]
603 
604  SideEffects []
605 
606  SeeAlso []
607 
608 ***********************************************************************/
609 int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit )
610 {
611  Abc_Obj_t * pFanout;
612  int i;
613  // if we encountered a node outside of the TFO cone of the fanins, quit
614  if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit )
615  return 0;
616  // if we encountered a node on the boundary, add it to the roots
617  if ( pNode->fMarkA )
618  {
619  Vec_PtrPushUnique( vRoots, pNode );
620  return 1;
621  }
622  // mark the node with the current TravId (needed to have all internal nodes marked)
623  Abc_NodeSetTravIdCurrent( pNode );
624  // traverse the fanouts
625  Abc_ObjForEachFanout( pNode, pFanout, i )
626  if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) )
627  return 0;
628  return 1;
629 }
630 
631 /**Function*************************************************************
632 
633  Synopsis [Collects the leaves and cone of the roots.]
634 
635  Description []
636 
637  SideEffects []
638 
639  SeeAlso []
640 
641 ***********************************************************************/
642 void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, int LevelLimit )
643 {
644  Abc_Obj_t * pFanin;
645  int i;
646  // skip visited nodes
647  if ( Abc_NodeIsTravIdCurrent(pNode) )
648  return;
649  // add node to leaves if it is not in TFI cone of the leaves (marked before) or below the limit
650  if ( !Abc_NodeIsTravIdPrevious(pNode) || (int)pNode->Level <= LevelLimit )
651  {
652  Abc_NodeSetTravIdCurrent( pNode );
653  Vec_PtrPush( vLeaves, pNode );
654  return;
655  }
656  // mark the node as visited
657  Abc_NodeSetTravIdCurrent( pNode );
658  // call for the node's fanins
659  Abc_ObjForEachFanin( pNode, pFanin, i )
660  Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone, LevelLimit );
661  // add the node to the cone in topological order
662  Vec_PtrPush( vCone, pNode );
663 }
664 
665 /**Function*************************************************************
666 
667  Synopsis []
668 
669  Description []
670 
671  SideEffects []
672 
673  SeeAlso []
674 
675 ***********************************************************************/
676 Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots )
677 {
678  Abc_Ntk_t * pNtkNew;
679  Abc_Obj_t * pObj;
680  int fCheck = 1;
681  int i;
682  assert( Abc_NtkIsStrash(pNtk) );
683  // start the network
684  pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
685  // duplicate the name and the spec
686  pNtkNew->pName = Extra_UtilStrsav( "temp" );
687  // map the constant nodes
688  Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
689  // create and map the PIs
690  Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
691  pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
692  // copy the AND gates
693  Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i )
694  pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
695  // compare the number of nodes before and after
696  if ( Vec_PtrSize(vCone) != Abc_NtkNodeNum(pNtkNew) )
697  printf( "Warning: Structural hashing during windowing reduced %d nodes (this is a bug).\n",
698  Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) );
699  // create the POs
700  Vec_PtrForEachEntry( Abc_Obj_t *, vRoots, pObj, i )
701  {
702  assert( !Abc_ObjIsComplement(pObj->pCopy) );
703  Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy );
704  }
705  // add the PI/PO names
706  Abc_NtkAddDummyPiNames( pNtkNew );
707  Abc_NtkAddDummyPoNames( pNtkNew );
708  // check
709  if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
710  {
711  printf( "Abc_NtkWindow: The network check has failed.\n" );
712  return NULL;
713  }
714  return pNtkNew;
715 }
716 
717 
718 /**Function*************************************************************
719 
720  Synopsis [Starts simulation to detect non-redundant edges.]
721 
722  Description []
723 
724  SideEffects []
725 
726  SeeAlso []
727 
728 ***********************************************************************/
729 void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk )
730 {
731  Abc_Obj_t * pObj;
732  unsigned uData, uData0, uData1;
733  int i;
734  Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0);
735  Abc_NtkForEachCi( pNtk, pObj, i )
736  pObj->pData = (void *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED;
737  Abc_NtkForEachNode( pNtk, pObj, i )
738  {
739  if ( i == 0 ) continue;
740  uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
741  uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
742  uData = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
743  uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
744  assert( pObj->pData == NULL );
745  pObj->pData = (void *)(ABC_PTRUINT_T)uData;
746  }
747 }
748 
749 /**Function*************************************************************
750 
751  Synopsis [Stops simulation to detect non-redundant edges.]
752 
753  Description []
754 
755  SideEffects []
756 
757  SeeAlso []
758 
759 ***********************************************************************/
760 void Abc_NtkRRSimulateStop( Abc_Ntk_t * pNtk )
761 {
762  Abc_Obj_t * pObj;
763  int i;
764  Abc_NtkForEachObj( pNtk, pObj, i )
765  pObj->pData = NULL;
766 }
767 
768 
769 
770 
771 
772 
773 
774 static void Sim_TraverseNodes_rec( Abc_Obj_t * pRoot, Vec_Str_t * vTargets, Vec_Ptr_t * vNodes );
775 static void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField );
776 static void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t * vField );
777 
778 /**Function*************************************************************
779 
780  Synopsis [Simulation to detect non-redundant edges.]
781 
782  Description []
783 
784  SideEffects []
785 
786  SeeAlso []
787 
788 ***********************************************************************/
789 Vec_Str_t * Abc_NtkRRSimulate( Abc_Ntk_t * pNtk )
790 {
791  Vec_Ptr_t * vNodes, * vField;
792  Vec_Str_t * vTargets;
793  Abc_Obj_t * pObj;
794  unsigned uData, uData0, uData1;
795  int PrevCi, Phase, i, k;
796 
797  // start the candidates
798  vTargets = Vec_StrStart( Abc_NtkObjNumMax(pNtk) + 1 );
799  Abc_NtkForEachNode( pNtk, pObj, i )
800  {
801  Phase = ((Abc_ObjFanoutNum(Abc_ObjFanin1(pObj)) > 1) << 1);
802  Phase |= (Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) > 1);
803  Vec_StrWriteEntry( vTargets, pObj->Id, (char)Phase );
804  }
805 
806  // simulate patters and store them in copy
807  Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0);
808  Abc_NtkForEachCi( pNtk, pObj, i )
809  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED;
810  Abc_NtkForEachNode( pNtk, pObj, i )
811  {
812  if ( i == 0 ) continue;
813  uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
814  uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
815  uData = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
816  uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
817  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)uData;
818  }
819  // store the result in data
820  Abc_NtkForEachCo( pNtk, pObj, i )
821  {
822  uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
823  if ( Abc_ObjFaninC0(pObj) )
824  pObj->pData = (void *)(ABC_PTRUINT_T)~uData0;
825  else
826  pObj->pData = (void *)(ABC_PTRUINT_T)uData0;
827  }
828 
829  // refine the candidates
830  for ( PrevCi = 0; PrevCi < Abc_NtkCiNum(pNtk); PrevCi = i )
831  {
832  vNodes = Vec_PtrAlloc( 10 );
833  Abc_NtkIncrementTravId( pNtk );
834  for ( i = PrevCi; i < Abc_NtkCiNum(pNtk); i++ )
835  {
836  Sim_TraverseNodes_rec( Abc_NtkCi(pNtk, i), vTargets, vNodes );
837  if ( Vec_PtrSize(vNodes) > 128 )
838  break;
839  }
840  // collect the marked nodes in the topological order
841  vField = Vec_PtrAlloc( 10 );
842  Abc_NtkIncrementTravId( pNtk );
843  Abc_NtkForEachCo( pNtk, pObj, k )
844  Sim_CollectNodes_rec( pObj, vField );
845 
846  // simulate these nodes
847  Sim_SimulateCollected( vTargets, vNodes, vField );
848  // prepare for the next loop
849  Vec_PtrFree( vNodes );
850  }
851 
852  // clean
853  Abc_NtkForEachObj( pNtk, pObj, i )
854  pObj->pData = NULL;
855  return vTargets;
856 }
857 
858 /**Function*************************************************************
859 
860  Synopsis [Collects nodes starting from the given node.]
861 
862  Description []
863 
864  SideEffects []
865 
866  SeeAlso []
867 
868 ***********************************************************************/
869 void Sim_TraverseNodes_rec( Abc_Obj_t * pRoot, Vec_Str_t * vTargets, Vec_Ptr_t * vNodes )
870 {
871  Abc_Obj_t * pFanout;
872  char Entry;
873  int k;
874  if ( Abc_NodeIsTravIdCurrent(pRoot) )
875  return;
876  Abc_NodeSetTravIdCurrent( pRoot );
877  // save the reached targets
878  Entry = Vec_StrEntry(vTargets, pRoot->Id);
879  if ( Entry & 1 )
880  Vec_PtrPush( vNodes, Abc_ObjNot(pRoot) );
881  if ( Entry & 2 )
882  Vec_PtrPush( vNodes, pRoot );
883  // explore the fanouts
884  Abc_ObjForEachFanout( pRoot, pFanout, k )
885  Sim_TraverseNodes_rec( pFanout, vTargets, vNodes );
886 }
887 
888 /**Function*************************************************************
889 
890  Synopsis [Collects nodes starting from the given node.]
891 
892  Description []
893 
894  SideEffects []
895 
896  SeeAlso []
897 
898 ***********************************************************************/
899 void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField )
900 {
901  Abc_Obj_t * pFanin;
902  int i;
903  if ( Abc_NodeIsTravIdCurrent(pRoot) )
904  return;
905  if ( !Abc_NodeIsTravIdPrevious(pRoot) )
906  return;
907  Abc_NodeSetTravIdCurrent( pRoot );
908  Abc_ObjForEachFanin( pRoot, pFanin, i )
909  Sim_CollectNodes_rec( pFanin, vField );
910  if ( !Abc_ObjIsCo(pRoot) )
911  pRoot->pData = (void *)(ABC_PTRUINT_T)Vec_PtrSize(vField);
912  Vec_PtrPush( vField, pRoot );
913 }
914 
915 /**Function*************************************************************
916 
917  Synopsis [Simulate the given nodes.]
918 
919  Description []
920 
921  SideEffects []
922 
923  SeeAlso []
924 
925 ***********************************************************************/
926 void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t * vField )
927 {
928  Abc_Obj_t * pObj, * pFanin0, * pFanin1, * pDisproved;
929  Vec_Ptr_t * vSims;
930  unsigned * pUnsigned, * pUnsignedF;
931  int i, k, Phase, fCompl;
932  // get simulation info
933  vSims = Sim_UtilInfoAlloc( Vec_PtrSize(vField), Vec_PtrSize(vNodes), 0 );
934  // simulate the nodes
935  Vec_PtrForEachEntry( Abc_Obj_t *, vField, pObj, i )
936  {
937  if ( Abc_ObjIsCi(pObj) )
938  {
939  pUnsigned = (unsigned *)Vec_PtrEntry( vSims, i );
940  for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
941  pUnsigned[k] = (unsigned)(ABC_PTRUINT_T)pObj->pCopy;
942  continue;
943  }
944  if ( Abc_ObjIsCo(pObj) )
945  {
946  pUnsigned = (unsigned *)Vec_PtrEntry( vSims, i );
947  pUnsignedF = (unsigned *)Vec_PtrEntry( vSims, (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData );
948  if ( Abc_ObjFaninC0(pObj) )
949  for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
950  pUnsigned[k] = ~pUnsignedF[k];
951  else
952  for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
953  pUnsigned[k] = pUnsignedF[k];
954  // update targets
955  for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
956  {
957  if ( pUnsigned[k] == (unsigned)(ABC_PTRUINT_T)pObj->pData )
958  continue;
959  pDisproved = (Abc_Obj_t *)Vec_PtrEntry( vNodes, k );
960  fCompl = Abc_ObjIsComplement(pDisproved);
961  pDisproved = Abc_ObjRegular(pDisproved);
962  Phase = Vec_StrEntry( vTargets, pDisproved->Id );
963  if ( fCompl )
964  Phase = (Phase & 2);
965  else
966  Phase = (Phase & 1);
967  Vec_StrWriteEntry( vTargets, pDisproved->Id, (char)Phase );
968  }
969  continue;
970  }
971  // simulate the node
972  pFanin0 = Abc_ObjFanin0(pObj);
973  pFanin1 = Abc_ObjFanin1(pObj);
974  }
975 }
976 
977 
978 
979 /*
980  {
981  unsigned uData;
982  if ( pFanin == Abc_ObjFanin0(pNode) )
983  {
984  uData = (unsigned)Abc_ObjFanin1(pNode)->pData;
985  uData = Abc_ObjFaninC1(pNode)? ~uData : uData;
986  }
987  else if ( pFanin == Abc_ObjFanin1(pNode) )
988  {
989  uData = (unsigned)Abc_ObjFanin0(pNode)->pData;
990  uData = Abc_ObjFaninC0(pNode)? ~uData : uData;
991  }
992  uData ^= (unsigned)pNode->pData;
993 // Extra_PrintBinary( stdout, &uData, 32 ); printf( "\n" );
994  if ( Extra_WordCountOnes(uData) > 8 )
995  continue;
996  }
997 */
998 
999 ////////////////////////////////////////////////////////////////////////
1000 /// END OF FILE ///
1001 ////////////////////////////////////////////////////////////////////////
1002 
1003 
1004 ABC_NAMESPACE_IMPL_END
1005 
memset
char * memset()
Abc_NtkRRSimulateStart
static void Abc_NtkRRSimulateStart(Abc_Ntk_t *pNtk)
Definition: abcRr.c:729
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Sim_SimulateCollected
static void Sim_SimulateCollected(Vec_Str_t *vTargets, Vec_Ptr_t *vNodes, Vec_Ptr_t *vField)
Definition: abcRr.c:926
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ObjFanin1
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
Abc_ObjIsCi
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
Abc_NtkRRTfo_int
static int Abc_NtkRRTfo_int(Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int LevelLimit, Abc_Obj_t *pEdgeFanin, Abc_Obj_t *pEdgeFanout)
Definition: abcRr.c:544
Abc_Obj_t_::fMarkA
unsigned fMarkA
Definition: abc.h:134
Abc_NtkObjNumMax
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
Abc_RRMan_t_::pFanin
Abc_Obj_t * pFanin
Definition: abcRr.c:41
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_ObjFaninC1
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Abc_RRManStart
static Abc_RRMan_t * Abc_RRManStart()
Definition: abcRr.c:248
Abc_RRMan_t_::nEdgesRemoved
int nEdgesRemoved
Definition: abcRr.c:58
Abc_NtkRRTfi_int
static int Abc_NtkRRTfi_int(Vec_Ptr_t *vLeaves, int LevelLimit)
Definition: abcRr.c:492
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkRR
int Abc_NtkRR(Abc_Ntk_t *pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: abcRr.c:98
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Abc_RRMan_t_::vCone
Vec_Ptr_t * vCone
Definition: abcRr.c:48
Abc_RRMan_t_::pFanout
Abc_Obj_t * pFanout
Definition: abcRr.c:42
SIM_RANDOM_UNSIGNED
#define SIM_RANDOM_UNSIGNED
Definition: sim.h:158
Abc_RRMan_t_::nEdgesTried
int nEdgesTried
Definition: abcRr.c:57
Abc_ObjChild1Copy
static Abc_Obj_t * Abc_ObjChild1Copy(Abc_Obj_t *pObj)
Definition: abc.h:387
Abc_ObjFaninC0
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
Abc_NtkDup
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:419
Abc_RRMan_t_::pNode
Abc_Obj_t * pNode
Definition: abcRr.c:40
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Abc_NtkCiNum
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Abc_RRMan_t_::vLeaves
Vec_Ptr_t * vLeaves
Definition: abcRr.c:47
Abc_RRMan_t_::pMiter
Abc_Ntk_t * pMiter
Definition: abcRr.c:52
Abc_NtkRRWindow
static int Abc_NtkRRWindow(Abc_RRMan_t *p)
Definition: abcRr.c:429
Abc_NtkCi
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
Prove_ParamsSetDefault
void Prove_ParamsSetDefault(Prove_Params_t *pParams)
FUNCTION DEFINITIONS ///.
Definition: fraigMan.c:46
Abc_RRMan_t_::timeUpdate
abctime timeUpdate
Definition: abcRr.c:62
Abc_NtkMiterProve
ABC_DLL int Abc_NtkMiterProve(Abc_Ntk_t **ppNtk, void *pParams)
FUNCTION DEFINITIONS ///.
Definition: abcProve.c:59
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_NodeIsTravIdPrevious
static int Abc_NodeIsTravIdPrevious(Abc_Obj_t *p)
Definition: abc.h:412
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Abc_RRManClean
static void Abc_RRManClean(Abc_RRMan_t *p)
Definition: abcRr.c:325
Abc_Aig_t_
DECLARATIONS ///.
Definition: abcAig.c:52
Abc_RRMan_t_::timeTotal
abctime timeTotal
Definition: abcRr.c:63
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Abc_Obj_t_::Level
unsigned Level
Definition: abc.h:142
Abc_ObjIsCo
static int Abc_ObjIsCo(Abc_Obj_t *pObj)
Definition: abc.h:352
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Abc_RRMan_t_::vFaninLeaves
Vec_Ptr_t * vFaninLeaves
Definition: abcRr.c:44
Abc_RRMan_t_::nLevelsOld
int nLevelsOld
Definition: abcRr.c:56
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_NtkAlloc
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
Abc_NtkReassignIds
ABC_DLL void Abc_NtkReassignIds(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:1769
Abc_Obj_t_
Definition: abc.h:128
Abc_ObjChild0
static Abc_Obj_t * Abc_ObjChild0(Abc_Obj_t *pObj)
Definition: abc.h:383
Abc_NtkWindow
static Abc_Ntk_t * Abc_NtkWindow(Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vCone, Vec_Ptr_t *vRoots)
Definition: abcRr.c:676
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
Abc_NtkRRSimulate
Vec_Str_t * Abc_NtkRRSimulate(Abc_Ntk_t *pNtk)
Definition: abcRr.c:789
Vec_StrWriteEntry
static void Vec_StrWriteEntry(Vec_Str_t *p, int i, char Entry)
Definition: vecStr.h:370
Abc_AigAnd
ABC_DLL Abc_Obj_t * Abc_AigAnd(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition: abcAig.c:700
Abc_NtkAddDummyPoNames
ABC_DLL void Abc_NtkAddDummyPoNames(Abc_Ntk_t *pNtk)
Definition: abcNames.c:398
Sim_UtilInfoAlloc
Vec_Ptr_t * Sim_UtilInfoAlloc(int nSize, int nWords, int fClean)
FUNCTION DEFINITIONS ///.
Definition: simUtils.c:57
Abc_ObjChild0Copy
static Abc_Obj_t * Abc_ObjChild0Copy(Abc_Obj_t *pObj)
Definition: abc.h:386
ProgressBarStruct
DECLARATIONS ///.
Definition: extraUtilProgress.c:32
Vec_StrEntry
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_RRMan_t_::timeMiter
abctime timeMiter
Definition: abcRr.c:60
Abc_NtkRRSimulateStop
static void Abc_NtkRRSimulateStop(Abc_Ntk_t *pNtk)
Definition: abcRr.c:760
Abc_NtkMiter
ABC_DLL Abc_Ntk_t * Abc_NtkMiter(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb, int nPartSize, int fImplic, int fMulti)
FUNCTION DEFINITIONS ///.
Definition: abcMiter.c:56
Abc_AigLevel
ABC_DLL int Abc_AigLevel(Abc_Ntk_t *pNtk)
Definition: abcAig.c:292
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_StrStart
static Vec_Str_t * Vec_StrStart(int nSize)
Definition: vecStr.h:95
Abc_NtkCreatePi
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Abc_RRMan_t_
Definition: abcRr.c:33
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
Abc_NodeIsPersistant
static int Abc_NodeIsPersistant(Abc_Obj_t *pNode)
Definition: abc.h:401
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
Abc_RRMan_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abcRr.c:36
Abc_NodeIsTravIdCurrent
static int Abc_NodeIsTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:411
Abc_Ntk_t_::pCopy
Abc_Ntk_t * pCopy
Definition: abc.h:204
Abc_ObjRegular
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
Abc_NtkRRProve
static int Abc_NtkRRProve(Abc_RRMan_t *p)
Definition: abcRr.c:352
Abc_RRMan_t
typedefABC_NAMESPACE_IMPL_START struct Abc_RRMan_t_ Abc_RRMan_t
DECLARATIONS ///.
Definition: abcRr.c:32
Abc_RRMan_t_::vRoots
Vec_Ptr_t * vRoots
Definition: abcRr.c:49
Sim_CollectNodes_rec
static void Sim_CollectNodes_rec(Abc_Obj_t *pRoot, Vec_Ptr_t *vField)
Definition: abcRr.c:899
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition: vecPtr.h:59
Abc_ObjForEachFanout
#define Abc_ObjForEachFanout(pObj, pFanout, i)
Definition: abc.h:526
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_RRManPrintStats
static void Abc_RRManPrintStats(Abc_RRMan_t *p)
Definition: abcRr.c:298
Abc_Ntk_t_::ntkFunc
Abc_NtkFunc_t ntkFunc
Definition: abc.h:157
Vec_Str_t_
Definition: bblif.c:47
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Obj_t_::Id
int Id
Definition: abc.h:132
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Abc_NtkIncrementTravId
static void Abc_NtkIncrementTravId(Abc_Ntk_t *p)
Definition: abc.h:406
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
Abc_RRMan_t_::vFanoutRoots
Vec_Ptr_t * vFanoutRoots
Definition: abcRr.c:45
Abc_RRManStop
static void Abc_RRManStop(Abc_RRMan_t *p)
Definition: abcRr.c:275
Abc_NtkRRTfo_rec
static int Abc_NtkRRTfo_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vRoots, int LevelLimit)
Definition: abcRr.c:609
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Abc_NtkIsDfsOrdered
ABC_DLL int Abc_NtkIsDfsOrdered(Abc_Ntk_t *pNtk)
Definition: abcDfs.c:667
Abc_NtkCleanCopy
ABC_DLL void Abc_NtkCleanCopy(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:507
Abc_ObjNotCond
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Abc_ObjNot
static Abc_Obj_t * Abc_ObjNot(Abc_Obj_t *p)
Definition: abc.h:324
Abc_RRMan_t_::nFanoutLevels
int nFanoutLevels
Definition: abcRr.c:38
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Sim_TraverseNodes_rec
static void Sim_TraverseNodes_rec(Abc_Obj_t *pRoot, Vec_Str_t *vTargets, Vec_Ptr_t *vNodes)
Definition: abcRr.c:869
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_RRMan_t_::timeProve
abctime timeProve
Definition: abcRr.c:61
Abc_ObjIsComplement
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
Abc_NtkRRTfi_rec
static void Abc_NtkRRTfi_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vCone, int LevelLimit)
Definition: abcRr.c:642
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_RRMan_t_::timeWindow
abctime timeWindow
Definition: abcRr.c:59
Vec_PtrShrink
static void Vec_PtrShrink(Vec_Ptr_t *p, int nSizeNew)
Definition: vecPtr.h:528
Abc_NtkForEachObj
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
Abc_RRMan_t_::pWnd
Abc_Ntk_t * pWnd
Definition: abcRr.c:50
Abc_NtkLevel
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Definition: abcDfs.c:1265
Abc_NtkAddDummyPiNames
ABC_DLL void Abc_NtkAddDummyPiNames(Abc_Ntk_t *pNtk)
Definition: abcNames.c:378
Abc_NtkCreatePo
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
Abc_ObjChild1
static Abc_Obj_t * Abc_ObjChild1(Abc_Obj_t *pObj)
Definition: abc.h:384
Abc_RRMan_t_::nFaninLevels
int nFaninLevels
Definition: abcRr.c:37
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Abc_NtkRRUpdate
static int Abc_NtkRRUpdate(Abc_Ntk_t *pNtk, Abc_Obj_t *pNode, Abc_Obj_t *pFanin, Abc_Obj_t *pFanout)
Definition: abcRr.c:385
Abc_Ntk_t_::ntkType
Abc_NtkType_t ntkType
Definition: abc.h:156
Prove_ParamsStruct_t_
Definition: ivyFraig.c:109
Abc_RRMan_t_::nNodesOld
int nNodesOld
Definition: abcRr.c:55
Abc_NodeSetTravIdCurrent
static void Abc_NodeSetTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:409
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Abc_AigReplace
ABC_DLL void Abc_AigReplace(Abc_Aig_t *pMan, Abc_Obj_t *pOld, Abc_Obj_t *pNew, int fUpdateLevel)
Definition: abcAig.c:850
Abc_RRMan_t_::pParams
Prove_Params_t * pParams
Definition: abcRr.c:53