formal_hw_verification/vai_reg/vai_reg.vhd

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;



entity vai_reg is
  generic (
    Formal : boolean := true
  );
  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;
    
    type t_vai is record
      Start  : std_logic;
      Stop   : std_logic;
      Data   : std_logic_vector(7 downto 0);
      Valid  : std_logic;
      Accept : std_logic;
    end record t_vai;
    
    signal s_job_req : t_vai;
    signal s_job_ack : t_vai;


  begin

    -- VHDL helper logic
    process is
    begin
      wait until rising_edge(Clk_i);
      s_job_req <= (DinStart_i, DinStop_i, Din_i, DinValid_i, DinAccept_o);
      s_job_ack <= (DoutStart_o, DoutStop_o, Dout_o, DoutValid_o, DoutAccept_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 {Reset_n_i = '0'[*2]; Reset_n_i = '1'[+]}[*1];


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

    -- Start stable until accepted
    JOB_REQ_START_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (DinStart_i = s_job_req.Start until_ DinAccept_o);
      
    -- Stop stable until accepted
    JOB_REQ_STOP_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (DinStop_i = s_job_req.Stop until_ DinAccept_o);
      
    -- Data stable until accepted
    JOB_REQ_DIN_STABLE : assume always
      DinValid_i and not DinAccept_o -> next (Din_i = s_job_req.Data until_ DinAccept_o);


    -- ASSERTIONS

    -- 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 (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 (DoutStart_o = s_job_ack.Start until_ DoutAccept_i);

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

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

--    READ_DATA : assert always
--      (DoutValid_o and not DoutStart_o and not DoutStop_o) ->
--      (Dout_o = s_register(to_integer(unsigned(a_addr))));


    -- 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;