diff --git a/fsm.v b/fsm.v deleted file mode 100644 index 272c4a898..000000000 --- a/fsm.v +++ /dev/null @@ -1,28 +0,0 @@ -module fsm (out); -output out; - -wire [2:0] ns; -wire [2:0] cs; - -always @( ns or cs ) -begin -case (cs) - 0 : ns = 3'b010; - 1 : ns = 3'b001; - 2 : ns = 3'b000; - 3 : ns = 3'b101; - 4 : ns = 3'b001; - 5 : ns = 3'b111; - 6 : ns = 3'b001; - 7 : ns = 3'b110; -endcase -end - -assign out = cs == 3'b001; - -wire [2:0] const0 = 3'h0; - - -CPL_FF#3 ff3 ( .q(cs), .qbar(), .d(ns), .clk(), .arst(), .arstval(const0) ); - -endmodule diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 9cb34bf3a..686d9f009 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -163,20 +163,6 @@ struct Wlc_Ntk_t_ typedef struct Wlc_Par_t_ Wlc_Par_t; struct Wlc_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 -}; - - -typedef struct WlcPdr_Par_t_ WlcPdr_Par_t; -struct WlcPdr_Par_t_ { int nBitsAdd; // adder bit-width int nBitsMul; // multiplier bit-widht @@ -190,7 +176,6 @@ struct WlcPdr_Par_t_ 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); } @@ -294,7 +279,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, WlcPdr_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 ========================================================*/ @@ -303,7 +288,6 @@ 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 fbaa1b8a7..1e5df918b 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -38,33 +38,6 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu /// 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->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.] @@ -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; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 7801abc66..df736e702 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); - WlcPdr_Par_t Pars, * pPars = &Pars; + Wlc_Par_t Pars, * pPars = &Pars; int c; - WlcPdr_ManSetDefaultParams( pPars ); + Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) { diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index e6ab0739c..c8fc15a76 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -114,6 +114,8 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) 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 }