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 ***********************************************************************/
Abc_NtkRR(Abc_Ntk_t * pNtk,int nFaninLevels,int nFanoutLevels,int fUseFanouts,int fVerbose)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 ***********************************************************************/
Abc_RRManStart()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 ***********************************************************************/
Abc_RRManStop(Abc_RRMan_t * p)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 ***********************************************************************/
Abc_RRManPrintStats(Abc_RRMan_t * p)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 ***********************************************************************/
Abc_RRManClean(Abc_RRMan_t * p)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 ***********************************************************************/
Abc_NtkRRProve(Abc_RRMan_t * p)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 ***********************************************************************/
Abc_NtkRRUpdate(Abc_Ntk_t * pNtk,Abc_Obj_t * pNode,Abc_Obj_t * pFanin,Abc_Obj_t * pFanout)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 = NULL, * pFanoutNew = NULL;
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 ***********************************************************************/
Abc_NtkRRWindow(Abc_RRMan_t * p)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 ***********************************************************************/
Abc_NtkRRTfi_int(Vec_Ptr_t * vLeaves,int LevelLimit)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 ***********************************************************************/
Abc_NtkRRTfo_int(Vec_Ptr_t * vLeaves,Vec_Ptr_t * vRoots,int LevelLimit,Abc_Obj_t * pEdgeFanin,Abc_Obj_t * pEdgeFanout)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 ***********************************************************************/
Abc_NtkRRTfo_rec(Abc_Obj_t * pNode,Vec_Ptr_t * vRoots,int LevelLimit)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 ***********************************************************************/
Abc_NtkRRTfi_rec(Abc_Obj_t * pNode,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vCone,int LevelLimit)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 ***********************************************************************/
Abc_NtkWindow(Abc_Ntk_t * pNtk,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vCone,Vec_Ptr_t * vRoots)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 ***********************************************************************/
Abc_NtkRRSimulateStart(Abc_Ntk_t * pNtk)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 ***********************************************************************/
Abc_NtkRRSimulateStop(Abc_Ntk_t * pNtk)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 ***********************************************************************/
Abc_NtkRRSimulate(Abc_Ntk_t * pNtk)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 ***********************************************************************/
Sim_TraverseNodes_rec(Abc_Obj_t * pRoot,Vec_Str_t * vTargets,Vec_Ptr_t * vNodes)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 ***********************************************************************/
Sim_CollectNodes_rec(Abc_Obj_t * pRoot,Vec_Ptr_t * vField)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 ***********************************************************************/
Sim_SimulateCollected(Vec_Str_t * vTargets,Vec_Ptr_t * vNodes,Vec_Ptr_t * vField)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
1006