parameterize design; fix minor makefile problemswq

counter/Makefile

@@ -1,6 +1,7 @@
-alu: counter.vhd counter_t.sv counter_f.sby
+.PHONY: counter
+counter: counter.vhd counter_t.sv counter_f.sby
 	sby -f -d work counter_f.sby
 
-
+.PHONY: clean
 clean:
 	rm -rf work

counter/counter.vhd

@@ -5,6 +5,9 @@ use ieee.numeric_std.all;
 
 
 entity counter is
+  generic (
+    Init : natural := 8
+  );
   port (
     Reset_n_i : in  std_logic;
     Clk_i     : in  std_logic;
@@ -23,7 +26,7 @@ begin
   process (Reset_n_i, Clk_i) is
   begin
     if (Reset_n_i = '0') then
-      Data_o <= 32x"8";
+      Data_o <= std_logic_vector(to_unsigned(Init, Data_o'length));
     elsif (rising_edge(Clk_i)) then
       if (unsigned(Data_o) <= 64) then
         Data_o <= std_logic_vector(unsigned(Data_o) + 1);
@@ -33,3 +36,4 @@ begin
 
 
 end architecture rtl;
+

counter/counter_t.sv

@@ -1,27 +1,29 @@
 module counter_t (
-    inout         Reset_n_i,
+    input         Reset_n_i,
     input         Clk_i,
     input  [31:0] Data_i,
     output [31:0] Data_o
 );
 
 
-  counter counter_i (
+  `define INIT_VALUE 8
+
+
+  counter #(.Init(`INIT_VALUE)) counter_i (
     .Reset_n_i(Reset_n_i),
     .Clk_i(Clk_i),
     .Data_o(Data_o)
   );
 
 
-  reg init_state;
+  reg init_state = 1;
 
-  initial init_state = 1;
+  always @(*)
+    if (init_state) assume (!Reset_n_i);
 
   always @(posedge Clk_i)
     init_state = 0;
 
-  always @(*)
-    assume (Reset_n_i == ~init_state);
 
 /*
   // Don't works with Verific at the moment
@@ -32,8 +34,9 @@ module counter_t (
 
 
   // Proves fail, counterexample hasn't initial reset active
-  assert property (@(posedge Clk_i) Data_o >= 8 && Data_o <= 64);
+  assert property (@(posedge Clk_i) Data_o >= `INIT_VALUE && Data_o <= 64);
   assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o < 64 |=> Data_o == $past(Data_o) + 1);
 
 
 endmodule
+