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