diff options
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaIf.c | 57 | ||||
-rw-r--r-- | src/aig/gia/giaSatLut.c | 10 | ||||
-rw-r--r-- | src/aig/gia/giaTim.c | 7 | ||||
-rw-r--r-- | src/base/abci/abc.c | 16 |
5 files changed, 82 insertions, 9 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 6a1dc99e..a3fe1dc5 100644 --- a/src/aig/gia/gia.h +++ b/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 ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index f5071929..e6e326e3 100644 --- a/src/aig/gia/giaIf.c +++ b/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 /// diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index 55a9e303..d8921bca 100644 --- a/src/aig/gia/giaSatLut.c +++ b/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 ); diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 98f0ee44..c065ab5a 100644 --- a/src/aig/gia/giaTim.c +++ b/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) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 34e1a177..22df8109 100644 --- a/src/base/abci/abc.c +++ b/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; } |