testsuite/formal: add a test for #145

3 files changed, 64 insertions, 0 deletions

diff --git a/testsuite/formal/ram/testsuite.sh b/testsuite/formal/ram/testsuite.sh
new file mode 100755
index 0000000..3cf2504
--- /dev/null
+++ b/testsuite/formal/ram/testsuite.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+topdir=../..
+. $topdir/testenv.sh
+
+formal wbr_ram
+
+clean
+echo OK
diff --git a/testsuite/formal/ram/wbr_ram.sby b/testsuite/formal/ram/wbr_ram.sby
new file mode 100644
index 0000000..84c8081
--- /dev/null
+++ b/testsuite/formal/ram/wbr_ram.sby
@@ -0,0 +1,16 @@
+[tasks]
+bmc
+
+[options]
+bmc: mode bmc
+bmc: depth 10
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 wbr_ram.vhd -e wbr_ram
+prep -top wbr_ram
+
+[files]
+wbr_ram.vhd
diff --git a/testsuite/formal/ram/wbr_ram.vhd b/testsuite/formal/ram/wbr_ram.vhd
new file mode 100644
index 0000000..945bd24
--- /dev/null
+++ b/testsuite/formal/ram/wbr_ram.vhd
@@ -0,0 +1,39 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity wbr_ram is
+   port (
+      clk_i     : in  std_logic;
+      addr_i    : in  std_logic_vector(7 downto 0);
+      wr_data_i : in  std_logic_vector(15 downto 0);
+      wr_en_i   : in  std_logic;
+      rd_data_o : out std_logic_vector(15 downto 0)
+   );
+end entity wbr_ram;
+
+architecture synthesis of wbr_ram is
+
+   type mem_t is array (0 to 255) of std_logic_vector(15 downto 0);
+
+begin
+
+   p_write_first : process (clk_i)
+      variable mem : mem_t := (others => (others => '0'));
+   begin
+      if rising_edge(clk_i) then
+         if wr_en_i = '1' then
+            mem(to_integer(unsigned(addr_i))) := wr_data_i;
+         end if;
+
+         rd_data_o <= mem(to_integer(unsigned(addr_i)));
+      end if;
+   end process p_write_first;
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk_i);
+
+  f_wbr : assert always {wr_en_i = '1'} |=> {rd_data_o = prev(wr_data_i)};
+
+end architecture synthesis;
+