diff options
Diffstat (limited to 'src/base/wlc')
| -rw-r--r-- | src/base/wlc/wlc.h | 18 | ||||
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 27 | ||||
| -rw-r--r-- | src/base/wlc/wlcCom.c | 4 |
3 files changed, 45 insertions, 4 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 9ca56917..cf8bdab4 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -174,6 +174,21 @@ struct Wlc_Par_t_ int fPdrVerbose; // verbose output }; + +typedef struct WlcPdr_Par_t_ WlcPdr_Par_t; +struct WlcPdr_Par_t_ +{ + int nBitsAdd; // adder bit-width + int nBitsMul; // multiplier bit-widht + int nBitsMux; // MUX bit-width + int nBitsFlop; // flop bit-width + int nIterMax; // the max number of iterations + int fXorOutput; // XOR outputs of word-level miter + int fVerbose; // verbose output + int fPdrVerbose; // verbose output +}; + + static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; } static inline int Wlc_NtkObjNumMax( Wlc_Ntk_t * p ) { return p->iObj; } static inline int Wlc_NtkPiNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vPis); } @@ -277,7 +292,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 ); +extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ); /*=== wlcAbs2.c ========================================================*/ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ @@ -286,6 +301,7 @@ extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int i extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ); /*=== wlcNtk.c ========================================================*/ extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ); +extern void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ); extern char * Wlc_ObjTypeName( Wlc_Obj_t * p ); extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc ); extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg ); diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 902c060d..8fde7f56 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -40,6 +40,31 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p ); /**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->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 @@ -310,7 +335,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec SeeAlso [] ***********************************************************************/ -int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ) { abctime clk = Abc_Clock(); abctime pdrClk; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index e980752b..d30b376e 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -458,9 +458,9 @@ usage: int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - Wlc_Par_t Pars, * pPars = &Pars; + WlcPdr_Par_t Pars, * pPars = &Pars; int c; - Wlc_ManSetDefaultParams( pPars ); + WlcPdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) { |