diff --git a/fifo/fifo.vhd b/fifo/fifo.vhd
index 494d705..a5968f1 100644
--- a/fifo/fifo.vhd
+++ b/fifo/fifo.vhd
@@ -283,6 +283,49 @@ begin
       {{s_cnt = 7 and Wen_i = '1' and Din_i = s_data} : {Ren_i[->8]}}
       |=> {Dout_o = s_data};
 
+
+    -- An alternative for GHDL: Replacing the [->] goto operator
+    -- by counting Ren_i starting when s_data is written into fifo.
+    -- The properties have to be slightly modified only.
+    -- Sadly proving these needs much more (engine dependend) time than
+    -- the separate checks above. I assume the counters are the reason.
+    gen_data_checks : for i in 0 to Depth-1 generate
+
+    begin
+
+      GEN : if i = 0 generate
+
+        DATA_FLOW_GEN : assert always
+          {{s_cnt = i and Wen_i = '1' and Din_i = s_data} ; {Ren_i}}
+          |=> {Dout_o = s_data};
+
+      else generate
+
+        signal s_ren_cnt : integer range -1 to i+1 := -1;
+
+      begin
+
+        process (Reset_n_i, Clk_i) is
+        begin
+          if not Reset_n_i then
+            s_ren_cnt <= -1;
+          elsif (rising_edge(Clk_i)) then
+            if s_cnt = i and Wen_i = '1' and Din_i = s_data then
+              s_ren_cnt <= 1 when Ren_i else 0;
+            else
+              s_ren_cnt <= s_ren_cnt + 1 when Ren_i = '1' and s_ren_cnt >= 0;
+            end if;
+          end if;
+        end process;
+
+        DATA_FLOW_GEN : assert always
+          {{s_cnt = i and Wen_i = '1' and Din_i = s_data} : {Ren_i[*]; s_ren_cnt = i+1}}
+          |-> {Dout_o = s_data};
+
+      end generate GEN;
+
+    end generate gen_data_checks;
+
   end generate FormalG;
 
 
diff --git a/fifo/symbiyosys.sby b/fifo/symbiyosys.sby
index 2eb4bd1..699d5e4 100644
--- a/fifo/symbiyosys.sby
+++ b/fifo/symbiyosys.sby
@@ -15,7 +15,7 @@ bmc: abc bmc3
 prove: abc pdr
 
 [script]
-ghdl --std=08 -gFormal=true -gDepth=8 -gWidth=16 fifo.vhd -e fifo
+ghdl --std=08 -gFormal=true -gDepth=8 -gWidth=4 fifo.vhd -e fifo
 prep -auto-top
 
 [files]
diff --git a/fwft_fifo/symbiyosys.sby b/fwft_fifo/symbiyosys.sby
index 4bc6ff1..aa197f2 100644
--- a/fwft_fifo/symbiyosys.sby
+++ b/fwft_fifo/symbiyosys.sby
@@ -15,7 +15,7 @@ bmc: abc bmc3
 prove: abc pdr
 
 [script]
-ghdl --std=08 -gFormal=true -gDepth=8 -gWidth=16 fifo.vhd fwft_fifo.vhd -e fwft_fifo
+ghdl --std=08 -gFormal=true -gDepth=8 -gWidth=4 fifo.vhd fwft_fifo.vhd -e fwft_fifo
 prep -top fwft_fifo
 
 # Convert all assumes to asserts in sub-units
diff --git a/vai_fifo/symbiyosys.sby b/vai_fifo/symbiyosys.sby
index 04a0ce9..75a821d 100644
--- a/vai_fifo/symbiyosys.sby
+++ b/vai_fifo/symbiyosys.sby
@@ -15,7 +15,7 @@ bmc: abc bmc3
 prove: abc pdr
 
 [script]
-ghdl --std=08 -gFormal=true -gDepth=8 -gWidth=16 fifo.vhd fwft_fifo.vhd vai_fifo.vhd -e vai_fifo
+ghdl --std=08 -gFormal=true -gDepth=8 -gWidth=4 fifo.vhd fwft_fifo.vhd vai_fifo.vhd -e vai_fifo
 prep -top vai_fifo
 
 # Convert all assumes to asserts in sub-units