fifo: Add example for GHDL property replication

* By replacing the goto operator with non-literal parameter
  by counting the read enabled with simple VHDL counters we
  can now replicate the properties instead of writing them
  all out.
* Decrease the data width to decrease run-time of unbounded proofs

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;
 
 

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]

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

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