summaryrefslogtreecommitdiffstats
path: root/src/base/wlc
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/wlc')
-rw-r--r--src/base/wlc/wlc.h18
-rw-r--r--src/base/wlc/wlcAbs.c27
-rw-r--r--src/base/wlc/wlcCom.c4
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 )
{