diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-01 02:19:19 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-01 02:19:19 -0700 |
commit | d3c018cd23df0954be488e6a97c4a7ad7577658e (patch) | |
tree | 2f23e04cc69141a82980ffb6ed0e482a8dd6bd98 /src/aig/gia/giaFrames.c | |
parent | a4908534f1a166fd52ed2763da31856e39945e09 (diff) | |
download | abc-d3c018cd23df0954be488e6a97c4a7ad7577658e.tar.gz abc-d3c018cd23df0954be488e6a97c4a7ad7577658e.tar.bz2 abc-d3c018cd23df0954be488e6a97c4a7ad7577658e.zip |
Reducing memory usage in bmc2 and bmc3.
Diffstat (limited to 'src/aig/gia/giaFrames.c')
-rw-r--r-- | src/aig/gia/giaFrames.c | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index a14122ae..48a0568e 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -915,6 +915,66 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) return pFrames; } + +/**Function************************************************************* + + Synopsis [Perform init unrolling as long as PO(s) are constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbose ) +{ + Gia_Man_t * pFrames, * pTemp; + Gia_Obj_t * pObj; + int i, f; + assert( Gia_ManRegNum(pAig) > 0 ); + if ( nFrames > 0 ) + printf( "Computing specialized unrolling with %d frames...\n", nFrames ); + pFrames = Gia_ManStart( Gia_ManObjNum(pAig) ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + Gia_ManHashAlloc( pFrames ); + Gia_ManConst0(pAig)->Value = 0; + for ( f = 0; nFrames == 0 || f < nFrames; f++ ) + { + if ( fVerbose && (f % 100 == 0) ) + { + printf( "%6d : ", f ); + Gia_ManPrintStats( pFrames, 0, 0 ); + } + Gia_ManForEachRo( pAig, pObj, i ) + pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0; + Gia_ManForEachPi( pAig, pObj, i ) + pObj->Value = Gia_ManAppendCi( pFrames ); + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( pAig, pObj, i ) + if ( Gia_ObjFanin0Copy(pObj) != 0 ) + break; + if ( i < Gia_ManPoNum(pAig) ) + break; + Gia_ManForEachRi( pAig, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + } + if ( fVerbose ) + printf( "Computed prefix of %d frames.\n", f ); + Gia_ManForEachRi( pAig, pObj, i ) + Gia_ManAppendCo( pFrames, pObj->Value ); + Gia_ManHashStop( pFrames ); + pFrames = Gia_ManCleanup( pTemp = pFrames ); + if ( fVerbose ) + printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", + Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) ); + Gia_ManStop( pTemp ); + return pFrames; +} + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |