1 /**CFile****************************************************************
2
3 FileName [sswClass.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [Representation of candidate equivalence classes.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswClass.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sswInt.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 topo order of their representatives.
33 */
34
35 // internal representation of candidate equivalence classes
36 struct Ssw_Cla_t_
37 {
38 // class information
39 Aig_Man_t * pAig; // original AIG manager
40 Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node
41 int * pClassSizes; // sizes of each equivalence class
42 int fConstCorr;
43 // statistics
44 int nClasses; // the total number of non-const classes
45 int nCands1; // the total number of const candidates
46 int nLits; // the number of literals in all classes
47 // memory
48 Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
49 Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
50 // temporary data
51 Vec_Ptr_t * vClassOld; // old equivalence class after splitting
52 Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
53 Vec_Ptr_t * vRefined; // the nodes refined since the last iteration
54 // procedures used for class refinement
55 void * pManData;
56 unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
57 int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant
58 int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
59 };
60
61 ////////////////////////////////////////////////////////////////////////
62 /// DECLARATIONS ///
63 ////////////////////////////////////////////////////////////////////////
64
Ssw_ObjNext(Aig_Obj_t ** ppNexts,Aig_Obj_t * pObj)65 static inline Aig_Obj_t * Ssw_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
Ssw_ObjSetNext(Aig_Obj_t ** ppNexts,Aig_Obj_t * pObj,Aig_Obj_t * pNext)66 static inline void Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
67
68 // iterator through the equivalence classes
69 #define Ssw_ManForEachClass( p, ppClass, i ) \
70 for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \
71 if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
72 // iterator through the nodes in one class
73 #define Ssw_ClassForEachNode( p, pRepr, pNode, i ) \
74 for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \
75 if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
76
77 ////////////////////////////////////////////////////////////////////////
78 /// FUNCTION DEFINITIONS ///
79 ////////////////////////////////////////////////////////////////////////
80
81 /**Function*************************************************************
82
83 Synopsis [Creates one equivalence class.]
84
85 Description []
86
87 SideEffects []
88
89 SeeAlso []
90
91 ***********************************************************************/
Ssw_ObjAddClass(Ssw_Cla_t * p,Aig_Obj_t * pRepr,Aig_Obj_t ** pClass,int nSize)92 static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
93 {
94 assert( p->pId2Class[pRepr->Id] == NULL );
95 assert( pClass[0] == pRepr );
96 p->pId2Class[pRepr->Id] = pClass;
97 assert( p->pClassSizes[pRepr->Id] == 0 );
98 assert( nSize > 1 );
99 p->pClassSizes[pRepr->Id] = nSize;
100 p->nClasses++;
101 p->nLits += nSize - 1;
102 }
103
104 /**Function*************************************************************
105
106 Synopsis [Removes one equivalence class.]
107
108 Description []
109
110 SideEffects []
111
112 SeeAlso []
113
114 ***********************************************************************/
Ssw_ObjRemoveClass(Ssw_Cla_t * p,Aig_Obj_t * pRepr)115 static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
116 {
117 Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
118 int nSize;
119 assert( pClass != NULL );
120 p->pId2Class[pRepr->Id] = NULL;
121 nSize = p->pClassSizes[pRepr->Id];
122 assert( nSize > 1 );
123 p->nClasses--;
124 p->nLits -= nSize - 1;
125 p->pClassSizes[pRepr->Id] = 0;
126 return pClass;
127 }
128
129 /**Function*************************************************************
130
131 Synopsis [Starts representation of equivalence classes.]
132
133 Description []
134
135 SideEffects []
136
137 SeeAlso []
138
139 ***********************************************************************/
Ssw_ClassesStart(Aig_Man_t * pAig)140 Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
141 {
142 Ssw_Cla_t * p;
143 p = ABC_ALLOC( Ssw_Cla_t, 1 );
144 memset( p, 0, sizeof(Ssw_Cla_t) );
145 p->pAig = pAig;
146 p->pId2Class = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
147 p->pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
148 p->vClassOld = Vec_PtrAlloc( 100 );
149 p->vClassNew = Vec_PtrAlloc( 100 );
150 p->vRefined = Vec_PtrAlloc( 1000 );
151 if ( pAig->pReprs == NULL )
152 Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
153 return p;
154 }
155
156 /**Function*************************************************************
157
158 Synopsis [Starts representation of equivalence classes.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ***********************************************************************/
Ssw_ClassesSetData(Ssw_Cla_t * p,void * pManData,unsigned (* pFuncNodeHash)(void *,Aig_Obj_t *),int (* pFuncNodeIsConst)(void *,Aig_Obj_t *),int (* pFuncNodesAreEqual)(void *,Aig_Obj_t *,Aig_Obj_t *))167 void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
168 unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node
169 int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant
170 int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
171 {
172 p->pManData = pManData;
173 p->pFuncNodeHash = pFuncNodeHash;
174 p->pFuncNodeIsConst = pFuncNodeIsConst;
175 p->pFuncNodesAreEqual = pFuncNodesAreEqual;
176 }
177
178 /**Function*************************************************************
179
180 Synopsis [Stop representation of equivalence classes.]
181
182 Description []
183
184 SideEffects []
185
186 SeeAlso []
187
188 ***********************************************************************/
Ssw_ClassesStop(Ssw_Cla_t * p)189 void Ssw_ClassesStop( Ssw_Cla_t * p )
190 {
191 if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
192 if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
193 Vec_PtrFree( p->vRefined );
194 ABC_FREE( p->pId2Class );
195 ABC_FREE( p->pClassSizes );
196 ABC_FREE( p->pMemClasses );
197 ABC_FREE( p );
198 }
199
200 /**Function*************************************************************
201
202 Synopsis [Stop representation of equivalence classes.]
203
204 Description []
205
206 SideEffects []
207
208 SeeAlso []
209
210 ***********************************************************************/
Ssw_ClassesReadAig(Ssw_Cla_t * p)211 Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p )
212 {
213 return p->pAig;
214 }
215
216 /**Function*************************************************************
217
218 Synopsis []
219
220 Description []
221
222 SideEffects []
223
224 SeeAlso []
225
226 ***********************************************************************/
Ssw_ClassesGetRefined(Ssw_Cla_t * p)227 Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
228 {
229 return p->vRefined;
230 }
231
232 /**Function*************************************************************
233
234 Synopsis []
235
236 Description []
237
238 SideEffects []
239
240 SeeAlso []
241
242 ***********************************************************************/
Ssw_ClassesClearRefined(Ssw_Cla_t * p)243 void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
244 {
245 Vec_PtrClear( p->vRefined );
246 }
247
248 /**Function*************************************************************
249
250 Synopsis [Stop representation of equivalence classes.]
251
252 Description []
253
254 SideEffects []
255
256 SeeAlso []
257
258 ***********************************************************************/
Ssw_ClassesCand1Num(Ssw_Cla_t * p)259 int Ssw_ClassesCand1Num( Ssw_Cla_t * p )
260 {
261 return p->nCands1;
262 }
263
264 /**Function*************************************************************
265
266 Synopsis [Stop representation of equivalence classes.]
267
268 Description []
269
270 SideEffects []
271
272 SeeAlso []
273
274 ***********************************************************************/
Ssw_ClassesClassNum(Ssw_Cla_t * p)275 int Ssw_ClassesClassNum( Ssw_Cla_t * p )
276 {
277 return p->nClasses;
278 }
279
280 /**Function*************************************************************
281
282 Synopsis [Stop representation of equivalence classes.]
283
284 Description []
285
286 SideEffects []
287
288 SeeAlso []
289
290 ***********************************************************************/
Ssw_ClassesLitNum(Ssw_Cla_t * p)291 int Ssw_ClassesLitNum( Ssw_Cla_t * p )
292 {
293 return p->nLits;
294 }
295
296 /**Function*************************************************************
297
298 Synopsis [Stop representation of equivalence classes.]
299
300 Description []
301
302 SideEffects []
303
304 SeeAlso []
305
306 ***********************************************************************/
Ssw_ClassesReadClass(Ssw_Cla_t * p,Aig_Obj_t * pRepr,int * pnSize)307 Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
308 {
309 if ( p->pId2Class[pRepr->Id] == NULL )
310 return NULL;
311 assert( p->pId2Class[pRepr->Id] != NULL );
312 assert( p->pClassSizes[pRepr->Id] > 1 );
313 *pnSize = p->pClassSizes[pRepr->Id];
314 return p->pId2Class[pRepr->Id];
315 }
316
317 /**Function*************************************************************
318
319 Synopsis [Stop representation of equivalence classes.]
320
321 Description []
322
323 SideEffects []
324
325 SeeAlso []
326
327 ***********************************************************************/
Ssw_ClassesCollectClass(Ssw_Cla_t * p,Aig_Obj_t * pRepr,Vec_Ptr_t * vClass)328 void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )
329 {
330 int i;
331 Vec_PtrClear( vClass );
332 if ( p->pId2Class[pRepr->Id] == NULL )
333 return;
334 assert( p->pClassSizes[pRepr->Id] > 1 );
335 for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
336 Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
337 }
338
339 /**Function*************************************************************
340
341 Synopsis [Checks candidate equivalence classes.]
342
343 Description []
344
345 SideEffects []
346
347 SeeAlso []
348
349 ***********************************************************************/
Ssw_ClassesCheck(Ssw_Cla_t * p)350 void Ssw_ClassesCheck( Ssw_Cla_t * p )
351 {
352 Aig_Obj_t * pObj, * pPrev, ** ppClass;
353 int i, k, nLits, nClasses, nCands1;
354 nClasses = nLits = 0;
355 Ssw_ManForEachClass( p, ppClass, k )
356 {
357 pPrev = NULL;
358 assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
359 Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
360 {
361 if ( i == 0 )
362 assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
363 else
364 {
365 assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
366 assert( pPrev->Id < pObj->Id );
367 nLits++;
368 }
369 pPrev = pObj;
370 }
371 nClasses++;
372 }
373 nCands1 = 0;
374 Aig_ManForEachObj( p->pAig, pObj, i )
375 nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
376 assert( p->nLits == nLits );
377 assert( p->nCands1 == nCands1 );
378 assert( p->nClasses == nClasses );
379 }
380
381 /**Function*************************************************************
382
383 Synopsis [Prints simulation classes.]
384
385 Description []
386
387 SideEffects []
388
389 SeeAlso []
390
391 ***********************************************************************/
Ssw_ClassesPrintOne(Ssw_Cla_t * p,Aig_Obj_t * pRepr)392 void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
393 {
394 Aig_Obj_t * pObj;
395 int i;
396 Abc_Print( 1, "{ " );
397 Ssw_ClassForEachNode( p, pRepr, pObj, i )
398 Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
399 Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
400 Abc_Print( 1, "}\n" );
401 }
402
403 /**Function*************************************************************
404
405 Synopsis [Prints simulation classes.]
406
407 Description []
408
409 SideEffects []
410
411 SeeAlso []
412
413 ***********************************************************************/
Ssw_ClassesPrint(Ssw_Cla_t * p,int fVeryVerbose)414 void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
415 {
416 Aig_Obj_t ** ppClass;
417 Aig_Obj_t * pObj;
418 int i;
419 Abc_Print( 1, "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
420 p->nCands1, p->nClasses, p->nCands1+p->nLits );
421 if ( !fVeryVerbose )
422 return;
423 Abc_Print( 1, "Constants { " );
424 Aig_ManForEachObj( p->pAig, pObj, i )
425 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
426 Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
427 Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
428 Abc_Print( 1, "}\n" );
429 Ssw_ManForEachClass( p, ppClass, i )
430 {
431 Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
432 Ssw_ClassesPrintOne( p, ppClass[0] );
433 }
434 Abc_Print( 1, "\n" );
435 }
436
437 /**Function*************************************************************
438
439 Synopsis [Prints simulation classes.]
440
441 Description []
442
443 SideEffects []
444
445 SeeAlso []
446
447 ***********************************************************************/
Ssw_ClassesRemoveNode(Ssw_Cla_t * p,Aig_Obj_t * pObj)448 void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
449 {
450 Aig_Obj_t * pRepr, * pTemp;
451 assert( p->pClassSizes[pObj->Id] == 0 );
452 assert( p->pId2Class[pObj->Id] == NULL );
453 pRepr = Aig_ObjRepr( p->pAig, pObj );
454 assert( pRepr != NULL );
455 // Vec_PtrPush( p->vRefined, pObj );
456 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
457 {
458 assert( p->pClassSizes[pRepr->Id] == 0 );
459 assert( p->pId2Class[pRepr->Id] == NULL );
460 Aig_ObjSetRepr( p->pAig, pObj, NULL );
461 p->nCands1--;
462 return;
463 }
464 // Vec_PtrPush( p->vRefined, pRepr );
465 Aig_ObjSetRepr( p->pAig, pObj, NULL );
466 assert( p->pId2Class[pRepr->Id][0] == pRepr );
467 assert( p->pClassSizes[pRepr->Id] >= 2 );
468 if ( p->pClassSizes[pRepr->Id] == 2 )
469 {
470 p->pId2Class[pRepr->Id] = NULL;
471 p->nClasses--;
472 p->pClassSizes[pRepr->Id] = 0;
473 p->nLits--;
474 }
475 else
476 {
477 int i, k = 0;
478 // remove the entry from the class
479 Ssw_ClassForEachNode( p, pRepr, pTemp, i )
480 if ( pTemp != pObj )
481 p->pId2Class[pRepr->Id][k++] = pTemp;
482 assert( k + 1 == p->pClassSizes[pRepr->Id] );
483 // reduce the class
484 p->pClassSizes[pRepr->Id]--;
485 p->nLits--;
486 }
487 }
488
489 /**Function*************************************************************
490
491 Synopsis [Takes the set of const1 cands and rehashes them using sim info.]
492
493 Description []
494
495 SideEffects []
496
497 SeeAlso []
498
499 ***********************************************************************/
Ssw_ClassesPrepareRehash(Ssw_Cla_t * p,Vec_Ptr_t * vCands,int fConstCorr)500 int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )
501 {
502 // Aig_Man_t * pAig = p->pAig;
503 Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
504 Aig_Obj_t * pObj, * pTemp, * pRepr;
505 int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
506
507 // allocate the hash table hashing simulation info into nodes
508 nTableSize = Abc_PrimeCudd( Vec_PtrSize(vCands)/2 );
509 ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
510 ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
511
512 // sort through the candidates
513 nEntries = 0;
514 p->nCands1 = 0;
515 Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
516 {
517 assert( p->pClassSizes[pObj->Id] == 0 );
518 Aig_ObjSetRepr( p->pAig, pObj, NULL );
519 // check if the node belongs to the class of constant 1
520 if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
521 {
522 Ssw_ObjSetConst1Cand( p->pAig, pObj );
523 p->nCands1++;
524 continue;
525 }
526 if ( fConstCorr )
527 continue;
528 // hash the node by its simulation info
529 iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
530 // add the node to the class
531 if ( ppTable[iEntry] == NULL )
532 {
533 ppTable[iEntry] = pObj;
534 }
535 else
536 {
537 // set the representative of this node
538 pRepr = ppTable[iEntry];
539 Aig_ObjSetRepr( p->pAig, pObj, pRepr );
540 // add node to the table
541 if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
542 { // this will be the second entry
543 p->pClassSizes[pRepr->Id]++;
544 nEntries++;
545 }
546 // add the entry to the list
547 Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
548 Ssw_ObjSetNext( ppNexts, pRepr, pObj );
549 p->pClassSizes[pRepr->Id]++;
550 nEntries++;
551 }
552 }
553
554 // copy the entries into storage in the topological order
555 nEntries2 = 0;
556 Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
557 {
558 nNodes = p->pClassSizes[pObj->Id];
559 // skip the nodes that are not representatives of non-trivial classes
560 if ( nNodes == 0 )
561 continue;
562 assert( nNodes > 1 );
563 // add the nodes to the class in the topological order
564 ppClassNew = p->pMemClassesFree + nEntries2;
565 ppClassNew[0] = pObj;
566 for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
567 pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
568 {
569 ppClassNew[nNodes-k] = pTemp;
570 }
571 // add the class of nodes
572 p->pClassSizes[pObj->Id] = 0;
573 Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
574 // increment the number of entries
575 nEntries2 += nNodes;
576 }
577 p->pMemClassesFree += nEntries2;
578 assert( nEntries == nEntries2 );
579 ABC_FREE( ppTable );
580 ABC_FREE( ppNexts );
581 // now it is time to refine the classes
582 return Ssw_ClassesRefine( p, 1 );
583 }
584
585 /**Function*************************************************************
586
587 Synopsis [Creates initial simulation classes.]
588
589 Description [Assumes that simulation info is assigned.]
590
591 SideEffects []
592
593 SeeAlso []
594
595 ***********************************************************************/
Ssw_ClassesPrepare(Aig_Man_t * pAig,int nFramesK,int fLatchCorr,int fConstCorr,int fOutputCorr,int nMaxLevs,int fVerbose)596 Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
597 {
598 // int nFrames = 4;
599 // int nWords = 1;
600 // int nIters = 16;
601
602 // int nFrames = 32;
603 // int nWords = 4;
604 // int nIters = 0;
605
606 int nFrames = Abc_MaxInt( nFramesK, 4 );
607 int nWords = 2;
608 int nIters = 16;
609 Ssw_Cla_t * p;
610 Ssw_Sml_t * pSml;
611 Vec_Ptr_t * vCands;
612 Aig_Obj_t * pObj;
613 int i, k, RetValue;
614 abctime clk;
615
616 // start the classes
617 p = Ssw_ClassesStart( pAig );
618 p->fConstCorr = fConstCorr;
619
620 // perform sequential simulation
621 clk = Abc_Clock();
622 pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
623 if ( fVerbose )
624 {
625 Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
626 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
627 Abc_Print( 1, "Initial simulation of %d frames with %d words. ", nFrames, nWords );
628 ABC_PRT( "Time", Abc_Clock() - clk );
629 }
630
631 // set comparison procedures
632 clk = Abc_Clock();
633 Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
634
635 // collect nodes to be considered as candidates
636 vCands = Vec_PtrAlloc( 1000 );
637 Aig_ManForEachObj( p->pAig, pObj, i )
638 {
639 if ( fLatchCorr )
640 {
641 if ( !Saig_ObjIsLo(p->pAig, pObj) )
642 continue;
643 }
644 else
645 {
646 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
647 continue;
648 // skip the node with more that the given number of levels
649 if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
650 continue;
651 }
652 Vec_PtrPush( vCands, pObj );
653 }
654
655 // this change will consider all PO drivers
656 if ( fOutputCorr )
657 {
658 Vec_PtrClear( vCands );
659 Aig_ManForEachObj( p->pAig, pObj, i )
660 pObj->fMarkB = 0;
661 Saig_ManForEachPo( p->pAig, pObj, i )
662 if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
663 Aig_ObjFanin0(pObj)->fMarkB = 1;
664 Aig_ManForEachObj( p->pAig, pObj, i )
665 if ( pObj->fMarkB )
666 Vec_PtrPush( vCands, pObj );
667 Aig_ManForEachObj( p->pAig, pObj, i )
668 pObj->fMarkB = 0;
669 }
670
671 // allocate room for classes
672 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
673 p->pMemClassesFree = p->pMemClasses;
674
675 // now it is time to refine the classes
676 Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
677 if ( fVerbose )
678 {
679 Abc_Print( 1, "Collecting candidate equivalence classes. " );
680 ABC_PRT( "Time", Abc_Clock() - clk );
681 }
682
683 clk = Abc_Clock();
684 // perform iterative refinement using simulation
685 for ( i = 1; i < nIters; i++ )
686 {
687 // collect const1 candidates
688 Vec_PtrClear( vCands );
689 Aig_ManForEachObj( p->pAig, pObj, k )
690 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
691 Vec_PtrPush( vCands, pObj );
692 assert( Vec_PtrSize(vCands) == p->nCands1 );
693 // perform new round of simulation
694 Ssw_SmlResimulateSeq( pSml );
695 // check equivalence classes
696 RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
697 if ( RetValue == 0 )
698 break;
699 }
700 Ssw_SmlStop( pSml );
701 Vec_PtrFree( vCands );
702 if ( fVerbose )
703 {
704 Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
705 nFrames, nWords, i-1 );
706 ABC_PRT( "Time", Abc_Clock() - clk );
707 }
708 Ssw_ClassesCheck( p );
709 // Ssw_ClassesPrint( p, 0 );
710 return p;
711 }
712
713 /**Function*************************************************************
714
715 Synopsis [Creates initial simulation classes.]
716
717 Description [Assumes that simulation info is assigned.]
718
719 SideEffects []
720
721 SeeAlso []
722
723 ***********************************************************************/
Ssw_ClassesPrepareSimple(Aig_Man_t * pAig,int fLatchCorr,int nMaxLevs)724 Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
725 {
726 Ssw_Cla_t * p;
727 Aig_Obj_t * pObj;
728 int i;
729 // start the classes
730 p = Ssw_ClassesStart( pAig );
731 // go through the nodes
732 p->nCands1 = 0;
733 Aig_ManForEachObj( pAig, pObj, i )
734 {
735 if ( fLatchCorr )
736 {
737 if ( !Saig_ObjIsLo(pAig, pObj) )
738 continue;
739 }
740 else
741 {
742 if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
743 continue;
744 // skip the node with more that the given number of levels
745 if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
746 continue;
747 }
748 Ssw_ObjSetConst1Cand( pAig, pObj );
749 p->nCands1++;
750 }
751 // allocate room for classes
752 p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
753 // Ssw_ClassesPrint( p, 0 );
754 return p;
755 }
756
757 /**Function*************************************************************
758
759 Synopsis [Creates initial simulation classes.]
760
761 Description [Assumes that simulation info is assigned.]
762
763 SideEffects []
764
765 SeeAlso []
766
767 ***********************************************************************/
Ssw_ClassesPrepareFromReprs(Aig_Man_t * pAig)768 Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig )
769 {
770 Ssw_Cla_t * p;
771 Aig_Obj_t * pObj, * pRepr;
772 int * pClassSizes, nEntries, i;
773 // start the classes
774 p = Ssw_ClassesStart( pAig );
775 // allocate memory for classes
776 p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
777 // count classes
778 p->nCands1 = 0;
779 Aig_ManForEachObj( pAig, pObj, i )
780 {
781 if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
782 {
783 p->nCands1++;
784 continue;
785 }
786 if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
787 {
788 if ( p->pClassSizes[pRepr->Id]++ == 0 )
789 p->pClassSizes[pRepr->Id]++;
790 }
791 }
792 // add nodes
793 nEntries = 0;
794 p->nClasses = 0;
795 pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
796 Aig_ManForEachObj( pAig, pObj, i )
797 {
798 if ( p->pClassSizes[i] )
799 {
800 p->pId2Class[i] = p->pMemClasses + nEntries;
801 nEntries += p->pClassSizes[i];
802 p->pId2Class[i][pClassSizes[i]++] = pObj;
803 p->nClasses++;
804 continue;
805 }
806 if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
807 continue;
808 if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
809 p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
810 }
811 p->pMemClassesFree = p->pMemClasses + nEntries;
812 p->nLits = nEntries - p->nClasses;
813 assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
814 ABC_FREE( pClassSizes );
815 // Abc_Print( 1, "After converting:\n" );
816 // Ssw_ClassesPrint( p, 0 );
817 return p;
818 }
819
820 /**Function*************************************************************
821
822 Synopsis [Creates initial simulation classes.]
823
824 Description [Assumes that simulation info is assigned.]
825
826 SideEffects []
827
828 SeeAlso []
829
830 ***********************************************************************/
Ssw_ClassesPrepareTargets(Aig_Man_t * pAig)831 Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig )
832 {
833 Ssw_Cla_t * p;
834 Aig_Obj_t * pObj;
835 int i;
836 // start the classes
837 p = Ssw_ClassesStart( pAig );
838 // go through the nodes
839 p->nCands1 = 0;
840 Saig_ManForEachPo( pAig, pObj, i )
841 {
842 Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
843 p->nCands1++;
844 }
845 // allocate room for classes
846 p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
847 // Ssw_ClassesPrint( p, 0 );
848 return p;
849 }
850
851 /**Function*************************************************************
852
853 Synopsis [Creates classes from the temporary representation.]
854
855 Description []
856
857 SideEffects []
858
859 SeeAlso []
860
861 ***********************************************************************/
Ssw_ClassesPreparePairs(Aig_Man_t * pAig,Vec_Int_t ** pvClasses)862 Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
863 {
864 Ssw_Cla_t * p;
865 Aig_Obj_t ** ppClassNew;
866 Aig_Obj_t * pObj, * pRepr, * pPrev;
867 int i, k, nTotalObjs, nEntries, Entry;
868 // start the classes
869 p = Ssw_ClassesStart( pAig );
870 // count the number of entries in the classes
871 nTotalObjs = 0;
872 for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
873 nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
874 // allocate memory for classes
875 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
876 // create constant-1 class
877 if ( pvClasses[0] )
878 Vec_IntForEachEntry( pvClasses[0], Entry, i )
879 {
880 assert( (i == 0) == (Entry == 0) );
881 if ( i == 0 )
882 continue;
883 pObj = Aig_ManObj( pAig, Entry );
884 Ssw_ObjSetConst1Cand( pAig, pObj );
885 p->nCands1++;
886 }
887 // create classes
888 nEntries = 0;
889 for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ )
890 {
891 if ( pvClasses[i] == NULL )
892 continue;
893 // get room for storing the class
894 ppClassNew = p->pMemClasses + nEntries;
895 nEntries += Vec_IntSize( pvClasses[i] );
896 // store the nodes of the class
897 pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) );
898 ppClassNew[0] = pRepr;
899 Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 )
900 {
901 pObj = Aig_ManObj( pAig, Entry );
902 assert( pPrev->Id < pObj->Id );
903 pPrev = pObj;
904 ppClassNew[k] = pObj;
905 Aig_ObjSetRepr( pAig, pObj, pRepr );
906 }
907 // create new class
908 Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) );
909 }
910 // prepare room for new classes
911 p->pMemClassesFree = p->pMemClasses + nEntries;
912 Ssw_ClassesCheck( p );
913 // Ssw_ClassesPrint( p, 0 );
914 return p;
915 }
916
917 /**Function*************************************************************
918
919 Synopsis [Creates classes from the temporary representation.]
920
921 Description []
922
923 SideEffects []
924
925 SeeAlso []
926
927 ***********************************************************************/
Ssw_ClassesPreparePairsSimple(Aig_Man_t * pMiter,Vec_Int_t * vPairs)928 Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
929 {
930 Ssw_Cla_t * p;
931 Aig_Obj_t ** ppClassNew;
932 Aig_Obj_t * pObj, * pRepr;
933 int i;
934 // start the classes
935 p = Ssw_ClassesStart( pMiter );
936 // allocate memory for classes
937 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
938 // create classes
939 for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
940 {
941 pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
942 pObj = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
943 assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
944 Aig_ObjSetRepr( pMiter, pObj, pRepr );
945 // get room for storing the class
946 ppClassNew = p->pMemClasses + i;
947 ppClassNew[0] = pRepr;
948 ppClassNew[1] = pObj;
949 // create new class
950 Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
951 }
952 // prepare room for new classes
953 p->pMemClassesFree = NULL;
954 Ssw_ClassesCheck( p );
955 // Ssw_ClassesPrint( p, 0 );
956 return p;
957 }
958
959 /**Function*************************************************************
960
961 Synopsis [Iteratively refines the classes after simulation.]
962
963 Description [Returns the number of refinements performed.]
964
965 SideEffects []
966
967 SeeAlso []
968
969 ***********************************************************************/
Ssw_ClassesRefineOneClass(Ssw_Cla_t * p,Aig_Obj_t * pReprOld,int fRecursive)970 int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
971 {
972 Aig_Obj_t ** pClassOld, ** pClassNew;
973 Aig_Obj_t * pObj, * pReprNew;
974 int i;
975
976 // split the class
977 Vec_PtrClear( p->vClassOld );
978 Vec_PtrClear( p->vClassNew );
979 Ssw_ClassForEachNode( p, pReprOld, pObj, i )
980 if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
981 Vec_PtrPush( p->vClassOld, pObj );
982 else
983 Vec_PtrPush( p->vClassNew, pObj );
984 // check if splitting happened
985 if ( Vec_PtrSize(p->vClassNew) == 0 )
986 return 0;
987 // remember that this class is refined
988 // Ssw_ClassForEachNode( p, pReprOld, pObj, i )
989 // Vec_PtrPush( p->vRefined, pObj );
990
991 // get the new representative
992 pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
993 assert( Vec_PtrSize(p->vClassOld) > 0 );
994 assert( Vec_PtrSize(p->vClassNew) > 0 );
995
996 // create old class
997 pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
998 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
999 {
1000 pClassOld[i] = pObj;
1001 Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
1002 }
1003 // create new class
1004 pClassNew = pClassOld + i;
1005 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1006 {
1007 pClassNew[i] = pObj;
1008 Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1009 }
1010
1011 // put classes back
1012 if ( Vec_PtrSize(p->vClassOld) > 1 )
1013 Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
1014 if ( Vec_PtrSize(p->vClassNew) > 1 )
1015 Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
1016
1017 // check if the class should be recursively refined
1018 if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
1019 return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1020 return 1;
1021 }
1022
1023 /**Function*************************************************************
1024
1025 Synopsis [Refines the classes after simulation.]
1026
1027 Description []
1028
1029 SideEffects []
1030
1031 SeeAlso []
1032
1033 ***********************************************************************/
Ssw_ClassesRefine(Ssw_Cla_t * p,int fRecursive)1034 int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive )
1035 {
1036 Aig_Obj_t ** ppClass;
1037 int i, nRefis = 0;
1038 Ssw_ManForEachClass( p, ppClass, i )
1039 nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive );
1040 return nRefis;
1041 }
1042
1043 /**Function*************************************************************
1044
1045 Synopsis [Refines the classes after simulation.]
1046
1047 Description []
1048
1049 SideEffects []
1050
1051 SeeAlso []
1052
1053 ***********************************************************************/
Ssw_ClassesRefineGroup(Ssw_Cla_t * p,Vec_Ptr_t * vReprs,int fRecursive)1054 int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )
1055 {
1056 Aig_Obj_t * pObj;
1057 int i, nRefis = 0;
1058 Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
1059 nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
1060 return nRefis;
1061 }
1062
1063 /**Function*************************************************************
1064
1065 Synopsis [Refine the group of constant 1 nodes.]
1066
1067 Description []
1068
1069 SideEffects []
1070
1071 SeeAlso []
1072
1073 ***********************************************************************/
Ssw_ClassesRefineConst1Group(Ssw_Cla_t * p,Vec_Ptr_t * vRoots,int fRecursive)1074 int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
1075 {
1076 Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
1077 int i;
1078 if ( Vec_PtrSize(vRoots) == 0 )
1079 return 0;
1080 // collect the nodes to be refined
1081 Vec_PtrClear( p->vClassNew );
1082 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
1083 if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
1084 Vec_PtrPush( p->vClassNew, pObj );
1085 // check if there is a new class
1086 if ( Vec_PtrSize(p->vClassNew) == 0 )
1087 return 0;
1088 p->nCands1 -= Vec_PtrSize(p->vClassNew);
1089 pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
1090 Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
1091 if ( Vec_PtrSize(p->vClassNew) == 1 )
1092 return 1;
1093 // create a new class composed of these nodes
1094 ppClassNew = p->pMemClassesFree;
1095 p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1096 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1097 {
1098 ppClassNew[i] = pObj;
1099 Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1100 }
1101 Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
1102 // refine them recursively
1103 if ( fRecursive )
1104 return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1105 return 1;
1106 }
1107
1108 /**Function*************************************************************
1109
1110 Synopsis [Refine the group of constant 1 nodes.]
1111
1112 Description []
1113
1114 SideEffects []
1115
1116 SeeAlso []
1117
1118 ***********************************************************************/
Ssw_ClassesRefineConst1(Ssw_Cla_t * p,int fRecursive)1119 int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
1120 {
1121 Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
1122 int i;
1123 // collect the nodes to be refined
1124 Vec_PtrClear( p->vClassNew );
1125 for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
1126 if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
1127 {
1128 pObj = Aig_ManObj( p->pAig, i );
1129 if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
1130 {
1131 Vec_PtrPush( p->vClassNew, pObj );
1132 // Vec_PtrPush( p->vRefined, pObj );
1133 }
1134 }
1135 // check if there is a new class
1136 if ( Vec_PtrSize(p->vClassNew) == 0 )
1137 return 0;
1138 if ( p->fConstCorr )
1139 {
1140 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1141 Aig_ObjSetRepr( p->pAig, pObj, NULL );
1142 return 1;
1143 }
1144 p->nCands1 -= Vec_PtrSize(p->vClassNew);
1145 pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
1146 Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
1147 if ( Vec_PtrSize(p->vClassNew) == 1 )
1148 return 1;
1149 // create a new class composed of these nodes
1150 ppClassNew = p->pMemClassesFree;
1151 p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1152 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1153 {
1154 ppClassNew[i] = pObj;
1155 Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1156 }
1157 Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
1158 // refine them recursively
1159 if ( fRecursive )
1160 return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1161 return 1;
1162 }
1163
1164
1165 ////////////////////////////////////////////////////////////////////////
1166 /// END OF FILE ///
1167 ////////////////////////////////////////////////////////////////////////
1168
1169
1170 ABC_NAMESPACE_IMPL_END
1171