summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaIf.c57
-rw-r--r--src/aig/gia/giaSatLut.c10
-rw-r--r--src/aig/gia/giaTim.c7
-rw-r--r--src/base/abci/abc.c16
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-25 06:53:30 +0000