Add genric setting counter end value

counter/counter.vhd

@@ -6,7 +6,8 @@ use ieee.numeric_std.all;
 
 entity counter is
   generic (
-    Init : natural := 8
+    InitVal : natural := 0;
+    EndVal  : natural := 64
   );
   port (
     Reset_n_i : in  std_logic;
@@ -26,9 +27,9 @@ begin
   process (Reset_n_i, Clk_i) is
   begin
     if (Reset_n_i = '0') then
-      Data_o <= std_logic_vector(to_unsigned(Init, Data_o'length));
+      Data_o <= std_logic_vector(to_unsigned(InitVal, Data_o'length));
     elsif (rising_edge(Clk_i)) then
-      if (unsigned(Data_o) < 64) then
+      if (to_integer(unsigned(Data_o)) < EndVal) then
         Data_o <= std_logic_vector(unsigned(Data_o) + 1);
       end if;
     end if;

counter/counter_f.sby

@@ -1,9 +1,11 @@
 [options]
 mode prove
+depth 30
 multiclock on
+wait on
 
 [engines]
-#smtbmc
+smtbmc
 abc pdr
 
 [script]

counter/counter_t.sv

@@ -5,10 +5,14 @@ module counter_t (
 );
 
 
-  `define INIT_VALUE 8
+  `define INITVAL 8
+  `define ENDVAL  64
 
 
-  counter #(.Init(`INIT_VALUE)) counter_i (
+  counter #(
+    .InitVal(`INITVAL),
+    .EndVal(`ENDVAL)
+  ) counter_i (
     .Reset_n_i(Reset_n_i),
     .Clk_i(Clk_i),
     .Data_o(Data_o)
@@ -34,18 +38,16 @@ module counter_t (
   end
 */
 
-
   // Intermediate assertions
   always @(*)
-    if (!Reset_n_i) assert (Data_o == `INIT_VALUE);
+    if (!Reset_n_i) assert (Data_o == `INITVAL);
 
 
-  // Fail with unbounded prove using SMTBMC, maybe the assertions have to be more strict
-  // there have to be more restrictions.
-  // With abc pdr is can be successfully proved
-  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);
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o == 64 |=> $stable(Data_o));
+  // Fails with unbounded prove using SMTBMC, maybe
+  // the assumptions/assertions have to be more strict.
+  // With abc pdr this can be successfully proved.
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o <  `ENDVAL |=> Data_o == $past(Data_o) + 1);
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o == `ENDVAL |=> $stable(Data_o));