vme_cli_arb.vhd 14.5 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

    signal p1_int_berr_ok          : in std_logic;

Michael Munch's avatar
Michael Munch committed
42
43
    signal p1_go                  : in std_logic;

44
    -- Signals to/from the second client.
45

46
47
48
49
50
51
    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
52
    signal p2_int_err_code         : out err_vec_t := C_ERR_OK;
53

54
55
56
57
58
59
60
    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;
61
    signal p2_int_blt_continue     : in std_logic;
62
63
64

    signal p2_int_berr_ok          : in std_logic;

65
    signal p2_go                  : in std_logic;
Michael Munch's avatar
Michael Munch committed
66

67
68
69
70
71
72
73
74
75
    -- 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
76
    signal vc_int_err_code         : in err_vec_t := C_ERR_OK;
77

78
79
80
81
82
83
84
    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;
85
    signal vc_int_blt_continue     : out std_logic;
86

Håkan Johansson's avatar
Håkan Johansson committed
87
    signal vc_int_berr_ok          : out std_logic
88

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

Håkan Johansson's avatar
Håkan Johansson committed
92
93
--    signal stop                 : in std_logic;
--    signal int_err_clear        : in std_logic;
94

Håkan Johansson's avatar
Håkan Johansson committed
95
--    signal int_data_ack : in std_logic;
96

Håkan Johansson's avatar
Håkan Johansson committed
97
--    -- Changed behaviour:
98

Håkan Johansson's avatar
Håkan Johansson committed
99
100
--    -- Single-cycle strobe:
--    signal int_data_strobe      : out std_logic := c_DATA_CLEAR;
101

102

103
104
105
106
107
108
109
    );
end entity;



architecture rtl of vme_cli_arb is

Michael Munch's avatar
Michael Munch committed
110
111
112
  -- signal state          : vme_data_state := STOPPED;
  -- signal addr_mode      : addr_type_t;
  -- signal transfer_mode  : transfer_type_t;
113
114
115
116
117



  -- In case we are not busy, which client would we like to
  -- make active (if any).
Michael Munch's avatar
Michael Munch committed
118
  signal cnt            : integer range 0 to 256:= 0;
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
  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
136
137
  signal prefer_1       : boolean := false;

138
139
  signal p1_int_data_o_latched   : vme_vec_64_t := (others => '0');
  signal p2_int_data_o_latched   : vme_vec_64_t := (others => '0');
140

Michael Munch's avatar
Michael Munch committed
141
142
  signal p1_int_err_code_latched : err_vec_t := C_ERR_OK;
  signal p2_int_err_code_latched : err_vec_t := C_ERR_OK;
143
144
begin

Michael Munch's avatar
Michael Munch committed
145
146
  want_1 <= (p1_go = '1' and p2_go  = '0') or (p1_go = '1' and     prefer_1);
  want_2 <= (p2_go = '1' and p1_go  = '0') or (p2_go = '1' and not prefer_1);
147

Michael Munch's avatar
Michael Munch committed
148
149
  start_1 <= vc_busy = '0' and want_1;
  start_2 <= vc_busy = '0' and want_2;
150
151
152

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

156
157
158
159
  process (clk)
  begin
    if (rising_edge(clk)) then

Michael Munch's avatar
Michael Munch committed
160
      cnt <= cnt + 1;
161

Michael Munch's avatar
Michael Munch committed
162
      if (vc_busy = '0') then
163
164
165
166
167
168
169
170
171
172
173
174
175
176
        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;

177
178
      -- We select on active instead of live, since active is cheaper (comes
      -- directly from a flip-flop, instead of logic), and
179
      -- vc_int_data_strobe will not come on the first cycle.
Michael Munch's avatar
Michael Munch committed
180
      if (active_1 and vc_int_data_strobe = '1') then
181
182
183
        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
184
      if (active_2 and vc_int_data_strobe = '1') then
185
186
187
188
        p2_int_data_o_latched   <= vc_int_data_o;
        p2_int_err_code_latched <= vc_int_err_code;
      end if;

189
190
191
192
193
    end if;
  end process;


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

195
196
197
  -- 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.
198

Michael Munch's avatar
Michael Munch committed
199
200
201
202
203
204
205
206
  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;
207
208
209

  -- Signals to the clients from the VME core:

210
211
212
  -- 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!
213

214
215
  -- Data is passed directly through on the cycle they have been latched.
  -- Otherwise, take the latched value:
Michael Munch's avatar
Michael Munch committed
216
  p1_int_data_o <= vc_int_data_o when (live_1 and vc_int_data_strobe = '1') else
217
                   p1_int_data_o_latched;
Michael Munch's avatar
Michael Munch committed
218
  p2_int_data_o <= vc_int_data_o when (live_2 and vc_int_data_strobe = '1') else
219
220
                   p2_int_data_o_latched;
  -- The error code follows the data.
Michael Munch's avatar
Michael Munch committed
221
  p1_int_err_code <= vc_int_err_code when (live_1 and vc_int_data_strobe = '1') else
222
                     p1_int_err_code_latched;
Michael Munch's avatar
Michael Munch committed
223
  p2_int_err_code <= vc_int_err_code when (live_2 and vc_int_data_strobe = '1') else
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
                     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...)
Michael Munch's avatar
Michael Munch committed
239
240
  p1_busy <= '1' when live_1 else '0';
  p2_busy <= '1' when live_2 else '0';
241

242
243
244
245
  FormalG : if Formal generate

    -- VHDL helper vars
    signal l_data       : vme_vec_64_t := (others => '0');
Michael Munch's avatar
Michael Munch committed
246
    signal l_err_code   : err_vec_t := C_ERR_OK;
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
    
  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
262
    -- psl default clock is rising_edge(clk);
263

Michael Munch's avatar
Michael Munch committed
264
265
266
267
    -- -- 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);
268

Michael Munch's avatar
Michael Munch committed
269
270
271
    -- -- 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';
272

Michael Munch's avatar
Michael Munch committed
273
274
275
    -- -- 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
276

277

Michael Munch's avatar
Michael Munch committed
278
279
280
281
    -- -- If both clients request access then we pick our favourite
    -- psl pick_pref_client_1: assert always
    --   {p1_go = '1' and p2_go = '1' and not prefer_1 and vc_busy = '0'}
    --   |=> start_2 until active_2;
282
    
Michael Munch's avatar
Michael Munch committed
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
    -- psl pick_pref_client_2: assert always
    --   {p1_go = '1' and p2_go = '1' and     prefer_1 and vc_busy = '0'}
    --   |=> 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;

    -- -- If we sent p1_go then the VME core will eventually receive it
    -- psl p1_vme_addr:        assert always {p1_go}
    --   |=> eventually! vc_int_addr = p1_int_addr ;
    -- psl p1_vme_data_i:      assert always {p1_go}
    --   |=> eventually! vc_int_data_i = p1_int_data_i ;
    -- psl p1_vme_am_i:        assert always {p1_go}
    --   |=> eventually! vc_int_am_i = p1_int_am_i ;
    -- psl p1_vme_rw:          assert always {p1_go}
    --   |=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
    -- psl p1_vme_go:          assert always {p1_go}
    --   |=> eventually! vc_int_vme_go = p1_int_vme_go ;
    -- psl p1_vme_blt_deci:    assert always {p1_go}
    --   |=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
    -- psl p1_vme_blt_cont:    assert always {p1_go}
    --   |=> eventually! vc_int_blt_continue = p1_int_blt_continue ;                       
    -- psl p1_vme_berr_ok:     assert always {p1_go}
    --   |=> eventually! vc_int_berr_ok = p1_int_berr_ok ;

    -- -- If we sent p2_go then the VME core will eventually receive it
    -- psl p2_vme_addr:        assert always {p2_go}
    --   |=> eventually! vc_int_addr = p2_int_addr ;
    -- psl p2_vme_data_i:      assert always {p2_go}
    --   |=> eventually! vc_int_data_i = p2_int_data_i ;
    -- psl p2_vme_am_i:        assert always {p2_go}
    --   |=> eventually! vc_int_am_i = p2_int_am_i ;
    -- psl p2_vme_rw:          assert always {p2_go}
    --   |=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
    -- psl p2_vme_go:          assert always {p2_go}
    --   |=> eventually! vc_int_vme_go = p2_int_vme_go ;
    -- psl p2_vme_blt_deci:    assert always {p2_go}
    --   |=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
    -- psl p2_vme_blt_cont:    assert always {p2_go}
    --   |=> eventually! vc_int_blt_continue = p2_int_blt_continue ;                       
    -- psl p2_vme_berr_ok:     assert always {p2_go}
    --   |=> 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;    
354
    
Michael Munch's avatar
Michael Munch committed
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
    -- -- 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;    
376
  end generate FormalG;
377
378
379
380
end architecture;