summaryrefslogtreecommitdiffstats
path: root/src/base/wlc
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/wlc')
-rw-r--r--src/base/wlc/wlc.h1
-rw-r--r--src/base/wlc/wlcAbs.c111
-rw-r--r--src/base/wlc/wlcCom.c2
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" );