diff options
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/wlc.h | 1 | ||||
-rw-r--r-- | src/base/wlc/wlcAbs.c | 111 | ||||
-rw-r--r-- | src/base/wlc/wlcCom.c | 2 |
3 files changed, 113 insertions, 1 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 91dc0573..9ca56917 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -277,6 +277,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) /*=== wlcAbs.c ========================================================*/ extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); +extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcAbs2.c ========================================================*/ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ 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 diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 6b542b94..e980752b 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -541,7 +541,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); return 0; } - Wlc_NtkAbsCore( pNtk, pPars ); + Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" ); |