vme_bus_arb.vhd 8.34 KB
Newer Older
Michael Munch's avatar
Michael Munch committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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
Michael Munch's avatar
Michael Munch committed
45
46
    FIRE_BUS_GRANT,     -- 4
    COOLDOWN            -- 5
Michael Munch's avatar
Michael Munch committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
    );

  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 =>
Michael Munch's avatar
Michael Munch committed
94
95
96
97
98
            vme_bgout_n_o <= "1111";            
            if (vme_bbsy_n_i = '1') then
              state <= COOLDOWN;
              n_wait <= c_N_BBSY_HIGH;
            else
Michael Munch's avatar
Michael Munch committed
99

Michael Munch's avatar
Michael Munch committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
              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;
                
Michael Munch's avatar
Michael Munch committed
123
124
              end if;
            end if;
Michael Munch's avatar
Michael Munch committed
125
        
Michael Munch's avatar
Michael Munch committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155

          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;

Michael Munch's avatar
Michael Munch committed
156
157
158
159
160
          when COOLDOWN =>
            if n_wait = 0 then
              state <= IDLE;
            end if;

Michael Munch's avatar
Michael Munch committed
161
162
163
164
165
166
167
168
169
170
171
172
173
174
        end case;      
      end if;
    end process;


  FormalG : if Formal generate    
  begin

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

Michael Munch's avatar
Michael Munch committed
175
    -- psl default clock is rising_edge(clk);
Michael Munch's avatar
Michael Munch committed
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224

    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:
Michael Munch's avatar
Michael Munch committed
225
226
      assert always (state = BUS_GRANTED and granted = 0
                     and vme_br_n_i = "1101" and vme_bbsy_n_i = '0')
Michael Munch's avatar
Michael Munch committed
227
228
229
      |=> vme_bclr_n_o = '0';

    if_bus_granted_to_1_then_requested_set_to_1:
Michael Munch's avatar
Michael Munch committed
230
231
      assert always (state = BUS_GRANTED and granted = 0
                     and vme_br_n_i = "1101"  and vme_bbsy_n_i = '0')
Michael Munch's avatar
Michael Munch committed
232
233
234
      |=> requested = 1;    

    if_bus_grant_0_and_req_on_0_then_bus_clear:
Michael Munch's avatar
Michael Munch committed
235
236
      assert always (state = BUS_GRANTED and granted = 0
                     and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
Michael Munch's avatar
Michael Munch committed
237
238
239
      |=> vme_bclr_n_o = '0';

    if_bus_grant_1_and_req_on_0_then_no_clear:
Michael Munch's avatar
Michael Munch committed
240
241
      assert always (state = BUS_GRANTED and granted = 1
                     and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
Michael Munch's avatar
Michael Munch committed
242
243
244
      |=> vme_bclr_n_o = '1';

    if_bus_grant_3_and_req_on_3_then_bus_clear:
Michael Munch's avatar
Michael Munch committed
245
246
      assert always (state = BUS_GRANTED and granted = 3
                     and vme_br_n_i = "0111"  and vme_bbsy_n_i = '0')
Michael Munch's avatar
Michael Munch committed
247
248
249
250
251
252
      |=> 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;

Michael Munch's avatar
Michael Munch committed
253
254
255
256
257
258
259
260
261
262
263
264
    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;        

Michael Munch's avatar
Michael Munch committed
265
266
267
268
269
270
271
  end generate FormalG;
  
  
end architecture;