vme_bus_arb.vhd

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

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

    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 := c_PIN_IN;
    signal vme_br_n_oe_n	: out std_logic := c_OE_OFF;

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

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

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

    signal vme_bclr_n_i         : in std_logic;
    signal vme_bclr_n_o         : out std_logic := '1';
    signal vme_bclr_n_dir       : out std_logic := c_PIN_IN

    );
end entity;



architecture rtl of vme_bus_arb is
  type vme_bus_arb_state is (
    IDLE,               -- 0
    BBSY_ASSERT_WAIT,   -- 1
    BBSY_DEASSERT_WAIT, -- 2
    BUS_GRANTED,        -- 3
    FIRE_BUS_GRANT,     -- 4
    COOLDOWN            -- 5
    );

  signal state                  : vme_bus_arb_state := IDLE;
  signal n_bbsy_high            : natural range 0 to 4 := 0;
  signal n_wait                 : natural range 0 to 32 := 0;
  signal granted                : natural range 0 to 3 := 0;
  signal requested              : natural range 0 to 3 := 0;

  constant c_N_BBSY_HIGH        : natural range 1 to 8 :=
    (40 / CLOCK_PERIOD);
  constant c_BBSY_TIMEOUT        : natural range 0 to 32 := 32;  
begin

    vme_br_n_dir        <= c_PIN_IN;
    vme_br_n_oe_n	<= c_OE_ON;
    vme_bgin_n_oe_n	<= c_OE_ON;
    vme_bgout_n_oe_n	<= c_OE_ON;
    vme_bbsy_n_dir      <= c_PIN_IN;
    vme_bclr_n_dir      <= c_PIN_OUT;
  
    process (clk)
      variable req : natural range 0 to 3;
    begin
      if (rising_edge(clk)) then
        if n_wait /= 0 then
          n_wait <= n_wait - 1;
        end if;

        case state is
          when IDLE =>
            vme_bgout_n_o	<= (others => '1');
            vme_bclr_n_o        <= '1';

            if vme_br_n_i /= "1111" then
              state <= FIRE_BUS_GRANT;
            else
              state <= IDLE;
            end if;

          when BBSY_ASSERT_WAIT =>
            if n_wait = 0 then
              state <= IDLE;
            elsif vme_bbsy_n_i = '0' then
              state <= BUS_GRANTED;
            end if;
            
          when BUS_GRANTED =>
            vme_bgout_n_o <= "1111";            
            if (vme_bbsy_n_i = '1') then
              state <= COOLDOWN;
              n_wait <= c_N_BBSY_HIGH;
            else

              if vme_br_n_i /= "1111" then

                -- Determine req priority
                if vme_br_n_i(3) = '0' then
                  req := 3;
                elsif vme_br_n_i(2) = '0' then
                  req := 2;
                elsif vme_br_n_i(1) = '0' then
                  req := 1;
                elsif vme_br_n_i(0) = '0' then
                  req := 0;
                end if;
                requested <= req;
                
                -- If higher or equal => req granted
                if req >= granted then
                  vme_bclr_n_o <= '0';
                  n_bbsy_high <= 0;
                  state <= BBSY_DEASSERT_WAIT;
                else
                  vme_bclr_n_o <= '1';
                end if;
                
              end if;
            end if;
        

          when BBSY_DEASSERT_WAIT =>
            if vme_bbsy_n_i = '1' then
              if n_bbsy_high = c_N_BBSY_HIGH then
                state <= FIRE_BUS_GRANT;
              else
                n_bbsy_high <= n_bbsy_high + 1;
              end if;
            else
              n_bbsy_high <= 0;
            end if;

          when FIRE_BUS_GRANT =>
            vme_bgout_n_o <= (others => '1');
            if vme_br_n_i(3) = '0' then
              vme_bgout_n_o(3) <= '0';
              granted <= 3;
            elsif vme_br_n_i(2) = '0' then
              vme_bgout_n_o(2) <= '0';
              granted <= 2;
            elsif vme_br_n_i(1) = '0' then
              vme_bgout_n_o(1) <= '0';
              granted <= 1;
            elsif vme_br_n_i(0) = '0' then
              vme_bgout_n_o(0) <= '0';
              granted <= 0;
            end if;
            state <= BBSY_ASSERT_WAIT;
            n_wait <= c_BBSY_TIMEOUT;

          when COOLDOWN =>
            if n_wait = 0 then
              state <= IDLE;
            end if;

        end case;      
      end if;
    end process;


  FormalG : if Formal generate    
  begin

    process (clk) begin
      if (rising_edge(clk)) then
        null;
      end if;
    end process;

    -- psl default clock is rising_edge(clk);

    stay_in_idle_until_br_received:    
    assert always (state = IDLE and vme_br_n_i = "1111")
      |=> state = IDLE until vme_br_n_i /= "1111";
    
    assert always (state = IDLE and vme_br_n_i /= "1111")
      |=> state = FIRE_BUS_GRANT;

    if_single_br_on_0_received_accept_it:
    assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1110")
      |=> vme_bgout_n_o = "1110";

    if_single_br_on_1_received_accept_it:
    assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1101")
      |=> vme_bgout_n_o = "1101";

    if_single_br_on_2_received_accept_it:
    assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1011")
      |=> vme_bgout_n_o = "1011";    

    if_single_br_on_3_received_accept_it:
    assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "0111")
      |=> vme_bgout_n_o = "0111";

    if_br_received_on_both_3_and_0_pick_3:
    assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "0110")
      |=> vme_bgout_n_o = "0111";

    if_br_received_then_next_state_is_bbsy_wait:    
    assert always (state = FIRE_BUS_GRANT and vme_br_n_i /= "1111")
      |=> state = BBSY_ASSERT_WAIT;

    when_waiting_for_bbsy_wait_until_bbsy_received:    
    assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '1')
      |=> state = BBSY_ASSERT_WAIT until vme_bbsy_n_i = '0' or n_wait = 0;

    when_waiting_for_bbsy_time_out_returns_to_idle:    
    assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '1' and n_wait = 0)
      |=> state = IDLE;

    when_waiting_for_bbsy_and_it_assert_then_go_to_bus_granted:    
    assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '0' and n_wait > 0)
      |=> state = BUS_GRANTED;

    bus_granted_rescind_bgout:
    assert always (state = BUS_GRANTED)
      |=> vme_bgout_n_o = "1111";

    if_bus_grant_0_and_req_on_1_then_bus_clear:
      assert always (state = BUS_GRANTED and granted = 0
                     and vme_br_n_i = "1101" and vme_bbsy_n_i = '0')
      |=> vme_bclr_n_o = '0';

    if_bus_granted_to_1_then_requested_set_to_1:
      assert always (state = BUS_GRANTED and granted = 0
                     and vme_br_n_i = "1101"  and vme_bbsy_n_i = '0')
      |=> requested = 1;    

    if_bus_grant_0_and_req_on_0_then_bus_clear:
      assert always (state = BUS_GRANTED and granted = 0
                     and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
      |=> vme_bclr_n_o = '0';

    if_bus_grant_1_and_req_on_0_then_no_clear:
      assert always (state = BUS_GRANTED and granted = 1
                     and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
      |=> vme_bclr_n_o = '1';

    if_bus_grant_3_and_req_on_3_then_bus_clear:
      assert always (state = BUS_GRANTED and granted = 3
                     and vme_br_n_i = "0111"  and vme_bbsy_n_i = '0')
      |=> vme_bclr_n_o = '0' and state = BBSY_DEASSERT_WAIT;

    remain_in_bbsy_deassert_atleast_4_cycles:
    assert always (state = BBSY_DEASSERT_WAIT and n_bbsy_high = 0)
      |=> state = BBSY_DEASSERT_WAIT until n_bbsy_high = c_N_BBSY_HIGH;

    if_bus_willingly_released_go_to_cooldown:
    assert always (state = BUS_GRANTED and vme_bbsy_n_i = '1')
      |=> state = COOLDOWN and n_wait = c_N_BBSY_HIGH;

    when_in_cool_down_stay_n_wait_cycles:
    assert always (state = COOLDOWN)
      |=> state = COOLDOWN until n_wait = 0;

    move_from_cooldown_to_idle:
    assert always (state = COOLDOWN and n_wait = 0)
      |=> state = IDLE;        

  end generate FormalG;
  
  
end architecture;