RD_TRANSPARENT not set correctly for memories

[MJoergen]

When inferring a single-port RAM with WRITE_FIRST behaviour, formal verification fails in the assert statement. It is seen that the input to yosys is incorrect.

The source file I'm using is:

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;

The corresponding yosys script is:

[tasks]
bmc

[options]
bmc: mode bmc
bmc: depth 10

[engines]
smtbmc

[script]
ghdl --std=08 wbr_ram.vhd -e wbr_ram
prep -top wbr_ram

[files]
wbr_ram.vhd

To examine the input to yosys I execute the command yosys -m ghdl -p 'ghdl --std=08 wbr_ram; dump'. This generates almost 200 lines of output, but the lines I'm focused on are these (starting at line 67):

  cell $mem \41
    parameter \WR_CLK_POLARITY 1'1
    parameter \WR_CLK_ENABLE 1'1
    parameter \RD_TRANSPARENT 1'0
    parameter \RD_CLK_POLARITY 1'1
    parameter \RD_CLK_ENABLE 1'1
    parameter \RD_PORTS 1
    parameter \WR_PORTS 1

In particular, the value of the parameter RD_TRANSPARENT seems incorrect. I believe it should be 1 and not 0.

[tgingold]

If you look at the output of ghdl --synth --std=08 wbr_ram.vhdl -e, you can see that the write first is correctly inferred.

So the issue is either within the plugin or later. Still investigating.

[tgingold]

And indeed, RD_TRANSPARENT is always set to 0 in the plugin.

[tgingold]

Should be fixed. Thank you for the issue.