Version abc81029

1 files changed, 104 insertions, 70 deletions

diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 3dfee28b..771fd530 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -482,75 +482,34 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates initial simulation classes.]
+  Synopsis    [Takes the set of const1 cands and rehashes them using sim info.]
 
-  Description [Assumes that simulation info is assigned.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
+int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
 {
-//    int nFrames =  4;
-//    int nWords  =  1;
-//    int nIters  = 16;
-
-//    int nFrames = 32;
-//    int nWords  =  4;
-//    int nIters  =  0;
-
-    int nFrames =  4;
-    int nWords  =  2;
-    int nIters  = 16;
-    Ssw_Cla_t * p;
-    Ssw_Sml_t * pSml;
+    Aig_Man_t * pAig = p->pAig;
     Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
     Aig_Obj_t * pObj, * pTemp, * pRepr;
-    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2, RetValue;
-    int clk;
-
-    // start the classes
-    p = Ssw_ClassesStart( pAig );
-
-    // perform sequential simulation
-clk = clock();
-    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
-if ( fVerbose )
-{
-    printf( "Allocated %.2f Mb for simulation information.\n", 
-        1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
-    printf( "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
-    PRT( "Time", clock() - clk );
-}
-
-    // set comparison procedures
-clk = clock();
-    Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
 
     // allocate the hash table hashing simulation info into nodes
-    nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
+    nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 );
     ppTable = CALLOC( Aig_Obj_t *, nTableSize ); 
     ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
 
-    // add all the nodes to the hash table
+    // sort through the candidates
     nEntries = 0;
-    Aig_ManForEachObj( p->pAig, pObj, i )
+    p->nCands1 = 0;
+    Vec_PtrForEachEntry( vCands, pObj, i )
     {
-        if ( fLatchCorr )
-        {
-            if ( !Saig_ObjIsLo(p->pAig, pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-            // skip the node with more that the given number of levels
-            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
-                continue;
-        }
+        assert( p->pClassSizes[pObj->Id] == 0 );
+        Aig_ObjSetRepr( p->pAig, pObj, NULL );
         // check if the node belongs to the class of constant 1
         if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
         {
@@ -562,7 +521,9 @@ clk = clock();
         iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
         // add the node to the class
         if ( ppTable[iEntry] == NULL )
+        {
             ppTable[iEntry] = pObj;
+        }
         else
         {
             // set the representative of this node
@@ -581,24 +542,18 @@ clk = clock();
             nEntries++;
         }
     }
-
-    // allocate room for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
-    p->pMemClassesFree = p->pMemClasses + nEntries;
  
     // copy the entries into storage in the topological order
     nEntries2 = 0;
-    Aig_ManForEachObj( p->pAig, pObj, i )
+    Vec_PtrForEachEntry( vCands, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-            continue;
         nNodes = p->pClassSizes[pObj->Id];
         // skip the nodes that are not representatives of non-trivial classes
         if ( nNodes == 0 )
             continue;
         assert( nNodes > 1 );
         // add the nodes to the class in the topological order
-        ppClassNew = p->pMemClasses + nEntries2;
+        ppClassNew = p->pMemClassesFree + nEntries2;
         ppClassNew[0] = pObj;
         for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp; 
               pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
@@ -611,12 +566,88 @@ clk = clock();
         // increment the number of entries
         nEntries2 += nNodes;
     }
+    p->pMemClassesFree += nEntries2;
     assert( nEntries == nEntries2 );
     free( ppTable );
     free( ppNexts );
+    // now it is time to refine the classes
+    return Ssw_ClassesRefine( p, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
+{
+//    int nFrames =  4;
+//    int nWords  =  1;
+//    int nIters  = 16;
+
+//    int nFrames = 32;
+//    int nWords  =  4;
+//    int nIters  =  0;
+
+    int nFrames =  4;
+    int nWords  =  2;
+    int nIters  = 16;
+    Ssw_Cla_t * p;
+    Ssw_Sml_t * pSml;
+    Vec_Ptr_t * vCands;
+    Aig_Obj_t * pObj;
+    int i, k, RetValue, clk;
+
+    // start the classes
+    p = Ssw_ClassesStart( pAig );
+
+    // perform sequential simulation
+clk = clock();
+    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
+if ( fVerbose )
+{
+    printf( "Allocated %.2f Mb to store simulation information.\n", 
+        1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
+    printf( "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
+    PRT( "Time", clock() - clk );
+}
+
+    // set comparison procedures
+clk = clock();
+    Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+
+    // collect nodes to be considered as candidates
+    vCands = Vec_PtrAlloc( 1000 );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( fLatchCorr )
+        {
+            if ( !Saig_ObjIsLo(p->pAig, pObj) )
+                continue;
+        }
+        else
+        {
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+                continue;
+            // skip the node with more that the given number of levels
+            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
+                continue;
+        }
+        Vec_PtrPush( vCands, pObj );
+    }
+
+    // allocate room for classes
+    p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
+    p->pMemClassesFree = p->pMemClasses;
 
     // now it is time to refine the classes
-    Ssw_ClassesRefine( p, 1 );
+    Ssw_ClassesPrepareRehash( p, vCands );
 if ( fVerbose )
 {
     printf( "Collecting candidate equivalence classes.        " );
@@ -625,27 +656,30 @@ PRT( "Time", clock() - clk );
 
 clk = clock();
     // perform iterative refinement using simulation
-    k = 0;
     for ( i = 1; i < nIters; i++ )
     {
+        // collect const1 candidates
+        Vec_PtrClear( vCands );
+        Aig_ManForEachObj( p->pAig, pObj, k )
+            if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
+                Vec_PtrPush( vCands, pObj );
+        assert( Vec_PtrSize(vCands) == p->nCands1 );
+        // perform new round of simulation
         Ssw_SmlResimulateSeq( pSml );
-        // simulate internal nodes
-        Ssw_SmlSimulateOne( pSml );
         // check equivalence classes
-        RetValue = Ssw_ClassesRefineConst1( p, 1 );
-        RetValue += Ssw_ClassesRefine( p, 1 );
-        k++;
+        RetValue = Ssw_ClassesPrepareRehash( p, vCands );
         if ( RetValue == 0 )
             break;
     }
-    Ssw_ClassesCheck( p );
     Ssw_SmlStop( pSml );
+    Vec_PtrFree( vCands );
 if ( fVerbose )
 {
     printf( "Simulation of %d frames with %d words (%2d rounds). ", 
-        nFrames, nWords, k );
+        nFrames, nWords, i-1 );
     PRT( "Time", clock() - clk );
 }
+    Ssw_ClassesCheck( p );
 //    Ssw_ClassesPrint( p, 0 );
     return p;
 }
@@ -848,7 +882,7 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
 {
     Aig_Obj_t ** pClassOld, ** pClassNew;
     Aig_Obj_t * pObj, * pReprNew;
-    int i;
+    int i; 
 
     // split the class
     Vec_PtrClear( p->vClassOld );