vhd :file: vai_reg_tb.vhd
library ieee;
use     ieee.std_logic_1164.all;
use     ieee.numeric_std.all;

entity vai_reg_tb is
-- Testbench has no ports
end entity vai_reg_tb ;

architecture tb of vai_reg_tb is
constant period         : time := 10 ns;

signal clk, reset       : std_logic := '0';
signal tb_complete      : std_logic := '0';

signal     Din_i        : std_logic_vector(7 downto 0) := (others => '0');
signal     DinValid_i   : std_logic := '0';
signal     DinStart_i   : std_logic := '0';
signal     DinStop_i    : std_logic := '0';
signal     DoutAccept_i : std_logic := '0';
signal     Dout_o       : std_logic_vector(7 downto 0);
signal     DoutValid_o  : std_logic;
signal     DoutStart_o  : std_logic;
signal     DoutStop_o   : std_logic;
signal     DinAccept_o  : std_logic;
begin

clk <= not clk after period/2 when tb_complete /= '1' else '0';

uut : entity work.vai_reg
    port map (
    reset_n_i => reset,
    clk_i       => clk,
    din_i       => din_i,
    dinvalid_i  => dinvalid_i,
    dinstart_i  => dinstart_i,
    dinstop_i   => dinstop_i,
    dinaccept_o => dinaccept_o,

    dout_o      => dout_o,
    doutvalid_o => doutvalid_o,
    doutstart_o => doutstart_o,
    doutstop_o  => doutstop_o,
    doutaccept_i=> doutaccept_i
    );
sim : process
begin
    wait for 10 us;
end process sim;
end architecture tb;

vhd :file: vai_reg.vhd
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity vai_reg is
  generic (
    Formal : boolean := false
  );
  port (
    Reset_n_i    : in  std_logic;
    Clk_i        : in  std_logic;
    -- req
    Din_i        : in  std_logic_vector(7 downto 0);
    DinValid_i   : in  std_logic;
    DinStart_i   : in  std_logic;
    DinStop_i    : in  std_logic;
    DinAccept_o  : out std_logic;
    -- ack
    Dout_o       : out std_logic_vector(7 downto 0);
    DoutValid_o  : out std_logic;
    DoutStart_o  : out std_logic;
    DoutStop_o   : out std_logic;
    DoutAccept_i : in  std_logic
  );
end entity vai_reg;
architecture rtl of vai_reg is

  constant C_READ  : std_logic_vector(3 downto 0) := x"0";
  constant C_WRITE : std_logic_vector(3 downto 0) := x"1";

  type t_fsm_state is (IDLE, GET_HEADER, GET_DATA,
                       SET_DATA, SEND_HEADER, SEND_DATA, SEND_FOOTER);
  signal s_fsm_state : t_fsm_state;

  type t_register is array(0 to 7) of std_logic_vector(7 downto 0);
  signal s_register : t_register;

  signal s_header : std_logic_vector(7 downto 0);
  signal s_data   : std_logic_vector(7 downto 0);

  signal s_error : boolean;
  signal s_dout_accepted : boolean;

  alias a_addr : std_logic_vector(3 downto 0) is s_header(7 downto 4);

begin

  s_dout_accepted <= (DoutValid_o and DoutAccept_i) = '1';

  process (Reset_n_i, Clk_i) is
  begin
    if (Reset_n_i = '0') then
      DinAccept_o <= '0';
      DoutStart_o <= '0';
      DoutStop_o  <= '0';
      DoutValid_o <= '0';
      Dout_o      <= (others => '0');
      s_header    <= (others => '0');
      s_data      <= (others => '0');
      s_register  <= (others => (others => '0'));
      s_error     <= false;
      s_fsm_state <= IDLE;
    elsif (rising_edge(Clk_i)) then
      case s_fsm_state is

        when IDLE =>
          DinAccept_o <= '0';
          DoutStart_o <= '0';
          DoutStop_o  <= '0';
          DoutValid_o <= '0';
          Dout_o      <= (others => '0');
          s_header    <= (others => '0');
          s_data      <= (others => '0');
          s_error     <= false;
          DinAccept_o <= '1';
          s_fsm_state <= GET_HEADER;

        when GET_HEADER =>
          if (DinValid_i = '1' and DinStart_i = '1') then
            s_header <= Din_i;
            if (Din_i(3 downto 0) = C_READ and DinStop_i = '1') then
              DinAccept_o <= '0';
              s_fsm_state <= GET_DATA;
            elsif (Din_i(3 downto 0) = C_WRITE and DinStop_i = '0') then
              s_fsm_state <= SET_DATA;
            else
              DinAccept_o <= '0';
              s_fsm_state <= IDLE;
            end if;
          end if;

        when GET_DATA =>
          if (unsigned(a_addr) <= 7) then
            s_data <= s_register(to_integer(unsigned(a_addr)));
          else
            s_error <= true;
            s_data  <= (others => '0');
          end if;
          s_fsm_state <= SEND_HEADER;

        when SET_DATA =>
          if (DinValid_i = '1') then
            DinAccept_o <= '0';
            if (DinStop_i = '1') then
              if (unsigned(a_addr) <= 7) then
                s_register(to_integer(unsigned(a_addr))) <= Din_i;
              else
                s_error <= true;
              end if;
              s_fsm_state <= SEND_HEADER;
            else
              s_fsm_state <= IDLE;
            end if;
          end if;

        when SEND_HEADER =>
          DoutValid_o <= '1';
          DoutStart_o <= '1';
          Dout_o      <= s_header;
          if (s_dout_accepted) then
            DoutValid_o <= '0';
            DoutStart_o <= '0';
            if (s_header(3 downto 0) = C_WRITE) then
              s_fsm_state <= SEND_FOOTER;
            else
              s_fsm_state <= SEND_DATA;
            end if;
          end if;

        when SEND_DATA =>
          DoutValid_o <= '1';
          Dout_o      <= s_data;
          if (s_dout_accepted) then
            DoutValid_o <= '0';
            s_fsm_state <= SEND_FOOTER;
          end if;

        when SEND_FOOTER =>
          DoutValid_o <= '1';
          DoutStop_o  <= '1';
          Dout_o      <= x"01" when s_error else x"00";
          if (s_dout_accepted) then
            Dout_o      <= (others => '0');
            DoutValid_o <= '0';
            DoutStop_o  <= '0';
            s_fsm_state <= IDLE;
          end if;

        when others => null;

      end case;
    end if;
  end process;

  FormalG : if Formal generate

    signal s_addr : natural range 0 to 15;

    type t_cmd is (READ, WRITE, NOP);
    signal s_cmd : t_cmd;

  begin

    -- VHDL helper logic
    process is
    begin
      wait until rising_edge(Clk_i);
      if (s_fsm_state = GET_HEADER) then
        if (DinValid_i = '1' and DinStart_i = '1') then
          s_cmd  <= READ  when Din_i(3 downto 0) = x"0" else
                    WRITE when Din_i(3 downto 0) = x"1" else
                    NOP;
          s_addr <= to_integer(unsigned(Din_i(7 downto 4)));
        end if;
      end if;
    end process;

    default clock is rising_edge(Clk_i);

    -- RESTRICTIONS

    -- Initial reset
    INITIAL_RESET : restrict {not Reset_n_i[*2]; Reset_n_i[+]}[*1];

    -- CONSTRAINTS

    -- Valid stable until accepted
    JOB_REQ_VALID_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (stable(DinValid_i) until_ DinAccept_o);

    -- Start stable until accepted
    JOB_REQ_START_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (stable(DinStart_i) until_ DinAccept_o);

    -- Stop stable until accepted
    JOB_REQ_STOP_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (stable(DinStop_i) until_ DinAccept_o);

    -- Data stable until accepted
    JOB_REQ_DIN_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (stable(Din_i) until_ DinAccept_o);

    -- ASSERTIONS

    -- Reset values
    AFTER_RESET : assert always
      not Reset_n_i
      ->
      s_fsm_state = IDLE and
      not DinAccept_o and
      not DoutStart_o and
      not DoutStop_o  and
      not DoutValid_o and
      s_register = (0 to 7 => x"00");

    -- FSM states in valid range
    FSM_STATES_VALID : assert always
      s_fsm_state = IDLE or s_fsm_state = GET_HEADER or
      s_fsm_state = GET_DATA or s_fsm_state = SET_DATA or
      s_fsm_state = SEND_HEADER or s_fsm_state = SEND_DATA or
      s_fsm_state = SEND_FOOTER;

    -- Discard jobs with invalid command
    INV_CMD_DISCARD : assert always
      s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
      Din_i(3 downto 0) /= x"0" and Din_i(3 downto 0) /= x"1"
      ->
      next s_fsm_state = IDLE;

    -- Discard read job with invalid stop flags
    READ_INV_FLAGS_DISCARD : assert always
      s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
      Din_i(3 downto 0) = x"0" and DinStop_i = '0'
      ->
      next s_fsm_state = IDLE;

    -- Discard write job with invalid stop flags
    WRITE_INV_FLAGS_DISCARD : assert always
      s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
      Din_i(3 downto 0) = x"1" and DinStop_i = '1'
      ->
      next s_fsm_state = IDLE;

    -- After a valid job read request,
    -- a job read acknowledge has to follow
    READ_VALID_ACK : assert always
      {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
       Din_i(3 downto 0) = x"0" and DinStop_i = '1'}
      |=>
      {-- Job ack header cycle
       not DoutValid_o [*];
       DoutValid_o and DoutStart_o and not DoutAccept_i [*];
       DoutValid_o and DoutStart_o and DoutAccept_i;
       -- Job ack data cycle
       not DoutValid_o [*];
       DoutValid_o and not DoutStart_o and not DoutStop_o and not DoutAccept_i [*];
       DoutValid_o and not DoutStart_o and not DoutStop_o and DoutAccept_i;
       -- Job ack footer cycle
       not DoutValid_o [*];
       DoutValid_o and DoutStop_o};

    -- After a valid job write request,
    -- a job read acknowledge has to follow
    WRITE_VALID_ACK : assert always
      {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
       Din_i(3 downto 0) = x"1" and DinStop_i = '0';
       not DinValid_i [*];
       DinValid_i and DinStop_i}
      |=>
      {-- Job ack header cycle
       not DoutValid_o [*];
       DoutValid_o and DoutStart_o and not DoutAccept_i [*];
       DoutValid_o and DoutStart_o and DoutAccept_i;
       -- Job ack footer cycle
       not DoutValid_o [*];
       DoutValid_o and DoutStop_o};

     -- Start & stop flag have to be exclusive
     JOB_ACK_NEVER_START_STOP : assert never
       DoutStart_o and DoutStop_o;

     -- Start & Stop have to be active together with valid
     JOB_ACK_START_STOP_VALID : assert always
       DoutStart_o or DoutStop_o -> DoutValid_o;

     -- Valid has to be stable until accepted
     JOB_ACK_VALID_STABLE : assert always
       DoutValid_o and not DoutAccept_i -> next (stable(DoutValid_o) until_ DoutAccept_i);

     -- Start has to be stable until accepted
     JOB_ACK_START_STABLE : assert always
       DoutValid_o and not DoutAccept_i -> next (stable(DoutStart_o) until_ DoutAccept_i);

     -- Stop has to be stable until accepted
     JOB_ACK_STOP_STABLE : assert always
       DoutValid_o and not DoutAccept_i -> next (stable(DoutStop_o) until_ DoutAccept_i);

     -- Data has to be stable until accepted
     JOB_ACK_DOUT_STABLE : assert always
       DoutValid_o and not DoutAccept_i -> next (stable(Dout_o) until_ DoutAccept_i);

    -- Data from selected address has to be read
    READ_DATA : assert always
      DoutValid_o and not DoutStart_o and not DoutStop_o and s_addr <= 7
      ->
      Dout_o = s_register(s_addr);

    -- 0 has to be read when invalid address is given
    READ_DATA_INV_ADDR : assert always
      DoutValid_o and not DoutStart_o and not DoutStop_o and s_addr > 7
      ->
      Dout_o = x"00";

    -- Register has to be written at given address with given data
    -- when correct job req write occurs
    WRITE_DATA : assert always
      -- Job req header cycle
      {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
       Din_i(3 downto 0) = x"1" and unsigned(Din_i(7 downto 4)) <= 7 and DinStop_i = '0';
       -- Job req data / footer cycle
       not DinValid_i [*];
       DinValid_i and not DinStart_i and DinStop_i and not DinAccept_o [*];
       DinValid_i and not DinStart_i and DinStop_i and DinAccept_o}
      |=>
      {s_register(s_addr) = prev(Din_i)};

    -- FUNCTIONAL COVERAGE

    FOOTER_VALID : cover {DoutValid_o = '1' and DoutStop_o = '1' and Dout_o = 8x"0"};
    FOOTER_ERR   : cover {DoutValid_o = '1' and DoutStop_o = '1' and Dout_o = 8x"1"};

  end generate FormalG;

end architecture rtl;

translate_expression: cannot handle IIR_KIND_PSL_STABLE (vai_reg.vhd:205:47)

******************** GHDL Bug occurred ***************************
Please report this bug on https://github.com/ghdl/ghdl/issues
GHDL release: 1.0-dev (v0.37.0-1099-g3bf13614) [Dunoon edition]
Compiled with GNAT Version: 8.4.0
Target: x86_64-linux-gnu
/home/dev/projects/test_psl/
Command line:
ghdl -r --std=08 -fpsl vai_reg_tb
Exception TYPES.INTERNAL_ERROR raised
Exception information:
raised TYPES.INTERNAL_ERROR : vhdl-errors.adb:32
Call stack traceback locations:
0x5562666f7036 0x5562668d3799 0x5562668a4b34 0x5562668a4c7b 0x5562668a59ad 0x5562668a7e77 0x5562668a7ca7 0x5562668a7f85 0x556266915f26 0x55626687d709 0x55626687a81b 0x556266888d86 0x55626691a89d 0x556266859e3a 0x556266793177 0x55626691e211 0x55626654ca85 0x7f44f5001bf5 0x55626654b218 0xfffffffffffffffe
******************************************************************