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

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

190
191
192
193
194
    end if;
  end process;


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

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

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

  -- Signals to the clients from the VME core:

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

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

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

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

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

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

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

281

Michael Munch's avatar
Michael Munch committed
282
283
    -- -- If both clients request access then we pick our favourite
    -- psl pick_pref_client_1: assert always
Michael Munch's avatar
Michael Munch committed
284
    --   {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
285
    --   |=> start_2 until active_2;
286
    
Michael Munch's avatar
Michael Munch committed
287
    -- psl pick_pref_client_2: assert always
Michael Munch's avatar
Michael Munch committed
288
    --   {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
289
290
291
292
293
294
295
296
297
298
299
300
301
    --   |=> 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
302
303
    -- -- 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
304
    --   |=> eventually! vc_int_addr = p1_int_addr ;
Michael Munch's avatar
Michael Munch committed
305
    -- psl p1_vme_data_i:      assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
306
    --   |=> eventually! vc_int_data_i = p1_int_data_i ;
Michael Munch's avatar
Michael Munch committed
307
    -- psl p1_vme_am_i:        assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
308
    --   |=> eventually! vc_int_am_i = p1_int_am_i ;
Michael Munch's avatar
Michael Munch committed
309
    -- psl p1_vme_rw:          assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
310
    --   |=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
311
    -- psl p1_vme_go:          assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
312
    --   |=> eventually! vc_int_vme_go = p1_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
313
    -- psl p1_vme_blt_deci:    assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
314
    --   |=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
315
    -- psl p1_vme_blt_cont:    assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
316
    --   |=> eventually! vc_int_blt_continue = p1_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
317
    -- psl p1_vme_berr_ok:     assert always {p1_int_vme_go}
Michael Munch's avatar
Michael Munch committed
318
319
    --   |=> eventually! vc_int_berr_ok = p1_int_berr_ok ;

Michael Munch's avatar
Michael Munch committed
320
321
    -- -- 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
322
    --   |=> eventually! vc_int_addr = p2_int_addr ;
Michael Munch's avatar
Michael Munch committed
323
    -- psl p2_vme_data_i:      assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
324
    --   |=> eventually! vc_int_data_i = p2_int_data_i ;
Michael Munch's avatar
Michael Munch committed
325
    -- psl p2_vme_am_i:        assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
326
    --   |=> eventually! vc_int_am_i = p2_int_am_i ;
Michael Munch's avatar
Michael Munch committed
327
    -- psl p2_vme_rw:          assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
328
    --   |=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
Michael Munch's avatar
Michael Munch committed
329
    -- psl p2_vme_go:          assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
330
    --   |=> eventually! vc_int_vme_go = p2_int_vme_go ;
Michael Munch's avatar
Michael Munch committed
331
    -- psl p2_vme_blt_deci:    assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
332
    --   |=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
Michael Munch's avatar
Michael Munch committed
333
    -- psl p2_vme_blt_cont:    assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
334
    --   |=> eventually! vc_int_blt_continue = p2_int_blt_continue ;                       
Michael Munch's avatar
Michael Munch committed
335
    -- psl p2_vme_berr_ok:     assert always {p2_int_vme_go}
Michael Munch's avatar
Michael Munch committed
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
    --   |=> 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;    
358
    
Michael Munch's avatar
Michael Munch committed
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
    -- -- 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;    
380
  end generate FormalG;
381
382
383
384
end architecture;