From d908b3be7a30010aa698b8856fff9e8c9825a90c Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Wed, 24 Mar 2021 08:01:44 +0100 Subject: testsuite/formal: add a test for #145 --- testsuite/formal/ram/testsuite.sh | 9 +++++++++ testsuite/formal/ram/wbr_ram.sby | 16 ++++++++++++++++ testsuite/formal/ram/wbr_ram.vhd | 39 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 64 insertions(+) create mode 100755 testsuite/formal/ram/testsuite.sh create mode 100644 testsuite/formal/ram/wbr_ram.sby create mode 100644 testsuite/formal/ram/wbr_ram.vhd 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; + -- cgit v1.2.3