1 /**CFile****************************************************************
2
3 FileName [fraClass.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 /*
27 The candidate equivalence classes are stored as a vector of pointers
28 to the array of pointers to the nodes in each class.
29 The first node of the class is its representative node.
30 The representative has the smallest topological order among the class nodes.
31 The nodes inside each class are ordered according to their topological order.
32 The classes are ordered according to the topological order of their representatives.
33 The array of pointers to the class nodes is terminated with a NULL pointer.
34 To enable dynamic addition of new classes (during class refinement),
35 each array has at least as many NULLs in the end, as there are nodes in the class.
36 */
37
38 ////////////////////////////////////////////////////////////////////////
39 /// DECLARATIONS ///
40 ////////////////////////////////////////////////////////////////////////
41
Fra_ObjNext(Aig_Obj_t ** ppNexts,Aig_Obj_t * pObj)42 static inline Aig_Obj_t * Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
Fra_ObjSetNext(Aig_Obj_t ** ppNexts,Aig_Obj_t * pObj,Aig_Obj_t * pNext)43 static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
44
45 ////////////////////////////////////////////////////////////////////////
46 /// FUNCTION DEFINITIONS ///
47 ////////////////////////////////////////////////////////////////////////
48
49 /**Function*************************************************************
50
51 Synopsis [Starts representation of equivalence classes.]
52
53 Description []
54
55 SideEffects []
56
57 SeeAlso []
58
59 ***********************************************************************/
Fra_ClassesStart(Aig_Man_t * pAig)60 Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
61 {
62 Fra_Cla_t * p;
63 p = ABC_ALLOC( Fra_Cla_t, 1 );
64 memset( p, 0, sizeof(Fra_Cla_t) );
65 p->pAig = pAig;
66 p->pMemRepr = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
67 memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
68 p->vClasses = Vec_PtrAlloc( 100 );
69 p->vClasses1 = Vec_PtrAlloc( 100 );
70 p->vClassesTemp = Vec_PtrAlloc( 100 );
71 p->vClassOld = Vec_PtrAlloc( 100 );
72 p->vClassNew = Vec_PtrAlloc( 100 );
73 p->pFuncNodeHash = Fra_SmlNodeHash;
74 p->pFuncNodeIsConst = Fra_SmlNodeIsConst;
75 p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
76 return p;
77 }
78
79 /**Function*************************************************************
80
81 Synopsis [Stop representation of equivalence classes.]
82
83 Description []
84
85 SideEffects []
86
87 SeeAlso []
88
89 ***********************************************************************/
Fra_ClassesStop(Fra_Cla_t * p)90 void Fra_ClassesStop( Fra_Cla_t * p )
91 {
92 ABC_FREE( p->pMemClasses );
93 ABC_FREE( p->pMemRepr );
94 if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
95 if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
96 if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
97 if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 );
98 if ( p->vClasses ) Vec_PtrFree( p->vClasses );
99 if ( p->vImps ) Vec_IntFree( p->vImps );
100 ABC_FREE( p );
101 }
102
103 /**Function*************************************************************
104
105 Synopsis [Starts representation of equivalence classes.]
106
107 Description []
108
109 SideEffects []
110
111 SeeAlso []
112
113 ***********************************************************************/
Fra_ClassesCopyReprs(Fra_Cla_t * p,Vec_Ptr_t * vFailed)114 void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
115 {
116 Aig_Obj_t * pObj;
117 int i;
118 Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
119 memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
120 if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
121 {
122 Aig_ManForEachObj( p->pAig, pObj, i )
123 {
124 if ( p->pAig->pReprs[i] != NULL )
125 printf( "Classes are not cleared!\n" );
126 assert( p->pAig->pReprs[i] == NULL );
127 }
128 }
129 if ( vFailed )
130 Vec_PtrForEachEntry( Aig_Obj_t *, vFailed, pObj, i )
131 p->pAig->pReprs[pObj->Id] = NULL;
132 }
133
134 /**Function*************************************************************
135
136 Synopsis [Prints simulation classes.]
137
138 Description []
139
140 SideEffects []
141
142 SeeAlso []
143
144 ***********************************************************************/
Fra_ClassCount(Aig_Obj_t ** pClass)145 int Fra_ClassCount( Aig_Obj_t ** pClass )
146 {
147 Aig_Obj_t * pTemp;
148 int i;
149 for ( i = 0; (pTemp = pClass[i]); i++ );
150 return i;
151 }
152
153 /**Function*************************************************************
154
155 Synopsis [Count the number of literals.]
156
157 Description []
158
159 SideEffects []
160
161 SeeAlso []
162
163 ***********************************************************************/
Fra_ClassesCountLits(Fra_Cla_t * p)164 int Fra_ClassesCountLits( Fra_Cla_t * p )
165 {
166 Aig_Obj_t ** pClass;
167 int i, nNodes, nLits = 0;
168 nLits = Vec_PtrSize( p->vClasses1 );
169 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
170 {
171 nNodes = Fra_ClassCount( pClass );
172 assert( nNodes > 1 );
173 nLits += nNodes - 1;
174 }
175 return nLits;
176 }
177
178 /**Function*************************************************************
179
180 Synopsis [Count the number of pairs.]
181
182 Description []
183
184 SideEffects []
185
186 SeeAlso []
187
188 ***********************************************************************/
Fra_ClassesCountPairs(Fra_Cla_t * p)189 int Fra_ClassesCountPairs( Fra_Cla_t * p )
190 {
191 Aig_Obj_t ** pClass;
192 int i, nNodes, nPairs = 0;
193 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
194 {
195 nNodes = Fra_ClassCount( pClass );
196 assert( nNodes > 1 );
197 nPairs += nNodes * (nNodes - 1) / 2;
198 }
199 return nPairs;
200 }
201
202 /**Function*************************************************************
203
204 Synopsis [Prints simulation classes.]
205
206 Description []
207
208 SideEffects []
209
210 SeeAlso []
211
212 ***********************************************************************/
Fra_PrintClass(Fra_Cla_t * p,Aig_Obj_t ** pClass)213 void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass )
214 {
215 Aig_Obj_t * pTemp;
216 int i;
217 for ( i = 1; (pTemp = pClass[i]); i++ )
218 assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
219 printf( "{ " );
220 for ( i = 0; (pTemp = pClass[i]); i++ )
221 printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
222 printf( "}\n" );
223 }
224
225 /**Function*************************************************************
226
227 Synopsis [Prints simulation classes.]
228
229 Description []
230
231 SideEffects []
232
233 SeeAlso []
234
235 ***********************************************************************/
Fra_ClassesPrint(Fra_Cla_t * p,int fVeryVerbose)236 void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
237 {
238 Aig_Obj_t ** pClass;
239 Aig_Obj_t * pObj;
240 int i;
241
242 printf( "Const = %5d. Class = %5d. Lit = %5d. ",
243 Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
244 if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
245 printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
246 printf( "\n" );
247
248 if ( fVeryVerbose )
249 {
250 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
251 assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
252 printf( "Constants { " );
253 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
254 printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
255 printf( "}\n" );
256 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
257 {
258 printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
259 Fra_PrintClass( p, pClass );
260 }
261 printf( "\n" );
262 }
263 }
264
265 /**Function*************************************************************
266
267 Synopsis [Creates initial simulation classes.]
268
269 Description [Assumes that simulation info is assigned.]
270
271 SideEffects []
272
273 SeeAlso []
274
275 ***********************************************************************/
Fra_ClassesPrepare(Fra_Cla_t * p,int fLatchCorr,int nMaxLevs)276 void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
277 {
278 Aig_Obj_t ** ppTable, ** ppNexts;
279 Aig_Obj_t * pObj, * pTemp;
280 int i, k, nTableSize, nEntries, nNodes, iEntry;
281
282 // allocate the hash table hashing simulation info into nodes
283 nTableSize = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
284 ppTable = ABC_FALLOC( Aig_Obj_t *, nTableSize );
285 ppNexts = ABC_FALLOC( Aig_Obj_t *, nTableSize );
286 memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
287
288 // add all the nodes to the hash table
289 Vec_PtrClear( p->vClasses1 );
290 Aig_ManForEachObj( p->pAig, pObj, i )
291 {
292 if ( fLatchCorr )
293 {
294 if ( !Aig_ObjIsCi(pObj) )
295 continue;
296 }
297 else
298 {
299 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
300 continue;
301 // skip the node with more that the given number of levels
302 if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
303 continue;
304 }
305 // hash the node by its simulation info
306 iEntry = p->pFuncNodeHash( pObj, nTableSize );
307 // check if the node belongs to the class of constant 1
308 if ( p->pFuncNodeIsConst( pObj ) )
309 {
310 Vec_PtrPush( p->vClasses1, pObj );
311 Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
312 continue;
313 }
314 // add the node to the class
315 if ( ppTable[iEntry] == NULL )
316 {
317 ppTable[iEntry] = pObj;
318 Fra_ObjSetNext( ppNexts, pObj, pObj );
319 }
320 else
321 {
322 Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
323 Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
324 }
325 }
326
327 // count the total number of nodes in the non-trivial classes
328 // mark the representative nodes of each equivalence class
329 nEntries = 0;
330 for ( i = 0; i < nTableSize; i++ )
331 if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
332 {
333 for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1;
334 pTemp != ppTable[i];
335 pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
336 assert( k > 1 );
337 nEntries += k;
338 // mark the node
339 assert( ppTable[i]->fMarkA == 0 );
340 ppTable[i]->fMarkA = 1;
341 }
342
343 // allocate room for classes
344 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
345 p->pMemClassesFree = p->pMemClasses + 2*nEntries;
346
347 // copy the entries into storage in the topological order
348 Vec_PtrClear( p->vClasses );
349 nEntries = 0;
350 Aig_ManForEachObj( p->pAig, pObj, i )
351 {
352 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
353 continue;
354 // skip the nodes that are not representatives of non-trivial classes
355 if ( pObj->fMarkA == 0 )
356 continue;
357 pObj->fMarkA = 0;
358 // add the class of nodes
359 Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
360 // count the number of entries in this class
361 for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1;
362 pTemp != pObj;
363 pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
364 nNodes = k;
365 assert( nNodes > 1 );
366 // add the nodes to the class in the topological order
367 p->pMemClasses[2*nEntries] = pObj;
368 for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1;
369 pTemp != pObj;
370 pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
371 {
372 p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
373 Fra_ClassObjSetRepr( pTemp, pObj );
374 }
375 // add as many empty entries
376 p->pMemClasses[2*nEntries + nNodes] = NULL;
377 // increment the number of entries
378 nEntries += k;
379 }
380 ABC_FREE( ppTable );
381 ABC_FREE( ppNexts );
382 // now it is time to refine the classes
383 Fra_ClassesRefine( p );
384 // Fra_ClassesPrint( p, 0 );
385 }
386
387 /**Function*************************************************************
388
389 Synopsis [Refines one class using simulation info.]
390
391 Description [Returns the new class if refinement happened.]
392
393 SideEffects []
394
395 SeeAlso []
396
397 ***********************************************************************/
Fra_RefineClassOne(Fra_Cla_t * p,Aig_Obj_t ** ppClass)398 Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
399 {
400 Aig_Obj_t * pObj, ** ppThis;
401 int i;
402 assert( ppClass[0] != NULL && ppClass[1] != NULL );
403
404 // check if the class is going to be refined
405 for ( ppThis = ppClass + 1; (pObj = *ppThis); ppThis++ )
406 if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
407 break;
408 if ( pObj == NULL )
409 return NULL;
410 // split the class
411 Vec_PtrClear( p->vClassOld );
412 Vec_PtrClear( p->vClassNew );
413 Vec_PtrPush( p->vClassOld, ppClass[0] );
414 for ( ppThis = ppClass + 1; (pObj = *ppThis); ppThis++ )
415 if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
416 Vec_PtrPush( p->vClassOld, pObj );
417 else
418 Vec_PtrPush( p->vClassNew, pObj );
419 /*
420 printf( "Refining class (" );
421 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
422 printf( "%d,", pObj->Id );
423 printf( ") + (" );
424 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
425 printf( "%d,", pObj->Id );
426 printf( ")\n" );
427 */
428 // put the nodes back into the class memory
429 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
430 {
431 ppClass[i] = pObj;
432 ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
433 Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
434 }
435 ppClass += 2*Vec_PtrSize(p->vClassOld);
436 // put the new nodes into the class memory
437 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
438 {
439 ppClass[i] = pObj;
440 ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
441 Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
442 }
443 return ppClass;
444 }
445
446 /**Function*************************************************************
447
448 Synopsis [Iteratively refines the classes after simulation.]
449
450 Description [Returns the number of refinements performed.]
451
452 SideEffects []
453
454 SeeAlso []
455
456 ***********************************************************************/
Fra_RefineClassLastIter(Fra_Cla_t * p,Vec_Ptr_t * vClasses)457 int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
458 {
459 Aig_Obj_t ** pClass, ** pClass2;
460 int nRefis;
461 pClass = (Aig_Obj_t **)Vec_PtrEntryLast( vClasses );
462 for ( nRefis = 0; (pClass2 = Fra_RefineClassOne( p, pClass )); nRefis++ )
463 {
464 // if the original class is trivial, remove it
465 if ( pClass[1] == NULL )
466 Vec_PtrPop( vClasses );
467 // if the new class is trivial, stop
468 if ( pClass2[1] == NULL )
469 {
470 nRefis++;
471 break;
472 }
473 // othewise, add the class and continue
474 assert( pClass2[0] != NULL );
475 Vec_PtrPush( vClasses, pClass2 );
476 pClass = pClass2;
477 }
478 return nRefis;
479 }
480
481 /**Function*************************************************************
482
483 Synopsis [Refines the classes after simulation.]
484
485 Description [Assumes that simulation info is assigned. Returns the
486 number of classes refined.]
487
488 SideEffects []
489
490 SeeAlso []
491
492 ***********************************************************************/
Fra_ClassesRefine(Fra_Cla_t * p)493 int Fra_ClassesRefine( Fra_Cla_t * p )
494 {
495 Vec_Ptr_t * vTemp;
496 Aig_Obj_t ** pClass;
497 int i, nRefis;
498 // refine the classes
499 nRefis = 0;
500 Vec_PtrClear( p->vClassesTemp );
501 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
502 {
503 // add the class to the new array
504 assert( pClass[0] != NULL );
505 Vec_PtrPush( p->vClassesTemp, pClass );
506 // refine the class iteratively
507 nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
508 }
509 // exchange the class representation
510 vTemp = p->vClassesTemp;
511 p->vClassesTemp = p->vClasses;
512 p->vClasses = vTemp;
513 return nRefis;
514 }
515
516 /**Function*************************************************************
517
518 Synopsis [Refines constant 1 equivalence class.]
519
520 Description []
521
522 SideEffects []
523
524 SeeAlso []
525
526 ***********************************************************************/
Fra_ClassesRefine1(Fra_Cla_t * p,int fRefineNewClass,int * pSkipped)527 int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
528 {
529 Aig_Obj_t * pObj, ** ppClass;
530 int i, k, nRefis = 1;
531 // check if there is anything to refine
532 if ( Vec_PtrSize(p->vClasses1) == 0 )
533 return 0;
534 // make sure constant 1 class contains only non-constant nodes
535 assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
536 // collect all the nodes to be refined
537 k = 0;
538 Vec_PtrClear( p->vClassNew );
539 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
540 {
541 if ( p->pFuncNodeIsConst( pObj ) )
542 Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
543 else
544 Vec_PtrPush( p->vClassNew, pObj );
545 }
546 Vec_PtrShrink( p->vClasses1, k );
547 if ( Vec_PtrSize(p->vClassNew) == 0 )
548 return 0;
549 /*
550 printf( "Refined const-1 class: {" );
551 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
552 printf( " %d", pObj->Id );
553 printf( " }\n" );
554 */
555 if ( Vec_PtrSize(p->vClassNew) == 1 )
556 {
557 Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL );
558 return 1;
559 }
560 // create a new class composed of these nodes
561 ppClass = p->pMemClassesFree;
562 p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
563 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
564 {
565 ppClass[i] = pObj;
566 ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
567 Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
568 }
569 assert( ppClass[0] != NULL );
570 Vec_PtrPush( p->vClasses, ppClass );
571 // iteratively refine this class
572 if ( fRefineNewClass )
573 nRefis += Fra_RefineClassLastIter( p, p->vClasses );
574 else if ( pSkipped )
575 (*pSkipped)++;
576 return nRefis;
577 }
578
579 /**Function*************************************************************
580
581 Synopsis [Starts representation of equivalence classes with one class.]
582
583 Description []
584
585 SideEffects []
586
587 SeeAlso []
588
589 ***********************************************************************/
Fra_ClassesTest(Fra_Cla_t * p,int Id1,int Id2)590 void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
591 {
592 Aig_Obj_t ** pClass;
593 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 );
594 pClass = p->pMemClasses;
595 assert( Id1 < Id2 );
596 pClass[0] = Aig_ManObj( p->pAig, Id1 );
597 pClass[1] = Aig_ManObj( p->pAig, Id2 );
598 pClass[2] = NULL;
599 pClass[3] = NULL;
600 Fra_ClassObjSetRepr( pClass[1], pClass[0] );
601 Vec_PtrPush( p->vClasses, pClass );
602 }
603
604 /**Function*************************************************************
605
606 Synopsis [Creates latch correspondence classes.]
607
608 Description []
609
610 SideEffects []
611
612 SeeAlso []
613
614 ***********************************************************************/
Fra_ClassesLatchCorr(Fra_Man_t * p)615 void Fra_ClassesLatchCorr( Fra_Man_t * p )
616 {
617 Aig_Obj_t * pObj;
618 int i, nEntries = 0;
619 Vec_PtrClear( p->pCla->vClasses1 );
620 Aig_ManForEachLoSeq( p->pManAig, pObj, i )
621 {
622 Vec_PtrPush( p->pCla->vClasses1, pObj );
623 Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
624 }
625 // allocate room for classes
626 p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
627 p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
628 }
629
630 /**Function*************************************************************
631
632 Synopsis [Postprocesses the classes by removing half of the less useful.]
633
634 Description []
635
636 SideEffects []
637
638 SeeAlso []
639
640 ***********************************************************************/
Fra_ClassesPostprocess(Fra_Cla_t * p)641 void Fra_ClassesPostprocess( Fra_Cla_t * p )
642 {
643 int Ratio = 2;
644 Fra_Sml_t * pComb;
645 Aig_Obj_t * pObj, * pRepr, ** ppClass;
646 int * pWeights, WeightMax = 0, i, k, c;
647 // perform combinational simulation
648 pComb = Fra_SmlSimulateComb( p->pAig, 32, 0 );
649 // compute the weight of each node in the classes
650 pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
651 memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
652 Aig_ManForEachObj( p->pAig, pObj, i )
653 {
654 pRepr = Fra_ClassObjRepr( pObj );
655 if ( pRepr == NULL )
656 continue;
657 pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
658 WeightMax = Abc_MaxInt( WeightMax, pWeights[i] );
659 }
660 Fra_SmlStop( pComb );
661 printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
662 // remove nodes from classes whose weight is less than WeightMax/Ratio
663 k = 0;
664 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
665 {
666 if ( pWeights[pObj->Id] >= WeightMax/Ratio )
667 Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
668 else
669 Fra_ClassObjSetRepr( pObj, NULL );
670 }
671 Vec_PtrShrink( p->vClasses1, k );
672 // in each class, compact the nodes
673 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
674 {
675 k = 1;
676 for ( c = 1; ppClass[c]; c++ )
677 {
678 if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
679 ppClass[k++] = ppClass[c];
680 else
681 Fra_ClassObjSetRepr( ppClass[c], NULL );
682 }
683 ppClass[k] = NULL;
684 }
685 // remove classes with only repr
686 k = 0;
687 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
688 if ( ppClass[1] != NULL )
689 Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
690 Vec_PtrShrink( p->vClasses, k );
691 printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
692 ABC_FREE( pWeights );
693 }
694
695 /**Function*************************************************************
696
697 Synopsis [Postprocesses the classes by selecting representative lowest in top order.]
698
699 Description []
700
701 SideEffects []
702
703 SeeAlso []
704
705 ***********************************************************************/
Fra_ClassesSelectRepr(Fra_Cla_t * p)706 void Fra_ClassesSelectRepr( Fra_Cla_t * p )
707 {
708 Aig_Obj_t ** pClass, * pNodeMin;
709 int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
710 // reassign representatives in each class
711 Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
712 {
713 // collect support sizes and find the min-support node
714 cMinSupp = -1;
715 pNodeMin = NULL;
716 nSuppSizeMin = ABC_INFINITY;
717 for ( c = 0; pClass[c]; c++ )
718 {
719 nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
720 // nSuppSizeCur = 1;
721 if ( nSuppSizeMin > nSuppSizeCur ||
722 (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
723 {
724 nSuppSizeMin = nSuppSizeCur;
725 pNodeMin = pClass[c];
726 cMinSupp = c;
727 }
728 }
729 // skip the case when the repr did not change
730 if ( cMinSupp == 0 )
731 continue;
732 // make the new node the representative of the class
733 pClass[cMinSupp] = pClass[0];
734 pClass[0] = pNodeMin;
735 // set the representative
736 for ( c = 0; pClass[c]; c++ )
737 Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
738 }
739 }
740
741
742
Fra_ObjEqu(Aig_Obj_t ** ppEquivs,Aig_Obj_t * pObj)743 static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return ppEquivs[pObj->Id]; }
Fra_ObjSetEqu(Aig_Obj_t ** ppEquivs,Aig_Obj_t * pObj,Aig_Obj_t * pNode)744 static inline void Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
745
Fra_ObjChild0Equ(Aig_Obj_t ** ppEquivs,Aig_Obj_t * pObj)746 static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)); }
Fra_ObjChild1Equ(Aig_Obj_t ** ppEquivs,Aig_Obj_t * pObj)747 static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)); }
748
749 /**Function*************************************************************
750
751 Synopsis [Add the node and its constraints to the new AIG.]
752
753 Description []
754
755 SideEffects []
756
757 SeeAlso []
758
759 ***********************************************************************/
Fra_ClassesDeriveNode(Aig_Man_t * pManFraig,Aig_Obj_t * pObj,Aig_Obj_t ** ppEquivs)760 static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
761 {
762 Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
763 // skip nodes without representative
764 if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
765 return;
766 assert( pObjRepr->Id < pObj->Id );
767 // get the new node
768 pObjNew = Fra_ObjEqu( ppEquivs, pObj );
769 // get the new node of the representative
770 pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
771 // if this is the same node, no need to add constraints
772 if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
773 return;
774 // these are different nodes - perform speculative reduction
775 // pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
776 // set the new node
777 // Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
778 // add the constraint
779 pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
780 pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
781 pMiter = Aig_Not( pMiter );
782 Aig_ObjCreateCo( pManFraig, pMiter );
783 }
784
785 /**Function*************************************************************
786
787 Synopsis [Derives AIG for the partitioned problem.]
788
789 Description []
790
791 SideEffects []
792
793 SeeAlso []
794
795 ***********************************************************************/
Fra_ClassesDeriveAig(Fra_Cla_t * p,int nFramesK)796 Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
797 {
798 Aig_Man_t * pManFraig;
799 Aig_Obj_t * pObj, * pObjNew;
800 Aig_Obj_t ** pLatches, ** ppEquivs;
801 int i, k, f, nFramesAll = nFramesK + 1;
802 assert( Aig_ManRegNum(p->pAig) > 0 );
803 assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
804 assert( nFramesK > 0 );
805 // start the fraig package
806 pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
807 pManFraig->pName = Abc_UtilStrsav( p->pAig->pName );
808 pManFraig->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
809 // allocate place for the node mapping
810 ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
811 Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
812 // create latches for the first frame
813 Aig_ManForEachLoSeq( p->pAig, pObj, i )
814 Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
815 // add timeframes
816 pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
817 for ( f = 0; f < nFramesAll; f++ )
818 {
819 // create PIs for this frame
820 Aig_ManForEachPiSeq( p->pAig, pObj, i )
821 Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
822 // set the constraints on the latch outputs
823 Aig_ManForEachLoSeq( p->pAig, pObj, i )
824 Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
825 // add internal nodes of this frame
826 Aig_ManForEachNode( p->pAig, pObj, i )
827 {
828 pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
829 Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
830 Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
831 }
832 if ( f == nFramesAll - 1 )
833 break;
834 if ( f == nFramesAll - 2 )
835 pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
836 // save the latch input values
837 k = 0;
838 Aig_ManForEachLiSeq( p->pAig, pObj, i )
839 pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
840 // insert them to the latch output values
841 k = 0;
842 Aig_ManForEachLoSeq( p->pAig, pObj, i )
843 Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
844 }
845 ABC_FREE( pLatches );
846 ABC_FREE( ppEquivs );
847 // mark the asserts
848 assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 );
849 printf( "Assert miters = %6d. Output miters = %6d.\n",
850 pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts );
851 // remove dangling nodes
852 Aig_ManCleanup( pManFraig );
853 return pManFraig;
854 }
855
856 ////////////////////////////////////////////////////////////////////////
857 /// END OF FILE ///
858 ////////////////////////////////////////////////////////////////////////
859
860
861 ABC_NAMESPACE_IMPL_END
862
863