vme_cli_arb.vhd 17.6 KB
Newer Older
1
2
library ieee;
use ieee.std_logic_1164.all;
Michael Munch's avatar
Michael Munch committed
3
4
library vme;
use vme.vme_pkg.all;
5
6
7
8
9
10
11
12
13

-- 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
14
15
16
17
  generic (
    -- To synth formal verification
    formal : boolean := true
  );
18
19
20
21
22
23
24
25
26
27
28
29
  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
30
    signal p1_int_err_code         : out err_vec_t := C_ERR_OK;
31

32
33
34
35
36
37
38
    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;
39
    signal p1_int_blt_continue     : in std_logic;
40
41
42
43

    signal p1_int_berr_ok          : in std_logic;

    -- Signals to/from the second client.
44

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

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

    signal p2_int_berr_ok          : in std_logic;

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

67
68
    -- Core 1
    signal vc1_busy                 : in std_logic := '0';
69

70
71
72
73
74
    signal vc1_int_data_o           : in vme_vec_64_t;
    signal vc1_int_data_strobe      : in std_logic := c_DATA_CLEAR;
    signal vc1_int_go_consumed_strobe : in std_logic := '0';
    signal vc1_int_blt_decision_strobe : in std_logic := '0';
    signal vc1_int_err_code         : in err_vec_t := C_ERR_OK;
75

76
77
78
79
80
    signal vc1_int_addr             : out vme_addr_t;
    signal vc1_int_data_i           : out vme_vec_64_t;
    signal vc1_int_am_i             : out am_vec_t;
    signal vc1_int_vme_rw           : out std_logic;
    signal vc1_int_vme_go           : out std_logic;
81

82
83
    signal vc1_int_blt_decided      : out std_logic;
    signal vc1_int_blt_continue     : out std_logic;
84

85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
    signal vc1_int_berr_ok          : out std_logic;


    -- Core 2
    signal vc2_busy                 : in std_logic := '0';

    signal vc2_int_data_o           : in vme_vec_64_t;
    signal vc2_int_data_strobe      : in std_logic := c_DATA_CLEAR;
    signal vc2_int_go_consumed_strobe : in std_logic := '0';
    signal vc2_int_blt_decision_strobe : in std_logic := '0';
    signal vc2_int_err_code         : in err_vec_t := C_ERR_OK;

    signal vc2_int_addr             : out vme_addr_t;
    signal vc2_int_data_i           : out vme_vec_64_t;
    signal vc2_int_am_i             : out am_vec_t;
    signal vc2_int_vme_rw           : out std_logic;
    signal vc2_int_vme_go           : out std_logic;

    signal vc2_int_blt_decided      : out std_logic;
    signal vc2_int_blt_continue     : out std_logic;

    signal vc2_int_berr_ok          : out std_logic    
107

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

Håkan Johansson's avatar
Håkan Johansson committed
111
112
--    signal stop                 : in std_logic;
--    signal int_err_clear        : in std_logic;
113

Håkan Johansson's avatar
Håkan Johansson committed
114
--    signal int_data_ack : in std_logic;
115

Håkan Johansson's avatar
Håkan Johansson committed
116
--    -- Changed behaviour:
117

Håkan Johansson's avatar
Håkan Johansson committed
118
119
--    -- Single-cycle strobe:
--    signal int_data_strobe      : out std_logic := c_DATA_CLEAR;
120

121

122
123
124
125
126
127
128
    );
end entity;



architecture rtl of vme_cli_arb is

Michael Munch's avatar
Michael Munch committed
129
130
131
  -- signal state          : vme_data_state := STOPPED;
  -- signal addr_mode      : addr_type_t;
  -- signal transfer_mode  : transfer_type_t;
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151



  -- In case we are not busy, which client would we like to
  -- make active (if any).
  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;

152
153
154
155

  -- Which core is active
  signal core_1         : boolean := true;
  
156
157
  -- Who will we prefer when we can take the next client, i.e. are
  -- no longer busy?
Michael Munch's avatar
Michael Munch committed
158
159
  signal prefer_1       : boolean := false;

160
161
  signal p1_int_data_o_latched   : vme_vec_64_t := (others => '0');
  signal p2_int_data_o_latched   : vme_vec_64_t := (others => '0');
162

Michael Munch's avatar
Michael Munch committed
163
164
  signal p1_int_err_code_latched : err_vec_t := C_ERR_OK;
  signal p2_int_err_code_latched : err_vec_t := C_ERR_OK;
165
166
167
168
169
170
171
172
173


  signal r_busy                  : std_logic := '0';
  signal r_data_o                : vme_vec_64_t;
  signal r_data_strobe           : std_logic := c_DATA_CLEAR;
  signal r_go_consumed_strobe    : std_logic := '0';
  signal r_blt_decision_strobe   : std_logic := '0';
  signal r_err_code              : err_vec_t := C_ERR_OK;
  signal r_vme_go                : std_logic := '0'; 
174
175
begin

176
177
178
179
180
181
182
183
  -- Muxed version of all inputs from VME cores
  r_busy                 <= vc1_busy                    when core_1 else vc2_busy;
  r_data_o               <= vc1_int_data_o              when core_1 else vc2_int_data_o;
  r_data_strobe          <= vc1_int_data_strobe         when core_1 else vc2_int_data_strobe;
  r_go_consumed_strobe   <= vc1_int_go_consumed_strobe  when core_1 else vc2_int_go_consumed_strobe;
  r_blt_decision_strobe  <= vc1_int_blt_decision_strobe when core_1 else vc2_int_blt_decision_strobe;
  r_err_code             <= vc1_int_err_code            when core_1 else vc2_int_err_code;
  
Michael Munch's avatar
Michael Munch committed
184
185
  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);
186

187
188
189
190
  -- start_1 <= r_busy = '0' and want_1;
  -- start_2 <= r_busy = '0' and want_2;
  start_1 <= vc1_busy = '0' and vc2_busy = '0' and want_1;
  start_2 <= vc1_busy = '0' and vc2_busy = '0' and want_2;  
191
192
193

  -- We kill the live assignment as soon as busy is removed.
  -- (Not really needed.)
194
195
  live_1 <= (active_1 and r_busy = '1') or start_1;
  live_2 <= (active_2 and r_busy = '1') or start_2;
196

Michael Munch's avatar
Michael Munch committed
197
198
199
200
  -- Only AM=0x19 are passed to core 2.
  core_1 <= p1_int_am_i /= c_AM_TRLOII when live_1 else
            p2_int_am_i /= c_AM_TRLOII;
  
201
202
203
  process (clk)
  begin
    if (rising_edge(clk)) then
204
      if (r_busy = '0') then
Michael Munch's avatar
Michael Munch committed
205
206
        -- Latch error code when busy pulled
        if (active_1) then
207
          p1_int_err_code_latched <= r_err_code;
Michael Munch's avatar
Michael Munch committed
208
209
        end if;
        if (active_2) then
210
          p2_int_err_code_latched <= r_err_code;
Michael Munch's avatar
Michael Munch committed
211
        end if;
212
213
214
215
216
217
218
        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;
Michael Munch's avatar
Michael Munch committed
219
        prefer_1 <= false;       
220
221
222
223
224
225
      end if;
      if (start_2) then
        active_2 <= true;
        prefer_1 <= true;
      end if;

226
227
      -- We select on active instead of live, since active is cheaper (comes
      -- directly from a flip-flop, instead of logic), and
228
229
230
      -- vc1_int_data_strobe will not come on the first cycle.
      if (active_1 and r_data_strobe = '1') then
        p1_int_data_o_latched   <= r_data_o;
231
      end if;
232
233
      if (active_2 and r_data_strobe = '1') then
        p2_int_data_o_latched   <= r_data_o;
234
235
      end if;

236
237
238
239
240
    end if;
  end process;


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

242
243
244
  -- 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.
245

246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
  -- We send all signals, except go, to both cores.
  vc1_int_addr         <= p1_int_addr          when live_1 else p2_int_addr;
  vc1_int_data_i       <= p1_int_data_i        when live_1 else p2_int_data_i;
  vc1_int_am_i         <= p1_int_am_i          when live_1 else p2_int_am_i;
  vc1_int_vme_rw       <= p1_int_vme_rw        when live_1 else p2_int_vme_rw;
  vc1_int_blt_decided  <= p1_int_blt_decided   when live_1 else p2_int_blt_decided;
  vc1_int_blt_continue <= p1_int_blt_continue  when live_1 else p2_int_blt_continue;
  vc1_int_berr_ok      <= p1_int_berr_ok       when live_1 else p2_int_berr_ok;

  vc2_int_addr         <= p1_int_addr          when live_1 else p2_int_addr;
  vc2_int_data_i       <= p1_int_data_i        when live_1 else p2_int_data_i;
  vc2_int_am_i         <= p1_int_am_i          when live_1 else p2_int_am_i;
  vc2_int_vme_rw       <= p1_int_vme_rw        when live_1 else p2_int_vme_rw;
  vc2_int_blt_decided  <= p1_int_blt_decided   when live_1 else p2_int_blt_decided;
  vc2_int_blt_continue <= p1_int_blt_continue  when live_1 else p2_int_blt_continue;
  vc2_int_berr_ok      <= p1_int_berr_ok       when live_1 else p2_int_berr_ok;


  -- Go handling.
  r_vme_go             <= p1_int_vme_go        when live_1 else p2_int_vme_go;
  vc1_int_vme_go       <= r_vme_go             when core_1 else '0';
  vc2_int_vme_go       <= r_vme_go             when not core_1 else '0';  
268
269
270

  -- Signals to the clients from the VME core:

271
272
273
  -- 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!
274

275
276
  -- Data is passed directly through on the cycle they have been latched.
  -- Otherwise, take the latched value:
277
  p1_int_data_o <= r_data_o when (live_1 and r_data_strobe = '1') else
278
                   p1_int_data_o_latched;
279
  p2_int_data_o <= r_data_o when (live_2 and r_data_strobe = '1') else
280
281
                   p2_int_data_o_latched;
  -- The error code follows the data.
282
  p1_int_err_code <= r_err_code when (live_1 and r_data_strobe = '1') else
283
                     p1_int_err_code_latched;
284
  p2_int_err_code <= r_err_code when (live_2 and r_data_strobe = '1') else
285
286
287
                     p2_int_err_code_latched;

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

291
292
  p1_int_go_consumed_strobe <= r_go_consumed_strobe when live_1 else '0';
  p2_int_go_consumed_strobe <= r_go_consumed_strobe when live_2 else '0';
293

294
295
  p1_int_blt_decision_strobe <= r_blt_decision_strobe when live_1 else '0';
  p2_int_blt_decision_strobe <= r_blt_decision_strobe when live_2 else '0';
296
297
298
299

  -- 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...)
300
301
  -- p1_busy <= '1' when live_1 else '0';
  -- p2_busy <= '1' when live_2 else '0';
302

303
304
305
  p1_busy <= '1' when active_1 else '0';
  p2_busy <= '1' when active_2 else '0';
  
306
307
308
309
  FormalG : if Formal generate

    -- VHDL helper vars
    signal l_data       : vme_vec_64_t := (others => '0');
Michael Munch's avatar
Michael Munch committed
310
    signal l_err_code   : err_vec_t := C_ERR_OK;
311
312
313
314
315
316
317
318
319
    
  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
320
321
        l_data <= vc1_int_data_o;
        l_err_code <= vc1_int_err_code;
322
323
324
325
      end if;
    end process;
    
    
Michael Munch's avatar
Michael Munch committed
326
    -- psl default clock is rising_edge(clk);
327

Michael Munch's avatar
Michael Munch committed
328
329
330
331
    -- -- 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);
332

Michael Munch's avatar
Michael Munch committed
333
    -- -- Don't start clients when VME core is busy
334
335
    -- psl busy_dont_start_1:  assert always {vc1_busy = '1'} |-> not start_1 until vc1_busy = '0';
    -- psl busy_dont_start_2:  assert always {vc1_busy = '1'} |-> not start_1 until vc1_busy = '0';
336

Michael Munch's avatar
Michael Munch committed
337
338
339
    -- -- 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
340

341

Michael Munch's avatar
Michael Munch committed
342
343
    -- -- If both clients request access then we pick our favourite
    -- psl pick_pref_client_1: assert always
344
    --   {p1_int_vme_go = '1' and p2_int_vme_go = '1' and not prefer_1 and vc1_busy = '0'}
Michael Munch's avatar
Michael Munch committed
345
    --   |=> start_2 until active_2;
346
    
Michael Munch's avatar
Michael Munch committed
347
    -- psl pick_pref_client_2: assert always
348
    --   {p1_int_vme_go = '1' and p2_int_vme_go = '1' and     prefer_1 and vc1_busy = '0'}
Michael Munch's avatar
Michael Munch committed
349
350
351
352
    --   |=> start_1 until active_1;

    -- -- While client is live it data output tracks live data
    -- psl live_track_1:
353
354
355
    --   assert always {active_1; vc1_int_data_strobe = '1'}
    --     |=> p1_int_data_o = vc1_int_data_o
    --     until vc1_int_data_strobe = '0' or not live_1;
Michael Munch's avatar
Michael Munch committed
356
357

    -- psl live_track_2:
358
359
360
    --   assert always {active_2; vc1_int_data_strobe = '1'}
    --     |=> p2_int_data_o = vc1_int_data_o
    --     until vc1_int_data_strobe = '0' or not live_2;
Michael Munch's avatar
Michael Munch committed
361

Michael Munch's avatar
Michael Munch committed
362
363
    -- -- 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}
364
    --   |=> eventually! vc1_int_addr = p1_int_addr ;
Michael Munch's avatar
Michael Munch committed
365
    -- psl p1_vme_data_i:      assert always {p1_int_vme_go}
366
    --   |=> eventually! vc1_int_data_i = p1_int_data_i ;
Michael Munch's avatar
Michael Munch committed
367
    -- psl p1_vme_am_i:        assert always {p1_int_vme_go}
368
    --   |=> eventually! vc1_int_am_i = p1_int_am_i ;
Michael Munch's avatar
Michael Munch committed
369
    -- psl p1_vme_rw:          assert always {p1_int_vme_go}
370
    --   |=> eventually! vc1_int_vme_rw = p1_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
371
    -- psl p1_vme_go:          assert always {p1_int_vme_go}
372
    --   |=> eventually! vc1_int_vme_go = p1_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
373
    -- psl p1_vme_blt_deci:    assert always {p1_int_vme_go}
374
    --   |=> eventually! vc1_int_blt_decided = p1_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
375
    -- psl p1_vme_blt_cont:    assert always {p1_int_vme_go}
376
    --   |=> eventually! vc1_int_blt_continue = p1_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
377
    -- psl p1_vme_berr_ok:     assert always {p1_int_vme_go}
378
    --   |=> eventually! vc1_int_berr_ok = p1_int_berr_ok ;
Michael Munch's avatar
Michael Munch committed
379

Michael Munch's avatar
Michael Munch committed
380
381
    -- -- 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}
382
    --   |=> eventually! vc1_int_addr = p2_int_addr ;
Michael Munch's avatar
Michael Munch committed
383
    -- psl p2_vme_data_i:      assert always {p2_int_vme_go}
384
    --   |=> eventually! vc1_int_data_i = p2_int_data_i ;
Michael Munch's avatar
Michael Munch committed
385
    -- psl p2_vme_am_i:        assert always {p2_int_vme_go}
386
    --   |=> eventually! vc1_int_am_i = p2_int_am_i ;
Michael Munch's avatar
Michael Munch committed
387
    -- psl p2_vme_rw:          assert always {p2_int_vme_go}
388
    --   |=> eventually! vc1_int_vme_rw = p2_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
389
    -- psl p2_vme_go:          assert always {p2_int_vme_go}
390
    --   |=> eventually! vc1_int_vme_go = p2_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
391
    -- psl p2_vme_blt_deci:    assert always {p2_int_vme_go}
392
    --   |=> eventually! vc1_int_blt_decided = p2_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
393
    -- psl p2_vme_blt_cont:    assert always {p2_int_vme_go}
394
    --   |=> eventually! vc1_int_blt_continue = p2_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
395
    -- psl p2_vme_berr_ok:     assert always {p2_int_vme_go}
396
    --   |=> eventually! vc1_int_berr_ok = p2_int_berr_ok ;
Michael Munch's avatar
Michael Munch committed
397
398
399

    -- -- Data strobes are routed to live client
    -- psl p1_get_d_strobe:     assert always {live_1}
400
    --   |=> p1_int_data_strobe = vc1_int_data_strobe until not live_1;
Michael Munch's avatar
Michael Munch committed
401
402

    -- psl p2_get_d_strobe:     assert always {live_2}
403
    --   |=> p2_int_data_strobe = vc1_int_data_strobe until not live_2;
Michael Munch's avatar
Michael Munch committed
404
405
406

    -- -- Go strobes are routed to live client
    -- psl p1_get_go_strobe:     assert always {live_1}
407
    --   |=> p1_int_go_consumed_strobe = vc1_int_go_consumed_strobe until not live_1;
Michael Munch's avatar
Michael Munch committed
408
409

    -- psl p2_get_go_strobe:     assert always {live_2}
410
    --   |=> p2_int_go_consumed_strobe = vc1_int_go_consumed_strobe until not live_2;    
Michael Munch's avatar
Michael Munch committed
411
412
413

    -- -- BLT decision strobes are routed to live client
    -- psl p1_get_blt_strobe:     assert always {live_1}
414
    --   |=> p1_int_blt_decision_strobe = vc1_int_blt_decision_strobe until not live_1;
Michael Munch's avatar
Michael Munch committed
415
416

    -- psl p2_get_blt_strobe:     assert always {live_2}
417
    --   |=> p2_int_blt_decision_strobe = vc1_int_blt_decision_strobe until not live_2;    
418
    
Michael Munch's avatar
Michael Munch committed
419
420
    -- -- Latched data tracks input while active and strobed
    -- psl p1_tracks_data:     assert always
421
    --   {active_1 and vc1_busy = '1' and vc1_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
422
    --   |=> p1_int_data_o_latched = l_data
423
    --   until vc1_int_data_strobe = '0' or not active_1;
Michael Munch's avatar
Michael Munch committed
424
425

    -- psl p2_tracks_data:     assert always
426
    --   {active_2 and vc1_busy = '1' and vc1_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
427
    --   |=> p2_int_data_o_latched = l_data
428
    --   until vc1_int_data_strobe = '0' or not active_2;
Michael Munch's avatar
Michael Munch committed
429
430
431

    -- -- Latched error tracks input while active and strobed
    -- psl p1_tracks_err:     assert always
432
    --   {active_1 and vc1_busy = '1' and vc1_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
433
    --   |=> p1_int_err_code_latched = l_err_code
434
    --   until vc1_int_data_strobe = '0' or not active_1;
Michael Munch's avatar
Michael Munch committed
435
436

    -- psl p2_tracks_err:     assert always
437
    --   {active_2 and vc1_busy = '1' and vc1_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
438
    --   |=> p2_int_err_code_latched = l_err_code
439
    --   until vc1_int_data_strobe = '0' or not active_2;    
440
  end generate FormalG;
441
442
443
444
end architecture;