diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-26 14:38:38 -0800 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-26 14:38:38 -0800 |
commit | 27bdffd5a20d34acaffd08de87565922ba9cd5fc (patch) | |
tree | 56c414142ccfed98e7535adde42b04ba3f1429e1 /src/base/wlc/wlcAbs.c | |
parent | cba376cfff789b51a6267caf17f163a167c28b59 (diff) | |
download | abc-27bdffd5a20d34acaffd08de87565922ba9cd5fc.tar.gz abc-27bdffd5a20d34acaffd08de87565922ba9cd5fc.tar.bz2 abc-27bdffd5a20d34acaffd08de87565922ba9cd5fc.zip |
small tweaks
Diffstat (limited to 'src/base/wlc/wlcAbs.c')
-rw-r--r-- | src/base/wlc/wlcAbs.c | 69 |
1 files changed, 58 insertions, 11 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index a929f8c5..b02c3662 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -410,25 +410,51 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe Vec_IntFree( vCoreSels ); + if ( pPars->fVerbose ) + Abc_Print( 1, "Proof-based refinement reduces %d (out of %d) white boxes\n", Vec_IntSize( *pvRefine ) - Vec_IntSize( vRefine ), Vec_IntSize( *pvRefine ) ); + Vec_IntFree( *pvRefine ); *pvRefine = vRefine; return 0; } -/**Function************************************************************* +static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark ) +{ + int Entry, i; + Wlc_Obj_t * pObj; int Count[4] = {0}; + Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ); - Synopsis [Mark operators that meet the abstraction criteria.] + assert( *pvBlacks ); - Description [This procedure returns the array of objects (vLeaves) that - should be abstracted because of their high bit-width. It uses input array (vUnmark) - to not abstract those objects that have been refined in the previous rounds.] - - SideEffects [] + Vec_IntForEachEntry( *pvBlacks, Entry, i ) + { + if ( Vec_BitEntry( vUnmark, Entry) ) + continue; + Vec_IntPush( vBlacks, Entry ); - SeeAlso [] + pObj = Wlc_NtkObj( p, Entry ); + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) + Count[0]++; + else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) + Count[1]++; + else if ( pObj->Type == WLC_OBJ_MUX ) + Count[2]++; + else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) + Count[3]++; + } + + assert( Vec_IntSize( vBlacks ) ); + + Vec_IntFree( *pvBlacks ); + *pvBlacks = vBlacks; + + if ( pPars->fVerbose ) + printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); + + return 0; +} -***********************************************************************/ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) { Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; @@ -468,6 +494,20 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t return vBlacks; } +/**Function************************************************************* + + Synopsis [Mark operators that meet the abstraction criteria.] + + Description [This procedure returns the array of objects (vLeaves) that + should be abstracted because of their high bit-width. It uses input array (vUnmark) + to not abstract those objects that have been refined in the previous rounds.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); @@ -797,6 +837,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_Man_t * pPdr; Vec_Vec_t * vClauses = NULL; Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL; + Vec_Int_t * vBlacks = NULL; int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1; // start the bitmap to mark objects that cannot be abstracted because of refinement // currently, this bitmap is empty because abstraction begins without refinement @@ -831,8 +872,12 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // get abstracted GIA and the set of pseudo-PIs (vPisNew) if ( pPars->fProofRefine ) { - vPisNew = Wlc_NtkGetBlacks( p, pPars, vUnmark ); - pAbs = Wlc_NtkAbs2( p, vPisNew, &vFfNew ); + if ( vBlacks == NULL ) + vBlacks = Wlc_NtkGetBlacks( p, pPars, vUnmark ); + else + Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark ); + pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew ); + vPisNew = Vec_IntDup( vBlacks ); } else { @@ -945,6 +990,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Aig_ManStop( pAig ); } + if ( vBlacks ) + Vec_IntFree( vBlacks ); Vec_IntFreeP( &vFfOld ); Vec_BitFree( vUnmark ); // report the result |