Make the unbounded prove work

* Fixed bug in check for end value in counter unit ;)
* Use abc engine with pdr solver
* Add asserts for reset

counter/counter.vhd

@@ -28,7 +28,7 @@ begin
     if (Reset_n_i = '0') then
       Data_o <= std_logic_vector(to_unsigned(Init, Data_o'length));
     elsif (rising_edge(Clk_i)) then
-      if (unsigned(Data_o) <= 64) then
+      if (unsigned(Data_o) < 64) then
         Data_o <= std_logic_vector(unsigned(Data_o) + 1);
       end if;
     end if;

counter/counter_f.sby

@@ -3,7 +3,8 @@ mode prove
 multiclock on
 
 [engines]
-smtbmc
+#smtbmc
+abc pdr
 
 [script]
 verific -vhdl counter.vhd

counter/counter_t.sv

@@ -17,8 +17,11 @@ module counter_t (
 
   reg init_state = 1;
 
-  always @(*)
+  // Initial reset
+  always @(*) begin
     if (init_state) assume (!Reset_n_i);
+    if (!init_state) assume (Reset_n_i);
+  end
 
   always @(posedge Clk_i)
     init_state = 0;
@@ -32,9 +35,18 @@ module counter_t (
 */
 
 
-  // Proves fail, counterexample hasn't initial reset active
+  // Intermediate assertions
+  always @(*)
+    if (!Reset_n_i) assert (Data_o == `INIT_VALUE);
+
+
+  // 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));
+
 
 
 endmodule