diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-19 09:55:58 -0800 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-19 09:55:58 -0800 |
commit | 6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c (patch) | |
tree | 3e431a17544f528d4f00ea0995e557978fa38ff2 /src/base/wlc/wlcAbs.c | |
parent | 24fdcecb2d034af4d7f7c26ec083f6baf1434018 (diff) | |
download | abc-6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c.tar.gz abc-6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c.tar.bz2 abc-6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c.zip |
working on pdr with wla
Diffstat (limited to 'src/base/wlc/wlcAbs.c')
-rw-r--r-- | src/base/wlc/wlcAbs.c | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 318df4dd..cfd1155d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -285,6 +285,117 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec /**Function************************************************************* + Synopsis [Performs PDR with word-level abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + abctime clk = Abc_Clock(); + int nIters, nNodes, nDcFlops, RetValue = -1; + // start the bitmap to mark objects that cannot be abstracted because of refinement + // currently, this bitmap is empty because abstraction begins without refinement + Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + // set up parameters to run PDR + Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; + Pdr_ManSetDefaultParams( pPdrPars ); + pPdrPars->fVerbose = pPars->fPdrVerbose; + + // perform refinement iterations + for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) + { + Aig_Man_t * pAig; + Abc_Cex_t * pCex; + Vec_Int_t * vPisNew, * vRefine; + Gia_Man_t * pGia, * pTemp; + Wlc_Ntk_t * pAbs; + + if ( pPars->fVerbose ) + printf( "\nIteration %d:\n", nIters ); + + // get abstracted GIA and the set of pseudo-PIs (vPisNew) + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); + + // if the abstraction has flops with DC-init state, + // new PIs were introduced by bit-blasting at the end of the PI list + // here we move these variables to be *before* PPIs, because + // PPIs are supposed to be at the end of the PI list for refinement + nDcFlops = Wlc_NtkDcFlopNum(pAbs); + if ( nDcFlops > 0 ) // DC-init flops are present + { + pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops ); + Gia_ManStop( pTemp ); + } + // if the word-level outputs have to be XORs, this is a place to do it + if ( pPars->fXorOutput ) + { + pGia = Gia_ManTransformMiter2( pTemp = pGia ); + Gia_ManStop( pTemp ); + } + if ( pPars->fVerbose ) + { + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); + Gia_ManPrintStats( pGia, NULL ); + } + Wlc_NtkFree( pAbs ); + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pAig = Gia_ManToAigSimple( pGia ); + RetValue = Pdr_ManSolve( pAig, pPdrPars ); + pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + + // consider outcomes + if ( pCex == NULL ) + { + assert( RetValue ); // proved or undecided + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + break; + } + + // perform refinement + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + if ( vRefine == NULL ) // real CEX + { + Abc_CexFree( pCex ); // return CEX in the future + break; + } + + // update the set of objects to be un-abstracted + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + Vec_IntFree( vRefine ); + Abc_CexFree( pCex ); + } + + Vec_BitFree( vUnmark ); + // report the result + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Abstraction " ); + if ( RetValue == 0 ) + printf( "resulted in a real CEX" ); + else if ( RetValue == 1 ) + printf( "is successfully proved" ); + else + printf( "timed out" ); + printf( " after %d iterations. ", nIters ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return RetValue; +} + +/**Function************************************************************* + Synopsis [Performs abstraction.] Description [Derives initial abstraction based on user-specified |