vme_data_bus.vhd

library ieee;
use ieee.std_logic_1164.all;
library vme;
use vme.vme_pkg.all;

entity vme_data_bus is
  generic (
    CLOCK_PERIOD  : integer := 10;
    FORMAL        : boolean := true
    );
  port (
    signal clk      : in std_logic; -- CLOCK with period CLOCK_PERIOD

    -- _n indicate active low (inverted) signals

    signal vme_addr_i		: in std_logic_vector(31 downto 0);
    signal vme_addr_o		: out std_logic_vector(31 downto 0);
    signal vme_addr_dir		: out std_logic := c_PIN_IN;
    signal vme_addr_oe_n	: out std_logic := c_OE_OFF;

    signal vme_am_i		: in am_vec_t;
    signal vme_am_o		: out am_vec_t;
    signal vme_am_dir		: out std_logic := c_PIN_IN;
--    signal vme_am_oe_n	: out std_logic -- Shared with addr
    signal vme_write_n_i        : in std_logic;
    signal vme_write_n_o        : out std_logic;
    -- write shares DIR and OE with AM

    signal vme_data_i		: in std_logic_vector(31 downto 0);
    signal vme_data_o		: out std_logic_vector(31 downto 0);
    signal vme_data_dir		: out std_logic := c_PIN_IN;
    signal vme_data_oe_n	: out std_logic := c_OE_OFF;

    signal vme_as_n_i		: in std_logic;
    signal vme_as_n_o		: out std_logic;
    signal vme_as_n_dir		: out std_logic := c_PIN_IN;

    signal vme_iack_n_i		: in std_logic;
    signal vme_iack_n_o		: out std_logic;
    signal vme_iack_n_dir	: out std_logic := c_PIN_IN;

    -- Always enabled, always input
    signal vme_iackin_n		: in std_logic;

    -- Enable IACKOUT_n. Will be pulled low
    signal vme_iackout_n_oe_n	: out std_logic := c_OE_OFF;

    signal vme_dtack_n_i	: in std_logic;
--    signal vme_dtack_n_o	: out std_logic;
    signal vme_dtack_n_dir	: out std_logic := c_PIN_IN;

--    signal vme_retry_i	        : in std_logic;
--    signal vme_retry_o	        : out std_logic;
--    signal vme_retry_dir	: out std_logic := c_PIN_IN;

    signal vme_ds_n_i	        : in std_logic_vector(1 downto 0);
    signal vme_ds_n_o	        : out std_logic_vector(1 downto 0);
    signal vme_ds_n_dir	        : out std_logic := c_PIN_IN;

    signal vme_berr_n_i         : in std_logic;
    signal vme_berr_n_o         : out std_logic;
    signal vme_berr_n_dir       : out std_logic;


    ---------------------------------
    -- SYS CONTROL START           --
    ---------------------------------

    -- signal vme_sysreset_n_i     : in std_logic;
    -- signal vme_sysreset_n_o     : out std_logic;
    -- signal vme_sysreset_n_dir   : out std_logic

    -- signal vme_sysfail_n_i     : in std_logic;
    -- signal vme_sysfail_n_o     : out std_logic;
    -- signal vme_sysfail_n_dir   : out std_logic

    -- signal vme_sysclk_i     : in std_logic;
    -- signal vme_sysclk_o     : out std_logic;
    -- signal vme_sysclk_dir   : out std_logic

    ---------------------------------
    -- SYS CONTROL END             --
    ---------------------------------


    ---------------------------------
    -- BUS REQUEST START           --
    ---------------------------------

    -- signal vme_br_n_i		: in std_logic_vector(3 downto 0);
    -- signal vme_br_n_o		: out std_logic_vector(3 downto 0);
    -- signal vme_br_n_dir		: out std_logic;
    -- signal vme_br_n_oe_n	: out std_logic;

    -- -- Fixed DIR = input
    -- signal vme_bgin_n_i		: in std_logic_vector(3 downto 0);
    -- signal vme_bgin_n_oe_n	: out std_logic;

    -- -- Fixed DIR = output
    -- signal vme_bgout_n_o	: out std_logic_vector(3 downto 0);
    -- signal vme_bgout_n_oe_n	: out std_logic;

    -- signal vme_bbsy_n_i         : in std_logic;
    -- signal vme_bbsy_n_o         : out std_logic;
    -- signal vme_bbsy_n_dir       : out std_logic;

    -- signal vme_bclr_n_i         : in std_logic;
    -- signal vme_bclr_n_o         : out std_logic;
    -- signal vme_bclr_n_dir       : out std_logic

    ---------------------------------
    -- BUS REQUEST END           --
    ---------------------------------


    ---------------------------------
    -- Mini BUS REQUEST START      --
    ---------------------------------
    -- Request bus
    signal vme_br_n_o		: out std_logic_vector(3 downto 0);
    -- Receive bus grant
    signal vme_bgin_n_i		: in std_logic_vector(3 downto 0);
    -- Output bus grant
    signal vme_bgout_n_o	: out std_logic_vector(3 downto 0);
    -- Signal bus ownership
    signal vme_bbsy_n_o         : out std_logic;
    -- Signal the we should clear bus
    signal vme_bclr_n_i         : in std_logic;

    ---------------------------------
    -- Mini BUS REQUEST END        --
    ---------------------------------


    ---------------------------------
    -- Serial data interface START --
    ---------------------------------

    -- signal vme_serdat_n_i         : in std_logic;
    -- signal vme_serdat_n_o         : out std_logic;
    -- signal vme_serdat_n_dir       : out std_logic

    -- signal vme_serclk_i         : in std_logic;
    -- signal vme_serclk_o         : out std_logic;
    -- signal vme_serclk_dir       : out std_logic

    -------------------------------
    -- Serial data interface END --
    -------------------------------

    -- This is asserted when not IDLE.
    signal busy                 : out std_logic := '0';
    
    -- Latched from last VME read operation.
    -- This is valid when int_data_strobe is high.
    signal int_data_read           : out vme_vec_64_t;

    -- Strobe that indicates new data in int_data_read
    signal int_data_strobe      : out std_logic := c_DATA_CLEAR;

    -- Strobe that indicates that the current value of
    -- int_vme_go have been consumed.
    signal int_go_consumed_strobe : out std_logic := '0';

    -- Strobe that indicates when a BLT decision is needed.
    -- See int_blt_decided and int_blt_continue
    signal int_blt_decision : out std_logic := '0';

    -- Error code.
    -- Consult vme_pkg.ERR_CODE for valid values.
    -- Will be vme_pkg.ERR_CODE.OK if no problems.
    signal int_err_code         : out err_vec_t := c_ERR_OK;    
   
    signal int_addr             : in vme_addr_t;
    signal int_data_write           : in vme_vec_64_t;

    signal int_am_i             : in am_vec_t;
    -- signal int_vme_op           : in VME_OP;
    signal int_vme_write           : in std_logic;
    signal int_vme_go           : in std_logic;


    signal int_blt_decided      : in std_logic;
    signal int_blt_continue     : in std_logic;
    signal int_timeout_n        : in std_logic

    );
end entity;



architecture rtl of vme_data_bus is
  type vme_data_state is (
    IDLE,               -- 0
    DTACK_HIGH_WAIT,    -- 1
    DTACK_LOW_WAIT,     -- 2
    AS_DELAY,           -- 3
    DS_DELAY,           -- 4
    IACK_HIGH_WAIT,     -- 5
    LATCH_DATA,         -- 6
    BLT_READ_WAIT,      -- 7
    BLT_WRITE_WAIT,     -- 8
    IDLE_DELAY,         -- 9
    TIMEOUT,            -- 10
    TIMEOUT_WAIT,       -- 11
    BERR_HIGH_WAIT      -- 12
    );

  type addr_type_t is (
    A16,
    A24,
    A32,
    ADDR_ERR
    );

  type transfer_type_t is (
    SINGLE,             -- 0
    BLT,                -- 1
    MBLT,               -- 2
    TRANSFER_ERR        -- 3
    );

  signal state          : vme_data_state := IDLE;
  signal addr_mode      : addr_type_t;
  signal transfer_mode  : transfer_type_t;
  signal data_placed    : std_logic := '0';

  signal n_wait      : natural range 0 to 8 := 0;
  constant c_N_AS_DELAY  : natural range 1 to 8 :=
    (35 / CLOCK_PERIOD);
  constant c_N_DS_DELAY  : natural range 1 to 8 :=
    (35 / CLOCK_PERIOD);
  constant c_N_DS_SPACING  : natural range 1 to 8 :=
    (35 / CLOCK_PERIOD);  
  constant c_N_DATA_WAIT  : natural range 1 to 8 :=
    (25 / CLOCK_PERIOD);
  constant c_N_TIMEOUT_WAIT  : natural range 1 to 8 :=
    (30 / CLOCK_PERIOD);


  -- Latched signals
  signal l_addr                 : vme_addr_t;
  signal l_rw                   : std_logic;
  signal l_am                   : am_vec_t;
  signal l_addr_mode            : addr_type_t;
  signal l_transfer_mode        : transfer_type_t;

  -- Latched data
  -- If READ_OP it stores the data read from slave.
  -- If WRITE_OP it stores the data to write to slave.
  signal l_data             : std_logic_vector(63 downto 0) := (others => '0');

  signal first_cycle                  : std_logic := '1';

  -- Timeout of operations, in order to never get stuck.
  constant TIMEOUT_CNT_MAX : integer := 255;
  signal timeout_cnt : integer range 0 to 255 := TIMEOUT_CNT_MAX;

  signal last_ds	        : std_logic_vector(1 downto 0);
  signal last_berr              : std_logic;
  
begin

  -- Determine addressing mode
  with int_am_i select addr_mode <=
    A16 when c_AM_A16 | c_AM_A16_LOCK | c_AM_A16_SUP,
    A24 when c_AM_A24_SUP_BLT | c_AM_A24_SUP_MBLT |
    	c_AM_A24_BLT | c_AM_A24_MBLT |
    	c_AM_A24_SUP_PROG | c_AM_A24_SUP_DATA |
	c_AM_A24_PROG | c_AM_A24_DATA |
	c_AM_A24_LOCK, -- In principle correct ADDR mode

    A32 when c_AM_A32_BLT | c_AM_A32_MBLT |
    	c_AM_A32_PROG | c_AM_A32_DATA |
	c_AM_A32_LOCK, -- In principle correct ADDR mode
    ADDR_ERR when others;


  with int_am_i select transfer_mode <=
    SINGLE when c_AM_A32_PROG | c_AM_A32_DATA |
    	        c_AM_A24_SUP_PROG | c_AM_A24_SUP_DATA |
	        c_AM_A24_PROG | c_AM_A24_DATA |
                c_AM_A16 | c_AM_A16_SUP,
    BLT when c_AM_A32_BLT | c_AM_A24_SUP_BLT |
             c_AM_A24_BLT,
    MBLT when c_AM_A32_MBLT | c_AM_A24_SUP_MBLT |
    	     c_AM_A24_MBLT,
    TRANSFER_ERR when others;

  process (clk)
      variable cur_data             : std_logic_vector(63 downto 0) := (others => '0');
  begin
    if (rising_edge(clk)) then

      -- Common delay counter
      if (n_wait /= 0) then
        n_wait <= n_wait - 1;
      end if;
  
      
      case state is
        when IDLE =>
          -- Revert to well defined state.
          vme_addr_oe_n <= c_OE_ON;
          vme_data_oe_n <= c_OE_ON;
          vme_iackout_n_oe_n <= c_OE_OFF;
          vme_addr_dir <= c_PIN_IN;
          vme_am_dir <= c_PIN_IN;
          vme_data_dir <= c_PIN_IN;
          vme_as_n_dir <= c_PIN_IN;
          vme_as_n_o <= '1';
          vme_berr_n_dir <= c_PIN_IN;
          vme_berr_n_o <= '1';
          vme_iack_n_dir <= c_PIN_IN;
          vme_dtack_n_dir <= c_PIN_IN;
          vme_ds_n_dir <= c_PIN_IN;
          vme_ds_n_o <= "11";
          int_data_strobe <= c_DATA_CLEAR;

          -- Munk: Retain error code until starting next cycle
          -- int_err_code <= c_ERR_OK;
          
          n_wait <= 0;
          first_cycle <= '1';
          busy <= '0';

          -- READ requested
          if vme_iack_n_i = '0' then
                state <= IACK_HIGH_WAIT;            
          elsif (int_vme_go = '1') then
            -- Signal that we have seen the GO
            int_go_consumed_strobe <= '1';

            if addr_mode = ADDR_ERR then
              int_err_code <= c_ERR_ADDR_MODE;
              state <= IDLE_DELAY;
            elsif transfer_mode = TRANSFER_ERR then
              int_err_code <= c_ERR_TRANSFER_MODE;
              state <= IDLE_DELAY;
            else                 
              -- Table 2-4 and Table 2-29
              -- A[0] = LWORD*
              -- B(i) = Byte(i)
              --     | A[31-24] A[23-16] A[15-8] A[7-0] D[31-24] D[23-16] D[15-8] D[7-0]
              --   ---------------------------------------------------------------------
              -- D16 |                                                      B(0)   B(1)
              -- D32 |                                    B(0)     B(1)     B(2)   B(3)
              -- D64 |   B(0)     B(1)     B(2)   B(3)    B(4)     B(5)     B(6)   B(7)
              l_addr <= int_addr;              
              l_data <= int_data_write;
              l_am <= int_am_i;
              l_rw <= int_vme_write;
              l_transfer_mode <= transfer_mode;
              l_addr_mode <= addr_mode;
              busy <= '1';
              int_err_code <= c_ERR_OK;
              -- Rule 2.30:
              -- The Master MUST NOT drive AS* low until IACK* has been high

              vme_addr_o <= int_addr;
              vme_addr_dir <= c_PIN_OUT;
              vme_am_o <= int_am_i;
              vme_am_dir <= c_PIN_OUT;

              vme_write_n_o <=  not int_vme_write;
              
              
              vme_iack_n_o <= '1'; -- We pull IACK* high
              vme_iack_n_dir <= c_PIN_OUT;

              -- If data lines are free then place data on them
              -- We also do this in MBLT mode.
              if (--transfer_mode /= MBLT and
                int_vme_write = c_VME_WRITE and
                vme_dtack_n_i = '1')
              then
                vme_data_o <= int_data_write(31 downto 0);
                vme_data_dir <= c_PIN_OUT;
                data_placed <= '1';
              end if;

              n_wait <= c_N_AS_DELAY;
              state <= AS_DELAY;
            end if;
          end if;

        -- Rule 2.30:
        -- The Master MUST NOT drive AS* low until IACK* has been high
        -- and the required lines among A[31..1], AM[5..0], and LWORD*
        -- have been valid for this minimum time.
        when AS_DELAY =>
          if (n_wait = 0) then 
            -- Signal valid address
            vme_as_n_o <= '0';
            vme_as_n_dir <= c_PIN_OUT;
            int_go_consumed_strobe <= '0';

            -- Rule 2.36:
            -- The Master MUST NOT drive DSA* low until it has driven AS* low.

            -- Rule 2.35:
            -- The Master MUST NOT drive DSA* low until both DTACK*
            -- and BERR* are high.

            -- Data lines free.
            if (vme_dtack_n_i & vme_berr_n_i = "11") then
              if (l_rw = c_VME_READ) then
                vme_ds_n_o <= "00";
                vme_ds_n_dir <= c_PIN_OUT;

                -- Wait for slave ACK.
                state <= DTACK_LOW_WAIT;
              else
                if (data_placed = '1') then
                  -- Data already together with addr.
                  -- We have waited enough.
                  vme_ds_n_o <= "00";
                  vme_ds_n_dir <= c_PIN_OUT;
                  data_placed <= '1';

                  -- Wait for slave ACK.
                  state <= DTACK_LOW_WAIT;
                else
                  -- Still in addressing phase.
                  -- We can only place data on D lines
                  vme_data_o <= l_data(31 downto 0);
                  vme_data_dir <= c_PIN_OUT;

                  -- Rule 2.34a
                  -- During write cycles [...] the Master MUST NOT drive DSA*
                  -- low until the required lines among D[31..0] have been
                  -- valid for this minimum time.
                  n_wait <= c_N_DS_DELAY;
                  state <= DS_DELAY;
                end if;              
              end if;
            else
              -- Data lines not free. We must wait.
              state <= DTACK_HIGH_WAIT;
            end if;
          end if;

        -- Data bus occupied. Wait for release.
        when DTACK_HIGH_WAIT =>
          if (vme_dtack_n_i & vme_berr_n_i = "11") then
            if (l_rw = c_VME_READ) then
              -- Read cycle. 
              if (n_wait = 0) then
                vme_ds_n_o <= "00";
                vme_ds_n_dir <= c_PIN_OUT;
                state <= DTACK_LOW_WAIT;
              else
                state <= DS_DELAY;
              end if;              
            else
              -- Write cycle. Place data and wait
              vme_data_o <= l_data(31 downto 0);
              if (l_transfer_mode = MBLT) then
                vme_addr_o <= l_data(63 downto 32);
              end if;
              vme_data_dir <= c_PIN_OUT;

              -- Rule 2.34a
              -- During write cycles [...] the Master MUST NOT drive DSA*
              -- low until the required lines among D[31..0] have been
              -- valid for this minimum time.
              n_wait <= c_N_DS_DELAY;
              state <= DS_DELAY;
            end if;
          end if;

        -- Rule 2.34a
        -- During write cycles [...] the Master MUST NOT drive DSA*
        -- low until the required lines among D[31..0] have been
        -- valid for this minimum time.
        when DS_DELAY =>
          -- Data has been placed. Wait to drive DS.
          if (n_wait = 0) then
              vme_ds_n_o <= "00";
              vme_ds_n_dir <= c_PIN_OUT;
              state <= DTACK_LOW_WAIT;
          end if;

        -- Wait for slave to ack transfer
        when DTACK_LOW_WAIT =>
          -- OBSERVATION 2.48:
          -- The Master is guaranteed that neither DTACK* nor BERR* will go low
          -- until this minimum time after it drives DSA* low.
          -- [30 ns]
          --
          -- Munk: Thus we can only catch BERR* here.
          -- Munk (17/8/2020) : Always catch BERR*.
          --   There might be bad modules or a bug in this code.
            
          if (vme_dtack_n_i = '0') then

            -- RULE 2.40:
            -- During all data transfer cycles, excluding A16, A24 and A32
            -- Read-Modify-Write and Retry cycles, the Master MUST drive A[31..1] and LWORD*
            -- with valid addressing information until it detects the first_cycle falling edge
            -- on DTACK* or BERR*.

            if (l_rw = c_VME_READ) then
              -- Munk: We can thus always flip dir on ADDR pins.
              -- This simplifies MBLT logic
              vme_addr_dir <= c_PIN_IN;
              if l_transfer_mode = MBLT and first_cycle = '1' then
                vme_ds_n_o <= "11";
                n_wait <= c_N_DS_SPACING; -- 40ns cooldown of DS*               
                state <= DTACK_HIGH_WAIT;
              else                
                n_wait <= c_N_DATA_WAIT;
                state <= LATCH_DATA;
              end if;
   
            else
              -- Rescind DS*
              vme_ds_n_o <= "11";
              case l_transfer_mode is
                when SINGLE =>
                  -- We are done. Terminate cycle and IDLE.
                  vme_as_n_o <= '1';
                  state <= IDLE;
                  busy <= '0';
                  int_data_strobe <= c_DATA_PRESENT;
                  int_err_code <= c_ERR_OK;
                when BLT =>
                  -- Per Rule 2.34a there must be 40ns delay
                  -- between DS* transistions. Handle this in next cycle
                  int_blt_decision <= '1';
                  int_data_strobe <= c_DATA_PRESENT;
                  state <= BLT_WRITE_WAIT;
                when MBLT =>
                  if first_cycle = '0' then
                    int_blt_decision <= '1';
                    int_data_strobe <= c_DATA_PRESENT;
                    state <= BLT_WRITE_WAIT;
                  else
                    -- ADDR broadcast. Now write data.
                    n_wait <= c_N_DS_SPACING; -- 40ns cooldown of DS*               
                    state <= DTACK_HIGH_WAIT;
                  end if;                  
                when others =>
                  assert false report "not implemented!";
              end case;              
            end if;
            first_cycle <= '0';
          end if;


        -- OBSERVATION 2.47a:
        -- During read cycles, the Master is guaranteed that D[31..0] will be
        -- valid within 25 nanoseconds after DTACK* goes low. In addition, during
        -- MBLT, A40BLT, and MD32 read cycles, the Master is guaranteed that A[31..1]
        -- and LWORD* will be valid within 25 nanoseconds after DTACK* goes low.
        -- This time does not apply to cycles where the Slave drives BERR* low instead
        -- of DTACK*.          
        when LATCH_DATA =>
          -- Table 2-4 and Table 2-29
          -- A[0] = LWORD*
          -- B(i) = Byte(i)
          -- B(0) is the most significant byte
          --
          --     | A[31-24] A[23-16] A[15-8] A[7-0] D[31-24] D[23-16] D[15-8] D[7-0]
          --   ---------------------------------------------------------------------
          -- D16 |                                                      B(0)   B(1)
          -- D32 |                                    B(0)     B(1)     B(2)   B(3)
          -- D64 |   B(0)     B(1)     B(2)   B(3)    B(4)     B(5)     B(6)   B(7)
          --
          -- Conclusion:
          -- The D lines always carry the least significant bits.
          -- If we run MBLT then the A lines with carry the MSB.
          -- 
          cur_data(31 downto 0) := vme_data_i;
          case l_transfer_mode is
            when SINGLE | BLT =>
              -- l_data(31 downto 0) => vme_data_i;
              cur_data(63 downto 32) := (others => '0');
            when MBLT =>
              -- l_data(31 downto 0) => vme_addr_i;
              cur_data(63 downto 32) := vme_addr_i;
            when others =>
              assert false report "Logic error!";
          end case;
          
          -- Munk: In principle we can have cur_data = l_data,
          -- first time n_wait = 0.
          -- In this case l_data is latched when n_wait = 1.
          -- Howver, according to observation 2.47a, then data is
          -- valid WITHIN 25ns. 
          if (n_wait = 0) then
            -- Latched data stable
            if (cur_data = l_data) then
              -- Slave only maintains data lines while
              -- DS* asserted. They can be deasserted now. 
              vme_ds_n_o <= "11";
              vme_ds_n_dir <= c_PIN_OUT;
              int_data_read <= cur_data;
              int_data_strobe <= c_DATA_PRESENT;

              case l_transfer_mode is
                when SINGLE =>
                  vme_as_n_o <= '1';
                  
                  state <= IDLE;
                  busy <= '0';
                  int_err_code <= c_ERR_OK;
                when BLT | MBLT =>
                  n_wait <= c_N_DS_SPACING;
                  int_blt_decision <= '1';
                  state <= BLT_READ_WAIT;
                when others =>
                  assert false report "Logic error!";
              end case;              
            else -- Unstable data. Try again
              n_wait <= 1;
            end if;
          end if;
          l_data <= cur_data;

        when BLT_WRITE_WAIT =>
          int_data_strobe <= c_DATA_CLEAR;
          if int_blt_decided = '1' then
            int_blt_decision <= '0';
            
            if int_blt_continue = '1' then
              l_data <= int_data_write; -- Latch new data
              state <= DTACK_HIGH_WAIT; -- Wait for slave to rescind DTACK
            else
              -- Terminate cycle
              vme_as_n_o <= '1';
              state <= IDLE;
              busy <= '0';
              int_err_code <= c_ERR_OK;
            end if;
          end if;                    

        when BLT_READ_WAIT =>
          int_data_strobe <= c_DATA_CLEAR;
          if int_blt_decided = '1' then            
            int_blt_decision <= '0';
            if int_blt_continue = '1' then          
              state <= DTACK_HIGH_WAIT;
            else
              -- Block transfer is terminated by AS* high.
              vme_as_n_o <= '1';
              n_wait <= 0;
              state <= IDLE;
              busy <= '0';
              int_err_code <= c_ERR_OK;
            end if;
          end if;
          
        when IACK_HIGH_WAIT =>
          if vme_iack_n_i = '1' then
            state <= IDLE;
          end if;
          -- Note: this state does not assert busy, since we
          -- are not working on behalf of the client.


        -- Delay return to IDLE.          
        when IDLE_DELAY =>
          state <= IDLE;
          busy <= '0';

        when BERR_HIGH_WAIT =>
          --if (last_berr_n = '1' and vme_berr_n_i = '1') then
          if (vme_berr_n_i = '1') then
            state <= IDLE;
          end if;          

        -- Timeout!  Something is preventing the state machine
        -- from completing.  Either an external error (e.g. a
        -- non-responding module), or a bug in this code.

        -- BERR is issued and we stop driving signals.
        when TIMEOUT =>
          vme_berr_n_dir <= c_PIN_OUT;
          vme_berr_n_o <= '0';
          
          vme_ds_n_dir <= c_PIN_IN;
          vme_ds_n_o <= "11";
          
          vme_as_n_dir <= c_PIN_IN;
          vme_as_n_o <= '1';

          vme_dtack_n_dir <= c_PIN_IN;

          -- Data present (error)
          int_data_strobe <= c_DATA_PRESENT;
          int_go_consumed_strobe <= '1';
          int_err_code <= (
            c_ERR_BERR_I => not vme_berr_n_i,
            c_ERR_TIMEOUT_I => '1',
            others => '0'
            );
          busy <= '0';
          -- Attempt to leave the TIMEOUT state
          n_wait <= c_N_TIMEOUT_WAIT;
          state <= TIMEOUT_WAIT;


        -- We stay here and wait 
        when TIMEOUT_WAIT =>
          -- Make sure that also noone else is driving
          -- AS, DS or DTACK before we consider leaving
          -- TIMEOUT state.

          if (vme_ds_n_i = "00" or
              vme_as_n_i = '0' or
              vme_dtack_n_i = '0') then
            -- Someone is still holding a strobe.
            n_wait <= c_N_TIMEOUT_WAIT;
          elsif (n_wait = 0) then
            -- Release BERR line
            vme_berr_n_o <= '1';
            vme_berr_n_dir <= c_PIN_IN;
            state <= BERR_HIGH_WAIT;
          end if;
      end case;

      -- This is after state machine, such that it can force
      -- into TIMEOUT state, no matter what happens.
      -- Also an seemingly indefinate wait in IACK_HIGH_WAIT
      -- will be cut short, such that we report failure to
      -- perform the access to our superiors.

      -- VME spec 2.37:
      -- [...]
      -- The Master, upon completing the first data transfer,
      -- (that is, driving the data strobes high) does not allow
      -- the address strobe to go high. Instead, it repeatedly
      -- drives the data strobe(s) low in response to data transfer
      -- acknowledgments from the Slave

      
      if (last_ds_n /= vme_ds_n_i or -- 
          state    = IDLE or
          state    = IDLE_DELAY or
          state    = TIMEOUT or
          state    = TIMEOUT_WAIT) then
        -- Things are good, or we have fired (no need to fire again).
        timeout_cnt <= TIMEOUT_CNT_MAX;
      elsif ((state /= BERR_HIGH_WAIT and vme_berr_n_i = '0') or
             int_timeout_n = '0')
        state <= TIMEOUT;
      elsif (timeout_cnt = 0) then
        -- We have been operating for too long, timeout.
        state <= TIMEOUT;
      else
        timeout_cnt <= timeout_cnt - 1;
      end if;


      last_ds_n <= vme_ds_n_i;
      last_berr_n <= vme_berr_n_i
    end if;
  end process;


  FormalG : if Formal generate

    -- VHDL helper vars
    signal f_addr               : std_logic_vector(31 downto 0) := (others => 'U');
    signal f_data               : std_logic_vector(63 downto 0) := (others => 'U');        
    signal f_latch_data2        : std_logic_vector(63 downto 0) := (others => 'U');    
    signal f_latch_data         : std_logic_vector(63 downto 0) := (others => 'U');
    signal f_blt_data           : std_logic_vector(63 downto 0) := (others => 'U');    
    signal f_am                 : am_vec_t := (others => 'U');
    signal f_berr_ok            : std_logic := 'U';
    signal f_vme_rw             : std_logic := 'U';
    
    signal f_blt_cycle          : integer := 0;
    
  begin

    process (clk) begin
      if (rising_edge(clk)) then
        if (state = IDLE and int_vme_go = '1') then
          f_addr <= int_addr;
          f_am <= int_am_i;
          f_vme_rw <= int_vme_write;
          f_data <= int_data_write;
        end if;

        if (state = LATCH_DATA) then
          f_latch_data2 <= f_latch_data;
          f_latch_data(31 downto 0) <= vme_data_i;
          f_latch_data(63 downto 32) <= vme_addr_i;
        end if;
        
        
        -- Data latched during BLT continue op
        if (state = BLT_WRITE_WAIT
            and int_blt_decided = '1' and int_blt_continue = '1')
        then
          f_blt_data <= int_data_write;
        end if;

        if (state = IDLE) then
          f_blt_cycle <= 0;
        elsif (state = BLT_WRITE_WAIT) then
          f_blt_cycle <= f_blt_cycle + 1;
        end if;
        

      end if;
    end process;

    -- psl default clock is rising_edge(clk);
    -- psl restrict {{vme_iack_n_i = '1' and vme_berr_n_i = '1'}[+]};

    -- -- Check that client input is latched
    -- psl when_go_addr_is_latched:
    --   assert always {int_vme_go = '1'
    --                  and transfer_mode /= TRANSFER_ERR
    --                  and addr_mode /= ADDR_ERR}
    --     |=> l_addr = f_addr until busy = '0';

    -- psl when_go_am_is_latched:
    --   assert always {int_vme_go = '1'
    --                  and transfer_mode /= TRANSFER_ERR
    --                  and addr_mode /= ADDR_ERR}
    --     |=> l_am = f_am until busy = '0';

    -- psl when_go_rw_is_latched:
    --   assert always {int_vme_go = '1'
    --                  and transfer_mode /= TRANSFER_ERR
    --                  and addr_mode /= ADDR_ERR}
    --     |=> l_rw = f_vme_rw until busy = '0';

    -- -- We only check data next cycle.
    -- -- This might be relatched
    -- psl when_go_data_is_latch:
    --   assert always {state = IDLE and int_vme_go = '1'
    --                  and transfer_mode /= TRANSFER_ERR
    --                  and addr_mode /= ADDR_ERR}
    --     |=> l_data = f_data;    

    -- -- Maintain BUSY until back in IDLE
    -- psl core_is_busy_until_idle:
    --   assert always {state = IDLE; int_vme_go = '1'
    --                  and transfer_mode /= TRANSFER_ERR
    --                  and addr_mode /= ADDR_ERR}
    --     |=> busy = '1' until state = IDLE;

    -- psl when_unsupported_addr_mode_issue_error_code:
    --   assert always {state = IDLE and int_vme_go = '1' and addr_mode = ADDR_ERR}
    --     |=> int_err_code = c_ERR_ADDR_MODE
    --     and state = IDLE_DELAY;

    -- psl when_unsupported_transfer_mode_issue_error_code:
    --   assert always {state = IDLE and int_vme_go = '1'
    --                  and transfer_mode = TRANSFER_ERR
    --                  and addr_mode /= ADDR_ERR}
    --     |=> int_err_code = c_ERR_TRANSFER_MODE
    --     and state = IDLE_DELAY;        

    -- -- If DTACK* is LOW after AS_DELAY,
    -- -- then we must wait for data lines to clear.
    -- psl core_will_not_start_until_dtack_high:
    --   assert always {vme_dtack_n_i = '0' and state = AS_DELAY and n_wait=0}
    --     |=> state = DTACK_HIGH_WAIT until vme_dtack_n_i = '1';

    -- -- We maintain go_consumed high until end of AS_DELAY
    -- psl go_consumed_is_signalled_until_as_delay:
    --   assert always {state = IDLE and int_vme_go = '1'}
    --     |=> int_go_consumed_strobe = '1' until state /= AS_DELAY;

    -- -- Don't fire AS* during AS_DELAY
    -- psl addr_strobe_are_not_fired_during_as_delay:
    --   assert always {state = AS_DELAY}
    --     |=> vme_as_n_o = '1' and vme_as_n_dir = c_PIN_IN
    --     until state /= AS_DELAY;

    -- -- AS* fires after we leave AS_DELAY
    -- psl addr_strobe_are_fired_after_as_delay:
    --   assert always {state = AS_DELAY and n_wait = 0}
    --     |=> vme_as_n_o = '0' and vme_as_n_dir = c_PIN_OUT;

    -- -- AS* fires after we leave AS_DELAY
    -- psl if_dtack_is_asserted_in_as_then_we_wait_until_deasserted:
    --   assert always {state = AS_DELAY and n_wait = 0 and vme_dtack_n_i = '0'}
    --     |=> state = DTACK_HIGH_WAIT and vme_ds_n_o = "11"
    --     until vme_dtack_n_i = '1';    

    -- -- Don't fire DS* during AS_DELAY
    -- psl data_strobes_are_not_fired_during_as_delay:
    --   assert always {state = AS_DELAY}
    --     |=> vme_ds_n_o = "11" and vme_ds_n_dir = c_PIN_IN
    --     until state /= AS_DELAY;

    -- psl data_strobe_are_fired_with_as_when_data_placed:
    --   assert always {vme_dtack_n_i = '1' and
    --                  state = AS_DELAY and l_rw = c_VME_WRITE
    --                  and data_placed = '1' and n_wait = 0}
    --     |=> vme_ds_n_o = "00";

    -- -- If writing and waiting for DTACK* HIGH,
    -- -- then data is placed when satisfied.
    -- psl when_writing_and_dtack_fires_place_data:
    --   assert always {l_transfer_mode = SINGLE
    --                  and l_rw = c_VME_WRITE
    --                  and state = DTACK_HIGH_WAIT; vme_dtack_n_i = '1'}
    --     |=> vme_data_o = l_data(31 downto 0);

    -- -- If IDLE and GO given
    -- -- and data lines are free (DTACK* = 1)
    -- -- and we are writing.
    -- -- Then place low 32 bits immideately 
    -- psl when_writing_and_dtack_is_high_then_data_is_placed:
    --   assert always {int_vme_go = '1' and state = IDLE
    --                  and int_vme_write = c_VME_WRITE and vme_dtack_n_i = '1'
    --                  and int_am_i = c_AM_A24_DATA}
    --     |=> vme_data_o = l_data(31 downto 0)
    --     until state = DTACK_LOW_WAIT or state = IDLE;

    -- -- When writing MBLT the data will be placed on the bus
    -- psl mblt_writing_data_is_placed_on_bus:
    --   assert always {state = DTACK_HIGH_WAIT and l_transfer_mode = MBLT
    --                  and first_cycle = '1' and vme_dtack_n_i = '1'
    --                  and l_rw = c_VME_WRITE}
    --     |=> vme_data_o = l_data(31 downto 0)
    --     and vme_addr_o = l_data(63 downto 32);

    -- -- When writing MBLT the data latched during BLT_WRITE_WAIT
    -- -- is written to both addr and data pins
    -- psl mblt_writing_data_is_placed_on_bus_second_time:
    --   assert always {state = DTACK_HIGH_WAIT and l_transfer_mode = MBLT
    --                  and first_cycle = '0' and vme_dtack_n_i = '1'
    --                  and l_rw = c_VME_WRITE and f_blt_cycle > 0}
    --     |=> vme_data_o = f_blt_data(31 downto 0)
    --     and vme_addr_o = f_blt_data(63 downto 32);            

    -- -- If stopping BLT write transaction,
    -- -- then return to IDLE
    -- psl return_to_idle_if_stopping_blt_write:
    --   assert always {state = BLT_WRITE_WAIT
    --                  and int_blt_decided = '1' and int_blt_continue = '0'}
    --     |=> state = IDLE;

    -- -- If stopping BLT read transaction,
    -- -- then return to IDLE
    -- psl return_to_idle_if_stopping_blt_read:
    --   assert always {state = BLT_READ_WAIT
    --                  and int_blt_decided = '1' and int_blt_continue = '0'}
    --     |=> state = IDLE;

    -- -- When latching 32 or 16 bit data,
    -- -- then low 32 bits are from data lines
    -- -- and high 32 bits are set to 0.
    -- psl data_is_latched_when_stable:
    --   assert always {state = LATCH_DATA and n_wait = 0
    --                  and f_latch_data = f_latch_data2 and l_transfer_mode /= MBLT}
    --     |-> l_data(31 downto 0) = f_latch_data(31 downto 0)
    --     and l_data(63 downto 32) = "00000000000000000000000000000000";

    -- -- When latching 64 bit data,
    -- -- then low 32 bits are from data lines
    -- -- and high 32 bits are from addr lines.    
    -- psl mblt_data_is_latched_when_stable:
    --   assert always {state = LATCH_DATA
    --                  and f_latch_data = f_latch_data2 and l_transfer_mode = MBLT;
    --                  n_wait = 0}
    --     |-> l_data(31 downto 0) = f_latch_data(31 downto 0)
    --     and l_data(63 downto 32) = f_latch_data(63 downto 32); 
    

    -- -- If BLT write is continued,
    -- -- then new data is latched.
    -- psl if_continueing_blt_write_then_latch_new_data:
    --   assert always {state = BLT_WRITE_WAIT
    --                  and int_blt_decided = '1' and int_blt_continue = '1'}
    --     |=> l_data = f_blt_data;    
    

  end generate FormalG;
  
  
end architecture;