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

Michael Munch's avatar
Michael Munch committed
67
    signal vc_busy                 : in std_logic := '0';
68

Michael Munch's avatar
Michael Munch committed
69
70
71
72
73
    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';
    signal vc_int_err_code         : in err_vec_t := C_ERR_OK;
74

Michael Munch's avatar
Michael Munch committed
75
76
77
78
79
    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;
80

Michael Munch's avatar
Michael Munch committed
81
82
    signal vc_int_blt_decided      : out std_logic;
    signal vc_int_blt_continue     : out std_logic;
83

Michael Munch's avatar
Michael Munch committed
84
    signal vc_int_berr_ok          : out std_logic
85

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

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

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

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

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

99

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



architecture rtl of vme_cli_arb is

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



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

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

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

Michael Munch's avatar
Michael Munch committed
142
143
  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);
144

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

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

153
154
155
  process (clk)
  begin
    if (rising_edge(clk)) then
Michael Munch's avatar
Michael Munch committed
156
157
158
159

      cnt <= cnt + 1;

      if (vc_busy = '0') then
Michael Munch's avatar
Michael Munch committed
160
161
        -- Latch error code when busy pulled
        if (active_1) then
Michael Munch's avatar
Michael Munch committed
162
          p1_int_err_code_latched <= vc_int_err_code;
Michael Munch's avatar
Michael Munch committed
163
164
        end if;
        if (active_2) then
Michael Munch's avatar
Michael Munch committed
165
          p2_int_err_code_latched <= vc_int_err_code;
Michael Munch's avatar
Michael Munch committed
166
        end if;
167
168
169
170
171
172
173
        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
174
        prefer_1 <= false;
175
176
177
178
179
180
      end if;
      if (start_2) then
        active_2 <= true;
        prefer_1 <= true;
      end if;

181
182
      -- We select on active instead of live, since active is cheaper (comes
      -- directly from a flip-flop, instead of logic), and
Michael Munch's avatar
Michael Munch committed
183
184
185
      -- vc_int_data_strobe will not come on the first cycle.
      if (active_1 and vc_int_data_strobe = '1') then
        p1_int_data_o_latched   <= vc_int_data_o;
186
      end if;
Michael Munch's avatar
Michael Munch committed
187
188
      if (active_2 and vc_int_data_strobe = '1') then
        p2_int_data_o_latched   <= vc_int_data_o;
189
190
      end if;

191
192
193
194
195
    end if;
  end process;


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

197
198
199
  -- 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.
200

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

  -- Signals to the clients from the VME core:

212
213
214
  -- 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!
215

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

  -- The strobes always go to the live client.
Michael Munch's avatar
Michael Munch committed
229
230
  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';
231

Michael Munch's avatar
Michael Munch committed
232
233
  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';
234

Michael Munch's avatar
Michael Munch committed
235
236
  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';
237
238
239
240

  -- 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...)
241
242
  -- p1_busy <= '1' when live_1 else '0';
  -- p2_busy <= '1' when live_2 else '0';
243

244
245
246
  p1_busy <= '1' when active_1 else '0';
  p2_busy <= '1' when active_2 else '0';
  
247
248
249
250
  FormalG : if Formal generate

    -- VHDL helper vars
    signal l_data       : vme_vec_64_t := (others => '0');
Michael Munch's avatar
Michael Munch committed
251
    signal l_err_code   : err_vec_t := C_ERR_OK;
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
Michael Munch's avatar
Michael Munch committed
261
262
        l_data <= vc_int_data_o;
        l_err_code <= vc_int_err_code;
263
264
265
266
      end if;
    end process;
    
    
Michael Munch's avatar
Michael Munch committed
267
    -- psl default clock is rising_edge(clk);
268

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

Michael Munch's avatar
Michael Munch committed
274
    -- -- Don't start clients when VME core is busy
Michael Munch's avatar
Michael Munch committed
275
276
    -- 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';
277

Michael Munch's avatar
Michael Munch committed
278
279
280
    -- -- 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
281

282

Michael Munch's avatar
Michael Munch committed
283
284
    -- -- If both clients request access then we pick our favourite
    -- psl pick_pref_client_1: assert always
Michael Munch's avatar
Michael Munch committed
285
    --   {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
286
    --   |=> start_2 until active_2;
287
    
Michael Munch's avatar
Michael Munch committed
288
    -- psl pick_pref_client_2: assert always
Michael Munch's avatar
Michael Munch committed
289
    --   {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
290
291
292
293
    --   |=> start_1 until active_1;

    -- -- While client is live it data output tracks live data
    -- psl live_track_1:
Michael Munch's avatar
Michael Munch committed
294
295
296
    --   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;
Michael Munch's avatar
Michael Munch committed
297
298

    -- psl live_track_2:
Michael Munch's avatar
Michael Munch committed
299
300
301
    --   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
302

Michael Munch's avatar
Michael Munch committed
303
304
    -- -- 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
305
    --   |=> eventually! vc_int_addr = p1_int_addr ;
Michael Munch's avatar
Michael Munch committed
306
    -- psl p1_vme_data_i:      assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
307
    --   |=> eventually! vc_int_data_i = p1_int_data_i ;
Michael Munch's avatar
Michael Munch committed
308
    -- psl p1_vme_am_i:        assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
309
    --   |=> eventually! vc_int_am_i = p1_int_am_i ;
Michael Munch's avatar
Michael Munch committed
310
    -- psl p1_vme_rw:          assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
311
    --   |=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
312
    -- psl p1_vme_go:          assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
313
    --   |=> eventually! vc_int_vme_go = p1_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
314
    -- psl p1_vme_blt_deci:    assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
315
    --   |=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
316
    -- psl p1_vme_blt_cont:    assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
317
    --   |=> eventually! vc_int_blt_continue = p1_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
318
    -- psl p1_vme_berr_ok:     assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
319
    --   |=> eventually! vc_int_berr_ok = p1_int_berr_ok ;
Michael Munch's avatar
Michael Munch committed
320

Michael Munch's avatar
Michael Munch committed
321
322
    -- -- 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
323
    --   |=> eventually! vc_int_addr = p2_int_addr ;
Michael Munch's avatar
Michael Munch committed
324
    -- psl p2_vme_data_i:      assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
325
    --   |=> eventually! vc_int_data_i = p2_int_data_i ;
Michael Munch's avatar
Michael Munch committed
326
    -- psl p2_vme_am_i:        assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
327
    --   |=> eventually! vc_int_am_i = p2_int_am_i ;
Michael Munch's avatar
Michael Munch committed
328
    -- psl p2_vme_rw:          assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
329
    --   |=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
330
    -- psl p2_vme_go:          assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
331
    --   |=> eventually! vc_int_vme_go = p2_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
332
    -- psl p2_vme_blt_deci:    assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
333
    --   |=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
334
    -- psl p2_vme_blt_cont:    assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
335
    --   |=> eventually! vc_int_blt_continue = p2_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
336
    -- psl p2_vme_berr_ok:     assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
337
    --   |=> eventually! vc_int_berr_ok = p2_int_berr_ok ;
Michael Munch's avatar
Michael Munch committed
338
339
340

    -- -- Data strobes are routed to live client
    -- psl p1_get_d_strobe:     assert always {live_1}
Michael Munch's avatar
Michael Munch committed
341
    --   |=> p1_int_data_strobe = vc_int_data_strobe until not live_1;
Michael Munch's avatar
Michael Munch committed
342
343

    -- psl p2_get_d_strobe:     assert always {live_2}
Michael Munch's avatar
Michael Munch committed
344
    --   |=> p2_int_data_strobe = vc_int_data_strobe until not live_2;
Michael Munch's avatar
Michael Munch committed
345
346
347

    -- -- Go strobes are routed to live client
    -- psl p1_get_go_strobe:     assert always {live_1}
Michael Munch's avatar
Michael Munch committed
348
    --   |=> p1_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_1;
Michael Munch's avatar
Michael Munch committed
349
350

    -- psl p2_get_go_strobe:     assert always {live_2}
Michael Munch's avatar
Michael Munch committed
351
    --   |=> p2_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_2;    
Michael Munch's avatar
Michael Munch committed
352
353
354

    -- -- BLT decision strobes are routed to live client
    -- psl p1_get_blt_strobe:     assert always {live_1}
Michael Munch's avatar
Michael Munch committed
355
    --   |=> p1_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_1;
Michael Munch's avatar
Michael Munch committed
356
357

    -- psl p2_get_blt_strobe:     assert always {live_2}
Michael Munch's avatar
Michael Munch committed
358
    --   |=> p2_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_2;    
359
    
Michael Munch's avatar
Michael Munch committed
360
361
    -- -- Latched data tracks input while active and strobed
    -- psl p1_tracks_data:     assert always
Michael Munch's avatar
Michael Munch committed
362
    --   {active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
363
    --   |=> p1_int_data_o_latched = l_data
Michael Munch's avatar
Michael Munch committed
364
    --   until vc_int_data_strobe = '0' or not active_1;
Michael Munch's avatar
Michael Munch committed
365
366

    -- psl p2_tracks_data:     assert always
Michael Munch's avatar
Michael Munch committed
367
    --   {active_2 and vc_busy = '1' and vc_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
368
    --   |=> p2_int_data_o_latched = l_data
Michael Munch's avatar
Michael Munch committed
369
    --   until vc_int_data_strobe = '0' or not active_2;
Michael Munch's avatar
Michael Munch committed
370
371
372

    -- -- Latched error tracks input while active and strobed
    -- psl p1_tracks_err:     assert always
Michael Munch's avatar
Michael Munch committed
373
    --   {active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
374
    --   |=> p1_int_err_code_latched = l_err_code
Michael Munch's avatar
Michael Munch committed
375
    --   until vc_int_data_strobe = '0' or not active_1;
Michael Munch's avatar
Michael Munch committed
376
377

    -- psl p2_tracks_err:     assert always
Michael Munch's avatar
Michael Munch committed
378
    --   {active_2 and vc_busy = '1' and vc_int_data_strobe = '1'}
Michael Munch's avatar
Michael Munch committed
379
    --   |=> p2_int_err_code_latched = l_err_code
Michael Munch's avatar
Michael Munch committed
380
    --   until vc_int_data_strobe = '0' or not active_2;    
381
  end generate FormalG;
382
383
384
385
end architecture;