Add counter as example for initial reset problems

counter/Makefile

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

counter/counter.vhd

@@ -0,0 +1,35 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+
+entity counter is
+  port (
+    Reset_n_i : in  std_logic;
+    Clk_i     : in  std_logic;
+    Data_o    : out std_logic_vector(31 downto 0)
+  );
+end entity counter;
+
+
+
+architecture rtl of counter is
+
+
+begin
+
+
+  process (Reset_n_i, Clk_i) is
+  begin
+    if (Reset_n_i = '0') then
+      Data_o <= 32x"8";
+    elsif (rising_edge(Clk_i)) then
+      if (unsigned(Data_o) <= 64) then
+        Data_o <= std_logic_vector(unsigned(Data_o) + 1);
+      end if;
+    end if;
+  end process;
+
+
+end architecture rtl;

counter/counter_f.sby

@@ -0,0 +1,15 @@
+[options]
+mode prove
+multiclock on
+
+[engines]
+smtbmc
+
+[script]
+verific -vhdl counter.vhd
+verific -formal counter_t.sv
+prep -top counter_t
+
+[files]
+counter.vhd
+counter_t.sv

counter/counter_t.sv

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