Adding AIG rehashing after LUT mapping in Gia.

src/aig/gia/gia.h

@@ -1305,6 +1305,7 @@ extern void                Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGi
 extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
 extern Gia_Man_t *         Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
 extern Gia_Man_t *         Gia_ManPerformDsdBalance( Gia_Man_t * p, int nLutSize, int nCutNum, int nRelaxRatio, int fVerbose );
+extern Gia_Man_t *         Gia_ManDupHashMapping( Gia_Man_t * p );
 /*=== giaJf.c ===========================================================*/
 extern void                Jf_ManSetDefaultPars( Jf_Par_t * pPars );
 extern Gia_Man_t *         Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );

src/aig/gia/giaIf.c

@@ -2183,9 +2183,15 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     }
     else 
     {
-        // mapping
+        int fHashMapping = 1;
         pNew = Gia_ManPerformMappingInt( p, (If_Par_t *)pp );
         Gia_ManTransferTiming( pNew, p );
+        if ( fHashMapping )
+        {
+            pNew = Gia_ManDupHashMapping( p = pNew );
+            Gia_ManTransferTiming( pNew, p );
+            Gia_ManStop( p );
+        }
     }
     pNew->MappedDelay = (int)((If_Par_t *)pp)->FinalDelay;
     pNew->MappedArea  = (int)((If_Par_t *)pp)->FinalArea;
@@ -2313,6 +2319,55 @@ void Gia_ManTestStruct( Gia_Man_t * p )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs hashing for a mapped AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupHashMapping( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew; 
+    Vec_Int_t * vMapping; 
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k;
+    assert( Gia_ManHasMapping(p) );
+    // copy the old manager with hashing
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // recreate mapping
+    vMapping = Vec_IntAlloc( Vec_IntSize(p->vMapping) );
+    Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
+    Gia_ManForEachLut( p, i )
+    {
+        pObj = Gia_ManObj( p, i );
+        Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pObj->Value), Vec_IntSize(vMapping) );
+        Vec_IntPush( vMapping, Gia_ObjLutSize(p, i) );
+        Gia_LutForEachFaninObj( p, i, pFanin, k )
+            Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->Value)  );
+        Vec_IntPush( vMapping, Abc_Lit2Var(pObj->Value) );
+    }
+    pNew->vMapping = vMapping;
+    return pNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/aig/gia/giaSatLut.c

@@ -46,6 +46,7 @@ struct Sbl_Man_t_
     int            nRuns;        // the number of runs
     int            nSmallWins;   // the number of small windows
     int            nLargeWins;   // the number of large windows
+    int            nIterOuts;    // the number of iters exceeded
     // parameters
     int            nBTLimit;     // conflicts
     int            DelayMax;     // external delay
@@ -1109,9 +1110,10 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
                 printf( "LitCount = %d.\n", LitCount );
             printf( "\n" );
         }
-        if ( nIters == 20 )
+        if ( nIters == 10 )
         {
-            printf( "Obj %d : Quitting after %d iterations.\n", iPivot, nIters );
+            p->nIterOuts++;
+            //printf( "Obj %d : Quitting after %d iterations.\n", iPivot, nIters );
             break;
         }
     }
@@ -1183,8 +1185,8 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit,
     }
     Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
     if ( p->fVerbose )
-    printf( "Tried = %d. Improved = %d.  Small win = %d. Large win = %d.  Total SAT runs = %d.\n", 
-        p->nTried, p->nImproved, p->nSmallWins, p->nLargeWins, p->nRuns );
+    printf( "Tried = %d. Improved = %d. SmallWin = %d. LargeWin = %d. IterOut = %d.  SAT runs = %d.\n", 
+        p->nTried, p->nImproved, p->nSmallWins, p->nLargeWins, p->nIterOuts, p->nRuns );
     if ( p->fVerbose )
     Sbl_ManPrintRuntime( p );
     Sbl_ManStop( p );

src/aig/gia/giaTim.c

@@ -137,6 +137,7 @@ int Gia_ManIsNormalized( Gia_Man_t * p )
 ***********************************************************************/
 Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
 {
+    int fHash = 1;
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int i;
@@ -170,11 +171,15 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
             Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
         printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
     }
+    if ( fHash ) Gia_ManHashAlloc( pNew );
     Gia_ManForEachAnd( p, pObj, i )
         if ( Gia_ObjIsBuf(pObj) )
             pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
-        else 
+        else if ( fHash )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    if ( fHash ) Gia_ManHashStop( pNew );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );

src/base/abci/abc.c

@@ -27641,8 +27641,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAddStrash = 0;
     int fCollapse = 0;
     int fAddMuxes = 0;
+    int fRehashMap = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Lacmh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Lacmrh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27666,6 +27667,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             fAddMuxes ^= 1;
             break;
+        case 'r':
+            fRehashMap ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -27677,7 +27681,12 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
         return 1;
     }
-    if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs )
+    if ( Gia_ManHasMapping(pAbc->pGia) && fRehashMap )
+    {
+        extern Gia_Man_t * Gia_ManDupHashMapping( Gia_Man_t * p );
+        pTemp = Gia_ManDupHashMapping( pAbc->pGia );
+    }
+    else if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs )
         pTemp = (Gia_Man_t *)If_ManDeriveGiaFromCells( pAbc->pGia );
     else if ( Gia_ManHasMapping(pAbc->pGia) )
         pTemp = (Gia_Man_t *)Dsm_ManDeriveGia( pAbc->pGia, fAddMuxes ); // delay-oriented unmapping
@@ -27730,12 +27739,13 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &st [-L num] [-acmh]\n" );
+    Abc_Print( -2, "usage: &st [-L num] [-acmrh]\n" );
     Abc_Print( -2, "\t         performs structural hashing\n" );
     Abc_Print( -2, "\t-a     : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
     Abc_Print( -2, "\t-L num : create MUX when sum of refs does not exceed this limit [default = %d]\n", Limit );
+    Abc_Print( -2, "\t-r     : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }