vme_cli_arb.vhd 14.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
library ieee;
use ieee.std_logic_1164.all;
use work.vme_pkg.all;

-- Multiplex signals between the VME core and two clients.
--
-- Each client sees signals such as if it was the only
-- client connected to the core.  (With the exception that it
-- may take a longer time before a 'go' request starts
-- to be processed).

entity vme_cli_arb is
13
14
15
16
  generic (
    -- To synth formal verification
    formal : boolean := true
  );
17
18
19
20
21
22
23
24
25
26
27
28
  port (
    signal clk      : in std_logic;

    -- Signals to/from the first client.
    -- For documentation on the signal purposes, see vme_bus.vhd.

    signal p1_busy                 : out std_logic := '0';

    signal p1_int_data_o           : out vme_vec_64_t;
    signal p1_int_data_strobe      : out std_logic := c_DATA_CLEAR;
    signal p1_int_go_consumed_strobe : out std_logic := '0';
    signal p1_int_blt_decision_strobe : out std_logic := '0';
Michael Munch's avatar
Michael Munch committed
29
    signal p1_int_err_code         : out err_vec_t := C_ERR_OK;
30

31
32
33
34
35
36
37
    signal p1_int_addr             : in vme_addr_t;
    signal p1_int_data_i           : in vme_vec_64_t;
    signal p1_int_am_i             : in am_vec_t;
    signal p1_int_vme_rw           : in std_logic;
    signal p1_int_vme_go           : in std_logic;

    signal p1_int_blt_decided      : in std_logic;
38
    signal p1_int_blt_continue     : in std_logic;
39
40
41
42

    signal p1_int_berr_ok          : in std_logic;

    -- Signals to/from the second client.
43

44
45
46
47
48
49
    signal p2_busy                 : out std_logic := '0';

    signal p2_int_data_o           : out vme_vec_64_t;
    signal p2_int_data_strobe      : out std_logic := c_DATA_CLEAR;
    signal p2_int_go_consumed_strobe : out std_logic := '0';
    signal p2_int_blt_decision_strobe : out std_logic := '0';
Michael Munch's avatar
Michael Munch committed
50
    signal p2_int_err_code         : out err_vec_t := C_ERR_OK;
51

52
53
54
55
56
57
58
    signal p2_int_addr             : in vme_addr_t;
    signal p2_int_data_i           : in vme_vec_64_t;
    signal p2_int_am_i             : in am_vec_t;
    signal p2_int_vme_rw           : in std_logic;
    signal p2_int_vme_go           : in std_logic;

    signal p2_int_blt_decided      : in std_logic;
59
    signal p2_int_blt_continue     : in std_logic;
60
61
62
63
64
65
66
67
68
69
70
71

    signal p2_int_berr_ok          : in std_logic;

    -- Signals to/from the VME core.
    -- Directions inverted relative to the core.

    signal vc_busy                 : in std_logic := '0';

    signal vc_int_data_o           : in vme_vec_64_t;
    signal vc_int_data_strobe      : in std_logic := c_DATA_CLEAR;
    signal vc_int_go_consumed_strobe : in std_logic := '0';
    signal vc_int_blt_decision_strobe : in std_logic := '0';
Michael Munch's avatar
Michael Munch committed
72
    signal vc_int_err_code         : in err_vec_t := C_ERR_OK;
73

74
75
76
77
78
79
80
    signal vc_int_addr             : out vme_addr_t;
    signal vc_int_data_i           : out vme_vec_64_t;
    signal vc_int_am_i             : out am_vec_t;
    signal vc_int_vme_rw           : out std_logic;
    signal vc_int_vme_go           : out std_logic;

    signal vc_int_blt_decided      : out std_logic;
81
    signal vc_int_blt_continue     : out std_logic;
82

Håkan Johansson's avatar
Håkan Johansson committed
83
    signal vc_int_berr_ok          : out std_logic
84

Håkan Johansson's avatar
Håkan Johansson committed
85
86
--    -- Dropped signals (since they cannot be multiplexed /
--    -- span multiple access cycles).
87

Håkan Johansson's avatar
Håkan Johansson committed
88
89
--    signal stop                 : in std_logic;
--    signal int_err_clear        : in std_logic;
90

Håkan Johansson's avatar
Håkan Johansson committed
91
--    signal int_data_ack : in std_logic;
92

Håkan Johansson's avatar
Håkan Johansson committed
93
--    -- Changed behaviour:
94

Håkan Johansson's avatar
Håkan Johansson committed
95
96
--    -- Single-cycle strobe:
--    signal int_data_strobe      : out std_logic := c_DATA_CLEAR;
97

98

99
100
101
102
103
104
105
    );
end entity;



architecture rtl of vme_cli_arb is

Michael Munch's avatar
Michael Munch committed
106
107
108
  -- signal state          : vme_data_state := STOPPED;
  -- signal addr_mode      : addr_type_t;
  -- signal transfer_mode  : transfer_type_t;
109
110
111
112
113



  -- In case we are not busy, which client would we like to
  -- make active (if any).
Michael Munch's avatar
Michael Munch committed
114
  signal cnt            : integer range 0 to 256:= 0;
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
  signal want_1         : boolean;
  signal want_2         : boolean;

  -- Who do we start?
  signal start_1         : boolean;
  signal start_2         : boolean;

  -- Who is live, i.e. is active, or activated this cycle.
  signal live_1         : boolean;
  signal live_2         : boolean;

  -- Who is currently live.
  signal active_1       : boolean := false;
  signal active_2       : boolean := false;

  -- Who will we prefer when we can take the next client, i.e. are
  -- no longer busy?
Michael Munch's avatar
Michael Munch committed
132
133
  signal prefer_1       : boolean := false;

134
135
  signal p1_int_data_o_latched   : vme_vec_64_t := (others => '0');
  signal p2_int_data_o_latched   : vme_vec_64_t := (others => '0');
136

Michael Munch's avatar
Michael Munch committed
137
138
  signal p1_int_err_code_latched : err_vec_t := C_ERR_OK;
  signal p2_int_err_code_latched : err_vec_t := C_ERR_OK;
139
140
begin

Michael Munch's avatar
Michael Munch committed
141
142
  want_1 <= (p1_int_vme_go = '1' and p2_int_vme_go  = '0') or (p1_int_vme_go = '1' and     prefer_1);
  want_2 <= (p2_int_vme_go = '1' and p1_int_vme_go  = '0') or (p2_int_vme_go = '1' and not prefer_1);
143

Michael Munch's avatar
Michael Munch committed
144
145
  start_1 <= vc_busy = '0' and want_1;
  start_2 <= vc_busy = '0' and want_2;
146
147
148

  -- We kill the live assignment as soon as busy is removed.
  -- (Not really needed.)
Michael Munch's avatar
Michael Munch committed
149
150
  live_1 <= (active_1 and vc_busy = '1') or start_1;
  live_2 <= (active_2 and vc_busy = '1') or start_2;
151

152
153
154
155
  process (clk)
  begin
    if (rising_edge(clk)) then

Michael Munch's avatar
Michael Munch committed
156
      cnt <= cnt + 1;
157

Michael Munch's avatar
Michael Munch committed
158
      if (vc_busy = '0') then
159
160
161
162
163
164
165
166
167
168
169
170
171
172
        active_1 <= false;
        active_2 <= false;
      end if;
      -- These assignments may overwrite the above, if we take another
      -- client directly.
      if (start_1) then
        active_1 <= true;
        prefer_1 <= false;
      end if;
      if (start_2) then
        active_2 <= true;
        prefer_1 <= true;
      end if;

173
174
      -- We select on active instead of live, since active is cheaper (comes
      -- directly from a flip-flop, instead of logic), and
175
      -- vc_int_data_strobe will not come on the first cycle.
Michael Munch's avatar
Michael Munch committed
176
      if (active_1 and vc_int_data_strobe = '1') then
177
178
179
        p1_int_data_o_latched   <= vc_int_data_o;
        p1_int_err_code_latched <= vc_int_err_code;
      end if;
Michael Munch's avatar
Michael Munch committed
180
      if (active_2 and vc_int_data_strobe = '1') then
181
182
183
184
        p2_int_data_o_latched   <= vc_int_data_o;
        p2_int_err_code_latched <= vc_int_err_code;
      end if;

185
186
187
188
189
    end if;
  end process;


  -- Signals to the VME core are taken from the live client:
190

191
192
193
  -- If no client is live, we (arbitrarily) take the signals from
  -- client 2.  This does not matter, since the VME core will
  -- only react to anything if the 'go' signal is given.
194

Michael Munch's avatar
Michael Munch committed
195
196
197
198
199
200
201
202
  vc_int_addr         <= p1_int_addr          when live_1 else p2_int_addr;
  vc_int_data_i       <= p1_int_data_i        when live_1 else p2_int_data_i;
  vc_int_am_i         <= p1_int_am_i          when live_1 else p2_int_am_i;
  vc_int_vme_rw       <= p1_int_vme_rw        when live_1 else p2_int_vme_rw;
  vc_int_vme_go       <= p1_int_vme_go        when live_1 else p2_int_vme_go;
  vc_int_blt_decided  <= p1_int_blt_decided   when live_1 else p2_int_blt_decided;
  vc_int_blt_continue <= p1_int_blt_continue  when live_1 else p2_int_blt_continue;
  vc_int_berr_ok      <= p1_int_berr_ok       when live_1 else p2_int_berr_ok;
203
204
205

  -- Signals to the clients from the VME core:

206
207
208
  -- TODO: All the selects below could use active_1 / active_2 instead
  -- of live_1 / live_2, since the signals from the VME core
  -- will not happen on the first cycle we are active!
209

210
211
  -- Data is passed directly through on the cycle they have been latched.
  -- Otherwise, take the latched value:
Michael Munch's avatar
Michael Munch committed
212
  p1_int_data_o <= vc_int_data_o when (live_1 and vc_int_data_strobe = '1') else
213
                   p1_int_data_o_latched;
Michael Munch's avatar
Michael Munch committed
214
  p2_int_data_o <= vc_int_data_o when (live_2 and vc_int_data_strobe = '1') else
215
216
                   p2_int_data_o_latched;
  -- The error code follows the data.
Michael Munch's avatar
Michael Munch committed
217
  p1_int_err_code <= vc_int_err_code when (live_1 and vc_int_data_strobe = '1') else
218
                     p1_int_err_code_latched;
Michael Munch's avatar
Michael Munch committed
219
  p2_int_err_code <= vc_int_err_code when (live_2 and vc_int_data_strobe = '1') else
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
                     p2_int_err_code_latched;

  -- The strobes always go to the live client.
  p1_int_data_strobe <= vc_int_data_strobe when live_1 else '0';
  p2_int_data_strobe <= vc_int_data_strobe when live_2 else '0';

  p1_int_go_consumed_strobe <= vc_int_go_consumed_strobe when live_1 else '0';
  p2_int_go_consumed_strobe <= vc_int_go_consumed_strobe when live_2 else '0';

  p1_int_blt_decision_strobe <= vc_int_blt_decision_strobe when live_1 else '0';
  p2_int_blt_decision_strobe <= vc_int_blt_decision_strobe when live_2 else '0';

  -- The busy of a client is simply while it is live.
  -- This actually means that we will report busy some cycles
  -- early.  (But the clients are not likely to use this signal...)
235
236
  -- p1_busy <= '1' when live_1 else '0';
  -- p2_busy <= '1' when live_2 else '0';
237

238
239
240
  p1_busy <= '1' when active_1 else '0';
  p2_busy <= '1' when active_2 else '0';
  
241
242
243
244
  FormalG : if Formal generate

    -- VHDL helper vars
    signal l_data       : vme_vec_64_t := (others => '0');
Michael Munch's avatar
Michael Munch committed
245
    signal l_err_code   : err_vec_t := C_ERR_OK;
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
    
  begin

    -- *_latched output will lack input by one clock cycle.
    -- GHDL does not have prev() operator,
    -- so latch things here for comparison.
    process (clk)
    begin
      if (rising_edge(clk)) then
        l_data <= vc_int_data_o;
        l_err_code <= vc_int_err_code;
      end if;
    end process;
    
    
Michael Munch's avatar
Michael Munch committed
261
    -- psl default clock is rising_edge(clk);
262

Michael Munch's avatar
Michael Munch committed
263
264
265
266
    -- -- Two clients may not be active at the same time
    -- psl not_two_live:       assert always not (live_1 and live_2);
    -- psl not_two_active:     assert always not (active_1 and active_2);
    -- psl not_two_busy:       assert not (p1_busy and p2_busy);
267

Michael Munch's avatar
Michael Munch committed
268
269
270
    -- -- Don't start clients when VME core is busy
    -- psl busy_dont_start_1:  assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
    -- psl busy_dont_start_2:  assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
271

Michael Munch's avatar
Michael Munch committed
272
273
274
    -- -- When we have started client 1 then prefer 2 until it runs
    -- psl if_start_1_pref_2:  assert always {start_1} |=> not prefer_1 until start_2;
    -- psl if_start_2_pref_1:  assert always {start_2} |=>     prefer_1 until start_1;
Michael Munch's avatar
Michael Munch committed
275

276

Michael Munch's avatar
Michael Munch committed
277
278
    -- -- If both clients request access then we pick our favourite
    -- psl pick_pref_client_1: assert always
Michael Munch's avatar
Michael Munch committed
279
    --   {p1_int_vme_go = '1' and p2_int_vme_go = '1' and not prefer_1 and vc_busy = '0'}
Michael Munch's avatar
Michael Munch committed
280
    --   |=> start_2 until active_2;
281
    
Michael Munch's avatar
Michael Munch committed
282
    -- psl pick_pref_client_2: assert always
Michael Munch's avatar
Michael Munch committed
283
    --   {p1_int_vme_go = '1' and p2_int_vme_go = '1' and     prefer_1 and vc_busy = '0'}
Michael Munch's avatar
Michael Munch committed
284
285
286
287
288
289
290
291
292
293
294
295
296
    --   |=> start_1 until active_1;

    -- -- While client is live it data output tracks live data
    -- psl live_track_1:
    --   assert always {active_1; vc_int_data_strobe = '1'}
    --     |=> p1_int_data_o = vc_int_data_o
    --     until vc_int_data_strobe = '0' or not live_1;

    -- psl live_track_2:
    --   assert always {active_2; vc_int_data_strobe = '1'}
    --     |=> p2_int_data_o = vc_int_data_o
    --     until vc_int_data_strobe = '0' or not live_2;

Michael Munch's avatar
Michael Munch committed
297
298
    -- -- If we sent p1_int_vme_go then the VME core will eventually receive it
    -- psl p1_vme_addr:        assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
299
    --   |=> eventually! vc_int_addr = p1_int_addr ;
Michael Munch's avatar
Michael Munch committed
300
    -- psl p1_vme_data_i:      assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
301
    --   |=> eventually! vc_int_data_i = p1_int_data_i ;
Michael Munch's avatar
Michael Munch committed
302
    -- psl p1_vme_am_i:        assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
303
    --   |=> eventually! vc_int_am_i = p1_int_am_i ;
Michael Munch's avatar
Michael Munch committed
304
    -- psl p1_vme_rw:          assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
305
    --   |=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
306
    -- psl p1_vme_go:          assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
307
    --   |=> eventually! vc_int_vme_go = p1_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
308
    -- psl p1_vme_blt_deci:    assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
309
    --   |=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
310
    -- psl p1_vme_blt_cont:    assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
311
    --   |=> eventually! vc_int_blt_continue = p1_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
312
    -- psl p1_vme_berr_ok:     assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
313
314
    --   |=> eventually! vc_int_berr_ok = p1_int_berr_ok ;

Michael Munch's avatar
Michael Munch committed
315
316
    -- -- If we sent p2_int_vme_go then the VME core will eventually receive it
    -- psl p2_vme_addr:        assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
317
    --   |=> eventually! vc_int_addr = p2_int_addr ;
Michael Munch's avatar
Michael Munch committed
318
    -- psl p2_vme_data_i:      assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
319
    --   |=> eventually! vc_int_data_i = p2_int_data_i ;
Michael Munch's avatar
Michael Munch committed
320
    -- psl p2_vme_am_i:        assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
321
    --   |=> eventually! vc_int_am_i = p2_int_am_i ;
Michael Munch's avatar
Michael Munch committed
322
    -- psl p2_vme_rw:          assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
323
    --   |=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
324
    -- psl p2_vme_go:          assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
325
    --   |=> eventually! vc_int_vme_go = p2_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
326
    -- psl p2_vme_blt_deci:    assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
327
    --   |=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
328
    -- psl p2_vme_blt_cont:    assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
329
    --   |=> eventually! vc_int_blt_continue = p2_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
330
    -- psl p2_vme_berr_ok:     assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
    --   |=> eventually! vc_int_berr_ok = p2_int_berr_ok ;

    -- -- Data strobes are routed to live client
    -- psl p1_get_d_strobe:     assert always {live_1}
    --   |=> p1_int_data_strobe = vc_int_data_strobe until not live_1;

    -- psl p2_get_d_strobe:     assert always {live_2}
    --   |=> p2_int_data_strobe = vc_int_data_strobe until not live_2;

    -- -- Go strobes are routed to live client
    -- psl p1_get_go_strobe:     assert always {live_1}
    --   |=> p1_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_1;

    -- psl p2_get_go_strobe:     assert always {live_2}
    --   |=> p2_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_2;    

    -- -- BLT decision strobes are routed to live client
    -- psl p1_get_blt_strobe:     assert always {live_1}
    --   |=> p1_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_1;

    -- psl p2_get_blt_strobe:     assert always {live_2}
    --   |=> p2_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_2;    
353
    
Michael Munch's avatar
Michael Munch committed
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
    -- -- Latched data tracks input while active and strobed
    -- psl p1_tracks_data:     assert always
    --   {active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
    --   |=> p1_int_data_o_latched = l_data
    --   until vc_int_data_strobe = '0' or not active_1;

    -- psl p2_tracks_data:     assert always
    --   {active_2 and vc_busy = '1' and vc_int_data_strobe = '1'}
    --   |=> p2_int_data_o_latched = l_data
    --   until vc_int_data_strobe = '0' or not active_2;

    -- -- Latched error tracks input while active and strobed
    -- psl p1_tracks_err:     assert always
    --   {active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
    --   |=> p1_int_err_code_latched = l_err_code
    --   until vc_int_data_strobe = '0' or not active_1;

    -- psl p2_tracks_err:     assert always
    --   {active_2 and vc_busy = '1' and vc_int_data_strobe = '1'}
    --   |=> p2_int_err_code_latched = l_err_code
    --   until vc_int_data_strobe = '0' or not active_2;    
375
  end generate FormalG;
376
377
378
379
end architecture;