luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

added datastructure for %pdra options

This commit is contained in:
Yen-Sheng Ho 2017-02-20 11:07:12 -08:00
parent 222b3741a4
commit 19510bd38e
3 changed files with 45 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/base/wlc/wlc.h
View File

@ -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 );

27
src/base/wlc/wlcAbs.c
View File

@ -38,6 +38,31 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p );
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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.]
@ -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;

4
src/base/wlc/wlcCom.c
View File

@ -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 )
{