clean up

fsm.v

-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

src/base/wlc/wlc.h

@@ -170,27 +170,12 @@ struct Wlc_Par_t_
     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 
-    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                    fCheckClauses;      // Check clauses in the reloaded trace                    
     int                    fPushClauses;       // Push clauses in the reloaded trace                    
     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);                                            }
@@ -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 );

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;

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

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
 }