diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-21 20:06:13 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-21 20:06:13 -0800 |
| commit | 01e6beea8e617eb5ef4f9b621b009eded9498a1f (patch) | |
| tree | 75b769832e94baf4a56f57bd5abc65312966adce /src/base/wlc/wlcAbs.c | |
| parent | c5e9506f5d5a5303b9df453fce7f313147799276 (diff) | |
| download | abc-01e6beea8e617eb5ef4f9b621b009eded9498a1f.tar.gz abc-01e6beea8e617eb5ef4f9b621b009eded9498a1f.tar.bz2 abc-01e6beea8e617eb5ef4f9b621b009eded9498a1f.zip | |
clean up
Diffstat (limited to 'src/base/wlc/wlcAbs.c')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 33 |
1 files changed, 3 insertions, 30 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index fbaa1b8a..1e5df918 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -40,33 +40,6 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) -{ - memset( pPars, 0, sizeof(WlcPdr_Par_t) ); - pPars->nBitsAdd = ABC_INFINITY; // adder bit-width - pPars->nBitsMul = ABC_INFINITY; // multiplier bit-width - pPars->nBitsMux = ABC_INFINITY; // MUX bit-width - pPars->nBitsFlop = ABC_INFINITY; // flop bit-width - pPars->nIterMax = 1000; // the max number of iterations - pPars->fXorOutput = 1; // XOR outputs of word-level miter - pPars->fCheckClauses = 1; // Check clauses in the reloaded trace - pPars->fPushClauses = 0; // Push clauses in the reloaded trace - pPars->fVerbose = 0; // verbose output - pPars->fPdrVerbose = 0; // show verbose PDR output -} - -/**Function************************************************************* - Synopsis [Mark operators that meet the abstraction criteria.] Description [This procedure returns the array of objects (vLeaves) that @@ -78,7 +51,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) +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) ); Wlc_Obj_t * pObj; int i, Count[4] = {0}; @@ -199,7 +172,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * SeeAlso [] ***********************************************************************/ -static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) +static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) { Wlc_Ntk_t * pNtkNew = NULL; Vec_Int_t * vPisOld = Vec_IntAlloc( 100 ); @@ -337,7 +310,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec SeeAlso [] ***********************************************************************/ -int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ) +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); abctime pdrClk; |