abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb4Sweep.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb2Sweep.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Non-linear quantification scheduling.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb2Sweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.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 [Find good static variable ordering.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Llb_Nonlin4SweepOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter, int fSaveAll )
46 {
47  Aig_Obj_t * pFanin0, * pFanin1;
48  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
49  return;
50  Aig_ObjSetTravIdCurrent( pAig, pObj );
51  assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
52  if ( Aig_ObjIsCi(pObj) )
53  {
54  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
55  return;
56  }
57  // try fanins with higher level first
58  pFanin0 = Aig_ObjFanin0(pObj);
59  pFanin1 = Aig_ObjFanin1(pObj);
60 // if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
61  if ( pFanin0->Level > pFanin1->Level )
62  {
63  Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll );
64  Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll );
65  }
66  else
67  {
68  Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll );
69  Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll );
70  }
71  if ( fSaveAll || pObj->fMarkA )
72  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [Find good static variable ordering.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAll )
87 {
88  Vec_Int_t * vOrder;
89  Aig_Obj_t * pObj;
90  int i, Counter = 0;
91  // collect nodes in the order
92  vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
93  Aig_ManIncrementTravId( pAig );
94  Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
95  Aig_ManForEachCo( pAig, pObj, i )
96  {
97  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
98  Llb_Nonlin4SweepOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter, fSaveAll );
99  }
100  Aig_ManForEachCi( pAig, pObj, i )
101  if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
102  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
103 // assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes
104  if ( pCounter )
105  *pCounter = Counter - Aig_ManCiNum(pAig) - Aig_ManCoNum(pAig);
106  return vOrder;
107 }
108 
109 
110 /**Function*************************************************************
111 
112  Synopsis [Performs BDD sweep on the netlist.]
113 
114  Description [Returns AIG with internal cut points labeled with fMarkA.]
115 
116  SideEffects []
117 
118  SeeAlso []
119 
120 ***********************************************************************/
121 int Llb4_Nonlin4SweepCutpoints( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nBddLimit, int fVerbose )
122 {
123  DdManager * dd;
124  DdNode * bFunc0, * bFunc1, * bFunc;
125  Aig_Obj_t * pObj;
126  int i, Counter = 0, Counter1 = 0;
127  dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
128  // assign elementary variables
129  Aig_ManCleanData( pAig );
130  Aig_ManForEachCi( pAig, pObj, i )
131  pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
132  // sweep internal nodes
133  Aig_ManForEachNode( pAig, pObj, i )
134  {
135 /*
136  if ( pObj->nRefs >= 4 )
137  {
138  bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); Cudd_Ref( bFunc );
139  pObj->pData = bFunc;
140  Counter1++;
141  continue;
142  }
143 */
144  bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
145  bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
146  bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
147  if ( Cudd_DagSize(bFunc) > nBddLimit )
148  {
149 // if ( fVerbose )
150 // printf( "Node %5d : Beg =%5d. ", i, Cudd_DagSize(bFunc) );
151 
152  // add cutpoint at a larger one
153  Cudd_RecursiveDeref( dd, bFunc );
154  if ( Cudd_DagSize(bFunc0) >= Cudd_DagSize(bFunc1) )
155  {
156  Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin0(pObj)->pData );
157  bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin0(pObj)) );
158  Aig_ObjFanin0(pObj)->pData = bFunc; Cudd_Ref( bFunc );
159  Aig_ObjFanin0(pObj)->fMarkA = 1;
160 
161 // if ( fVerbose )
162 // printf( "Ref =%3d ", Aig_ObjFanin0(pObj)->nRefs );
163  }
164  else
165  {
166  Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin1(pObj)->pData );
167  bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin1(pObj)) );
168  Aig_ObjFanin1(pObj)->pData = bFunc; Cudd_Ref( bFunc );
169  Aig_ObjFanin1(pObj)->fMarkA = 1;
170 
171 // if ( fVerbose )
172 // printf( "Ref =%3d ", Aig_ObjFanin1(pObj)->nRefs );
173  }
174  // perform new operation
175  bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
176  bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
177  bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
178 // assert( Cudd_DagSize(bFunc) <= nBddLimit );
179 
180 // if ( fVerbose )
181 // printf( "End =%5d.\n", Cudd_DagSize(bFunc) );
182  Counter++;
183  }
184  pObj->pData = bFunc;
185 //printf( "%d ", Cudd_DagSize(bFunc) );
186  }
187 //printf( "\n" );
188  // clean up
189  Aig_ManForEachNode( pAig, pObj, i )
190  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
191  Extra_StopManager( dd );
192 // Aig_ManCleanMarkA( pAig );
193  if ( fVerbose )
194  printf( "Added %d cut points. Used %d high fanout points.\n", Counter, Counter1 );
195  return Counter + Counter1;
196 }
197 
198 /**Function*************************************************************
199 
200  Synopsis [Derives BDDs for the partitions.]
201 
202  Description []
203 
204  SideEffects []
205 
206  SeeAlso []
207 
208 ***********************************************************************/
209 DdNode * Llb_Nonlin4SweepPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots )
210 {
211  DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
212  if ( Aig_ObjIsConst1(pObj) )
213  return Cudd_ReadOne(dd);
214  if ( Aig_ObjIsCi(pObj) )
215  return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
216  if ( pObj->pData )
217  return (DdNode *)pObj->pData;
218  if ( Aig_ObjIsCo(pObj) )
219  {
220  bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
221  bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart );
222  Vec_PtrPush( vRoots, bPart );
223  return NULL;
224  }
225  bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
226  bBdd1 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) );
227  bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
228  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
229  {
230  vVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
231  bPart = Cudd_bddXnor( dd, vVar, bBdd ); Cudd_Ref( bPart );
232  Vec_PtrPush( vRoots, bPart );
233  Cudd_RecursiveDeref( dd, bBdd );
234  bBdd = vVar; Cudd_Ref( vVar );
235  }
236  pObj->pData = bBdd;
237  return bBdd;
238 }
239 
240 /**Function*************************************************************
241 
242  Synopsis [Derives BDDs for the partitions.]
243 
244  Description []
245 
246  SideEffects []
247 
248  SeeAlso []
249 
250 ***********************************************************************/
251 Vec_Ptr_t * Llb_Nonlin4SweepPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fTransition )
252 {
253  Vec_Ptr_t * vRoots;
254  Aig_Obj_t * pObj;
255  int i;
256  Aig_ManCleanData( pAig );
257  vRoots = Vec_PtrAlloc( 100 );
258  if ( fTransition )
259  {
260  Saig_ManForEachLi( pAig, pObj, i )
261  Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots );
262  }
263  else
264  {
265  Saig_ManForEachPo( pAig, pObj, i )
266  Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots );
267  }
268  Aig_ManForEachNode( pAig, pObj, i )
269  if ( pObj->pData )
270  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
271  return vRoots;
272 }
273 
274 /**Function*************************************************************
275 
276  Synopsis [Get bad state monitor.]
277 
278  Description []
279 
280  SideEffects []
281 
282  SeeAlso []
283 
284 ***********************************************************************/
285 DdNode * Llb4_Nonlin4SweepBadMonitor( Aig_Man_t * pAig, Vec_Int_t * vOrder, DdManager * dd )
286 {
287  Aig_Obj_t * pObj;
288  DdNode * bRes, * bVar, * bTemp;
289  int i;
290  abctime TimeStop;
291  TimeStop = dd->TimeStop; dd->TimeStop = 0;
292  bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
293  Saig_ManForEachPo( pAig, pObj, i )
294  {
295  bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
296  bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
297  Cudd_RecursiveDeref( dd, bTemp );
298  }
299  Cudd_Deref( bRes );
300  dd->TimeStop = TimeStop;
301  return Cudd_Not(bRes);
302 }
303 
304 /**Function*************************************************************
305 
306  Synopsis [Creates quantifiable variables for both types of traversal.]
307 
308  Description []
309 
310  SideEffects []
311 
312  SeeAlso []
313 
314 ***********************************************************************/
315 Vec_Int_t * Llb_Nonlin4SweepVars2Q( Aig_Man_t * pAig, Vec_Int_t * vOrder, int fAddLis )
316 {
317  Vec_Int_t * vVars2Q;
318  Aig_Obj_t * pObj;
319  int i;
320  vVars2Q = Vec_IntAlloc( 0 );
321  Vec_IntFill( vVars2Q, Aig_ManObjNumMax(pAig), 1 );
322  // add flop outputs
323  Saig_ManForEachLo( pAig, pObj, i )
324  Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
325  // add flop inputs
326  if ( fAddLis )
327  Saig_ManForEachLi( pAig, pObj, i )
328  Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
329  return vVars2Q;
330 }
331 
332 /**Function*************************************************************
333 
334  Synopsis [Multiply every partition by the cube.]
335 
336  Description []
337 
338  SideEffects []
339 
340  SeeAlso []
341 
342 ***********************************************************************/
343 void Llb_Nonlin4SweepDeref( DdManager * dd, Vec_Ptr_t * vParts )
344 {
345  DdNode * bFunc;
346  int i;
347  Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
348  Cudd_RecursiveDeref( dd, bFunc );
349  Vec_PtrFree( vParts );
350 }
351 
352 /**Function*************************************************************
353 
354  Synopsis [Multiply every partition by the cube.]
355 
356  Description []
357 
358  SideEffects []
359 
360  SeeAlso []
361 
362 ***********************************************************************/
363 void Llb_Nonlin4SweepPrint( Vec_Ptr_t * vFuncs )
364 {
365  DdNode * bFunc;
366  int i;
367  printf( "(%d) ", Vec_PtrSize(vFuncs) );
368  Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
369  printf( "%d ", Cudd_DagSize(bFunc) );
370  printf( "\n" );
371 }
372 
373 /**Function*************************************************************
374 
375  Synopsis [Computes bad states.]
376 
377  Description []
378 
379  SideEffects []
380 
381  SeeAlso []
382 
383 ***********************************************************************/
384 DdManager * Llb4_Nonlin4SweepBadStates( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nVars )
385 {
386  DdManager * dd;
387  Vec_Ptr_t * vParts;
388  Vec_Int_t * vVars2Q;
389  DdNode * bMonitor, * bImage;
390  // get quantifiable variables
391  vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 0 );
392  // start BDD manager and create partitions
393  dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
394  vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 0 );
395 //printf( "Outputs: " );
396 //Llb_Nonlin4SweepPrint( vParts );
397  // compute image of the partitions
398  bMonitor = Llb4_Nonlin4SweepBadMonitor( pAig, vOrder, dd ); Cudd_Ref( bMonitor );
399  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
400  bImage = Llb_Nonlin4Image( dd, vParts, bMonitor, vVars2Q ); Cudd_Ref( bImage );
401  Cudd_RecursiveDeref( dd, bMonitor );
402  Llb_Nonlin4SweepDeref( dd, vParts );
403  Vec_IntFree( vVars2Q );
404  // save image and return
405  dd->bFunc = bImage;
406  return dd;
407 }
408 
409 /**Function*************************************************************
410 
411  Synopsis [Computes clusters.]
412 
413  Description []
414 
415  SideEffects []
416 
417  SeeAlso []
418 
419 ***********************************************************************/
420 DdManager * Llb4_Nonlin4SweepGroups( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nVars, Vec_Ptr_t ** pvGroups, int nBddLimitClp, int fVerbose )
421 {
422  DdManager * dd;
423  Vec_Ptr_t * vParts;
424  Vec_Int_t * vVars2Q;
425  // get quantifiable variables
426  vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 1 );
427  // start BDD manager and create partitions
428  dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
429  vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 1 );
430 //printf( "Transitions: " );
431 //Llb_Nonlin4SweepPrint( vParts );
432  // compute image of the partitions
433 
434  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
435  *pvGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddLimitClp );
436  Llb_Nonlin4SweepDeref( dd, vParts );
437 // *pvGroups = vParts;
438 
439 if ( fVerbose )
440 {
441 printf( "Groups: " );
442 Llb_Nonlin4SweepPrint( *pvGroups );
443 }
444 
445  Vec_IntFree( vVars2Q );
446  return dd;
447 }
448 
449 
450 /**Function*************************************************************
451 
452  Synopsis [Creates quantifiable variables for both types of traversal.]
453 
454  Description []
455 
456  SideEffects []
457 
458  SeeAlso []
459 
460 ***********************************************************************/
461 void Llb_Nonlin4SweepPrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups, int fVerbose )
462 {
463  Aig_Obj_t * pObj;
464  int i, * pSupp;
465  int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;
466 
467  pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
468  Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );
469 
470  Aig_ManForEachObj( pAig, pObj, i )
471  {
472  if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
473  continue;
474  // remove variables that do not participate
475  if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 )
476  {
477  if ( Aig_ObjIsNode(pObj) )
478  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
479  continue;
480  }
481  nSuppAll++;
482  if ( Saig_ObjIsPi(pAig, pObj) )
483  nSuppPi++;
484  else if ( Saig_ObjIsLo(pAig, pObj) )
485  nSuppLo++;
486  else if ( Saig_ObjIsPo(pAig, pObj) )
487  nSuppPo++;
488  else if ( Saig_ObjIsLi(pAig, pObj) )
489  nSuppLi++;
490  else
491  nSuppAnd++;
492  }
493  ABC_FREE( pSupp );
494 
495  if ( fVerbose )
496  {
497  printf( "Groups =%3d ", Vec_PtrSize(vGroups) );
498  printf( "Variables: all =%4d ", nSuppAll );
499  printf( "pi =%4d ", nSuppPi );
500  printf( "po =%4d ", nSuppPo );
501  printf( "lo =%4d ", nSuppLo );
502  printf( "li =%4d ", nSuppLi );
503  printf( "and =%4d", nSuppAnd );
504  printf( "\n" );
505  }
506 }
507 
508 /**Function*************************************************************
509 
510  Synopsis [Performs BDD sweep on the netlist.]
511 
512  Description [Returns BDD manager, ordering, clusters, and bad states
513  inside dd->bFunc.]
514 
515  SideEffects []
516 
517  SeeAlso []
518 
519 ***********************************************************************/
520 void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose )
521 {
522  DdManager * ddBad, * ddWork;
523  Vec_Ptr_t * vGroups;
524  Vec_Int_t * vOrder;
525  int Counter, nCutPoints;
526 
527  // get the original ordering
528  Aig_ManCleanMarkA( pAig );
529  vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 1 );
530  assert( Counter == Aig_ManNodeNum(pAig) );
531  // mark the nodes
532  nCutPoints = Llb4_Nonlin4SweepCutpoints( pAig, vOrder, nSweepMax, fVerbose );
533  Vec_IntFree( vOrder );
534  // get better ordering
535  vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 0 );
536  assert( Counter == nCutPoints );
537  Aig_ManCleanMarkA( pAig );
538  // compute the BAD states
539  ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) );
540  // compute the clusters
541  ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose );
542  // transfer the result from the Bad manager
543 //printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) );
544  ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc ); Cudd_Ref( ddWork->bFunc );
545  Cudd_RecursiveDeref( ddBad, ddBad->bFunc ); ddBad->bFunc = NULL;
546  Extra_StopManager( ddBad );
547  // update ordering to exclude quantified variables
548 //printf( "Bad after = %d.\n", Cudd_DagSize(ddWork->bFunc) );
549 
550  Llb_Nonlin4SweepPrintSuppProfile( ddWork, pAig, vOrder, vGroups, fVerbose );
551 
552  // return the result
553  *pdd = ddWork;
554  *pvOrder = vOrder;
555  *pvGroups = vGroups;
556 }
557 
558 /**Function*************************************************************
559 
560  Synopsis [Performs BDD sweep on the netlist.]
561 
562  Description []
563 
564  SideEffects []
565 
566  SeeAlso []
567 
568 ***********************************************************************/
569 void Llb4_Nonlin4SweepExperiment( Aig_Man_t * pAig )
570 {
571  DdManager * dd;
572  Vec_Int_t * vOrder;
573  Vec_Ptr_t * vGroups;
574  Llb4_Nonlin4Sweep( pAig, 100, 500, &dd, &vOrder, &vGroups, 1 );
575 
576  Llb_Nonlin4SweepDeref( dd, vGroups );
577 
578  Cudd_RecursiveDeref( dd, dd->bFunc );
579  Extra_StopManager( dd );
580  Vec_IntFree( vOrder );
581 }
582 
583 ////////////////////////////////////////////////////////////////////////
584 /// END OF FILE ///
585 ////////////////////////////////////////////////////////////////////////
586 
587 
588 ABC_NAMESPACE_IMPL_END
589 
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Llb4_Nonlin4Sweep
void Llb4_Nonlin4Sweep(Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)
Definition: llb4Sweep.c:520
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Llb_Nonlin4SweepPrint
void Llb_Nonlin4SweepPrint(Vec_Ptr_t *vFuncs)
Definition: llb4Sweep.c:363
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdManager::TimeStop
abctime TimeStop
Definition: cuddInt.h:489
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Llb_Nonlin4SweepPartitions_rec
DdNode * Llb_Nonlin4SweepPartitions_rec(DdManager *dd, Aig_Obj_t *pObj, Vec_Int_t *vOrder, Vec_Ptr_t *vRoots)
Definition: llb4Sweep.c:209
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
DdManager::bFunc
DdNode * bFunc
Definition: cuddInt.h:487
Llb_Nonlin4SweepPrintSuppProfile
void Llb_Nonlin4SweepPrintSuppProfile(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups, int fVerbose)
Definition: llb4Sweep.c:461
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
Extra_VectorSupportArray
int * Extra_VectorSupportArray(DdManager *dd, DdNode **F, int n, int *support)
Definition: extraBddMisc.c:572
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
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
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
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Cudd_bddTransfer
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: cuddBridge.c:409
Llb4_Nonlin4SweepExperiment
void Llb4_Nonlin4SweepExperiment(Aig_Man_t *pAig)
Definition: llb4Sweep.c:569
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
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Llb_Nonlin4SweepPartitions
Vec_Ptr_t * Llb_Nonlin4SweepPartitions(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fTransition)
Definition: llb4Sweep.c:251
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Llb_Nonlin4Group
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
Definition: llb4Image.c:806
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
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
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
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Llb_Nonlin4Image
DdNode * Llb_Nonlin4Image(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
Definition: llb4Image.c:752
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
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
Llb_ObjBddVar
static int Llb_ObjBddVar(Vec_Int_t *vOrder, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: llbInt.h:109
Llb_Nonlin4SweepOrder
Vec_Int_t * Llb_Nonlin4SweepOrder(Aig_Man_t *pAig, int *pCounter, int fSaveAll)
Definition: llb4Sweep.c:86
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Llb_Nonlin4SweepDeref
void Llb_Nonlin4SweepDeref(DdManager *dd, Vec_Ptr_t *vParts)
Definition: llb4Sweep.c:343
Llb4_Nonlin4SweepBadMonitor
DdNode * Llb4_Nonlin4SweepBadMonitor(Aig_Man_t *pAig, Vec_Int_t *vOrder, DdManager *dd)
Definition: llb4Sweep.c:285
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
Llb4_Nonlin4SweepGroups
DdManager * Llb4_Nonlin4SweepGroups(Aig_Man_t *pAig, Vec_Int_t *vOrder, int nVars, Vec_Ptr_t **pvGroups, int nBddLimitClp, int fVerbose)
Definition: llb4Sweep.c:420
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Llb_Nonlin4SweepVars2Q
Vec_Int_t * Llb_Nonlin4SweepVars2Q(Aig_Man_t *pAig, Vec_Int_t *vOrder, int fAddLis)
Definition: llb4Sweep.c:315
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Llb4_Nonlin4SweepBadStates
DdManager * Llb4_Nonlin4SweepBadStates(Aig_Man_t *pAig, Vec_Int_t *vOrder, int nVars)
Definition: llb4Sweep.c:384
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
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
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Llb_Nonlin4SweepOrder_rec
ABC_NAMESPACE_IMPL_START void Llb_Nonlin4SweepOrder_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vOrder, int *pCounter, int fSaveAll)
DECLARATIONS ///.
Definition: llb4Sweep.c:45
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Vec_PtrArray
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Llb4_Nonlin4SweepCutpoints
int Llb4_Nonlin4SweepCutpoints(Aig_Man_t *pAig, Vec_Int_t *vOrder, int nBddLimit, int fVerbose)
Definition: llb4Sweep.c:121
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223