diff options
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 29 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 6 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 48 | ||||
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 1 |
5 files changed, 71 insertions, 16 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 8a468feb..099c693b 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -237,6 +237,7 @@ struct Gia_ParVta_t_ int fVerbose; // verbose flag int fVeryVerbose; // print additional information int iFrame; // the number of frames covered + int iFrameProved; // the number of frames proved int nFramesNoChange; // the number of last frames without changes }; @@ -726,6 +727,8 @@ extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ); extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ); extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); +extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ); +extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); /*=== giaAbsGla.c ===========================================================*/ extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta ); extern int Ga2_ManPerform( Gia_Man_t * p, Gia_ParVta_t * pPars ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 59b5ddfe..c5acfa2a 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -707,6 +707,35 @@ void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose ) ABC_FREE( pCounts ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ) +{ + Gia_Obj_t * pObj; + int i, Count = 0; + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) + Count++; + return Count; +} +int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ) +{ + Gia_Obj_t * pObj; + int i, Count = 0; + Gia_ManForEachAnd( p, pObj, i ) + if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) + Count++; + return Count; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 65296d22..57122da5 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1537,20 +1537,17 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl } void Gla_ManReportMemory( Gla_Man_t * p ) { + extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ); Gla_Obj_t * pGla; -// int i; double memTot = 0; double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); double memSat = sat_solver2_memory( p->pSat, 1 ); double memPro = sat_solver2_memory_proof( p->pSat ); double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int); -// double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t); double memRef = Rnm_ManMemoryUsage( p->pRnm ); double memOth = sizeof(Gla_Man_t); for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ ) memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int); -// for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) -// memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int); memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); memOth += Vec_IntCap(p->vTemp) * sizeof(int); memOth += Vec_IntCap(p->vAbs) * sizeof(int); @@ -1562,6 +1559,7 @@ void Gla_ManReportMemory( Gla_Man_t * p ) ABC_PRMP( "Memory: Refine ", memRef, memTot ); ABC_PRMP( "Memory: Other ", memOth, memTot ); ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); + Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrame, 1 ); } diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 316dcec8..18e63fa0 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -408,6 +408,29 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->pTable = ABC_CALLOC( int, 6 * p->nTable ); return p; } + +void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ) +{ + FILE * pFile; + char pFileName[32]; + sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" ); + + pFile = fopen( pFileName, "wb+" ); + + fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d", + pGia->pName, + Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia), + (int)(1 + sat_solver2_memory_proof(pSat)/(1<<20)), + iFrame ); + + if ( pGia->vGateClasses ) + fprintf( pFile, " ff=%d and=%d", + Gia_GlaCountFlops( pGia, pGia->vGateClasses ), + Gia_GlaCountNodes( pGia, pGia->vGateClasses ) ); + + fprintf( pFile, "\n" ); + fclose( pFile ); +} void Ga2_ManReportMemory( Ga2_Man_t * p ) { double memTot = 0; @@ -435,6 +458,7 @@ void Ga2_ManReportMemory( Ga2_Man_t * p ) ABC_PRMP( "Memory: Hash ", memHash,memTot ); ABC_PRMP( "Memory: Other ", memOth, memTot ); ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); + Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 ); } void Ga2_ManStop( Ga2_Man_t * p ) { @@ -1477,7 +1501,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Vec_Int_t * vCore, * vPPis; clock_t clk2, clk = clock(); int Status = l_Undef, RetValue = -1, fOneIsSent = 0; - int i, c, f, Lit, iFrameProved = -1; + int i, c, f, Lit; // check trivial case assert( Gia_ManPoNum(pAig) == 1 ); ABC_FREE( pAig->pCexSeq ); @@ -1543,7 +1567,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // add static clauses to this timeframe Ga2_ManAddAbsClauses( p, f ); // skip checking if skipcheck is enabled (&gla -s) - if ( p->pPars->fUseSkip && f <= iFrameProved ) + if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved ) continue; // skip checking if we need to skip several starting frames (&gla -S <num>) if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart ) @@ -1632,11 +1656,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) goto finish; if ( c == 0 ) { - if ( f > iFrameProved ) + if ( f > p->pPars->iFrameProved ) p->pPars->nFramesNoChange++; break; } - if ( f > iFrameProved ) + if ( f > p->pPars->iFrameProved ) p->pPars->nFramesNoChange = 0; // derive the core @@ -1695,8 +1719,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) break; } // remember the last proved frame - if ( iFrameProved < f ) - iFrameProved = f; + if ( p->pPars->iFrameProved < f ) + p->pPars->iFrameProved = f; // print statistics if ( pPars->fVerbose ) Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); @@ -1761,18 +1785,18 @@ finish: if ( p->pPars->fVerbose ) Abc_Print( 1, "\n" ); if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) - Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, iFrameProved+1, p->pPars->nFramesNoChange ); + Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) - Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, iFrameProved+1, p->pPars->nFramesNoChange ); + Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 ) - Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, iFrameProved+1 ); + Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, p->pPars->iFrameProved+1 ); else - Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", iFrameProved+1 ); + Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", p->pPars->iFrameProved+1 ); } else { - p->pPars->iFrame = iFrameProved; - Abc_Print( 1, "GLA completed %d frames and produced a %d-stable abstraction. ", iFrameProved+1, p->pPars->nFramesNoChange ); + p->pPars->iFrame = p->pPars->iFrameProved; + Abc_Print( 1, "GLA completed %d frames and produced a %d-stable abstraction. ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); } } else diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 878903b1..b5115947 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -164,6 +164,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) p->fPropFanout = 1; // propagate fanouts during refinement p->fVerbose = 0; // verbose flag p->iFrame = -1; // the number of frames covered + p->iFrameProved = -1; // the number of frames proved } /**Function************************************************************* |