aboutsummaryrefslogtreecommitdiffstats
path: root/testsuite/formal/ram/wbr_ram.vhd
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/formal/ram/wbr_ram.vhd')
-rw-r--r--testsuite/formal/ram/wbr_ram.vhd39
1 files changed, 39 insertions, 0 deletions
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;
+