Commit | Line | Data |
---|---|---|
86530b38 AT |
1 | // ========== Copyright Header Begin ========================================== |
2 | // | |
3 | // OpenSPARC T2 Processor File: pcx_l2t_checker.v | |
4 | // Copyright (C) 1995-2007 Sun Microsystems, Inc. All Rights Reserved | |
5 | // 4150 Network Circle, Santa Clara, California 95054, U.S.A. | |
6 | // | |
7 | // * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. | |
8 | // | |
9 | // This program is free software; you can redistribute it and/or modify | |
10 | // it under the terms of the GNU General Public License as published by | |
11 | // the Free Software Foundation; version 2 of the License. | |
12 | // | |
13 | // This program is distributed in the hope that it will be useful, | |
14 | // but WITHOUT ANY WARRANTY; without even the implied warranty of | |
15 | // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
16 | // GNU General Public License for more details. | |
17 | // | |
18 | // You should have received a copy of the GNU General Public License | |
19 | // along with this program; if not, write to the Free Software | |
20 | // Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA | |
21 | // | |
22 | // For the avoidance of doubt, and except that if any non-GPL license | |
23 | // choice is available it will apply instead, Sun elects to use only | |
24 | // the General Public License version 2 (GPLv2) at this time for any | |
25 | // software where a choice of GPL license versions is made | |
26 | // available with the language indicating that GPLv2 or any later version | |
27 | // may be used, or where a choice of which version of the GPL is applied is | |
28 | // otherwise unspecified. | |
29 | // | |
30 | // Please contact Sun Microsystems, Inc., 4150 Network Circle, Santa Clara, | |
31 | // CA 95054 USA or visit www.sun.com if you need additional information or | |
32 | // have any questions. | |
33 | // | |
34 | // ========== Copyright Header End ============================================ | |
35 | `ifdef FC_BENCH | |
36 | `define TB_TOP tb_top | |
37 | `else | |
38 | `ifdef CCM | |
39 | `define TB_TOP tb_top | |
40 | `else | |
41 | `define TB_TOP l2sat_top | |
42 | `endif | |
43 | `endif | |
44 | ||
45 | `define pcx_req0 `TB_TOP.cpu.pcx_sctag0_data_rdy_px1 | |
46 | `define pcx_atm0 `TB_TOP.cpu.pcx_sctag0_atm_px1 | |
47 | `define pcx_valid0 `TB_TOP.cpu.pcx_sctag0_data_px2[129:129] | |
48 | `define pcx_req0_type `TB_TOP.cpu.pcx_sctag0_data_px2[128:124] | |
49 | `define pcx_req0_nc `TB_TOP.cpu.pcx_sctag0_data_px2[123:123] | |
50 | `define pcx_req0_cpu_id `TB_TOP.cpu.pcx_sctag0_data_px2[122:120] | |
51 | `define pcx_req0_thread_id `TB_TOP.cpu.pcx_sctag0_data_px2[119:117] | |
52 | `define pcx_req0_inv `TB_TOP.cpu.pcx_sctag0_data_px2[116:116] | |
53 | `define pcx_req0_pf `TB_TOP.cpu.pcx_sctag0_data_px2[115:115] | |
54 | `define pcx_req0_bis `TB_TOP.cpu.pcx_sctag0_data_px2[114:114] | |
55 | `define pcx_req0_size `TB_TOP.cpu.pcx_sctag0_data_px2[111:104] | |
56 | `define pcx_req0_bnk_addr `TB_TOP.cpu.pcx_sctag0_data_px2[72:70] | |
57 | `define clk `TB_TOP.cpu.l2clk | |
58 | `define rst_n `TB_TOP.reset | |
59 | `define partial_mode_bank0 `TB_TOP.cpu.l2t0.ncu_l2t_pm | |
60 | `define pcx_sctag0_data_rdy_px1 `TB_TOP.cpu.pcx_sctag0_data_rdy_px1 | |
61 | ||
62 | `define LOAD 5'b00000 | |
63 | `define IFILL 5'b10000 | |
64 | `define STORE 5'b00001 | |
65 | `define CAS_1 5'b00010 | |
66 | `define CAS_2 5'b00011 | |
67 | `define SWAP 5'b00111 | |
68 | `define STRLD 5'b00100 | |
69 | `define STRST 5'b00101 | |
70 | `define MMULD 5'b01000 | |
71 | ||
72 | `define BANK0 3'b000 | |
73 | `define BANK1 3'b001 | |
74 | `define BANK2 3'b010 | |
75 | `define BANK3 3'b011 | |
76 | `define BANK4 3'b100 | |
77 | `define BANK5 3'b101 | |
78 | `define BANK6 3'b110 | |
79 | `define BANK7 3'b111 | |
80 | ||
81 | `define CPU0 3'b000 | |
82 | `define CPU1 3'b001 | |
83 | `define CPU2 3'b010 | |
84 | `define CPU3 3'b011 | |
85 | `define CPU4 3'b100 | |
86 | `define CPU5 3'b101 | |
87 | `define CPU6 3'b110 | |
88 | `define CPU7 3'b111 | |
89 | ||
90 | module pcx_l2t_checker(); // top level module l2_pcx_protocol | |
91 | reg pcx_sctag0_data_rdy_px1_d1; | |
92 | wire[3:0] AB; | |
93 | assign AB = {`TB_TOP.cpu.l2t0.ncu_l2t_ba67, `TB_TOP.cpu.l2t0.ncu_l2t_ba45, `TB_TOP.cpu.l2t0.ncu_l2t_ba23, `TB_TOP.cpu.l2t0.ncu_l2t_ba01}; | |
94 | ||
95 | always @(posedge `TB_TOP.cpu.l2clk) | |
96 | begin | |
97 | pcx_sctag0_data_rdy_px1_d1 <= `pcx_sctag0_data_rdy_px1; | |
98 | end | |
99 | ||
100 | `ifdef FC_BENCH | |
101 | ||
102 | //Check that in Partial Cores Partial Banks mode, the corresponding | |
103 | //l2clk is gated off and the address translation is correct. | |
104 | /* | |
105 | x0in assert -var (`TB_TOP.cpu.l2t0.l2clk == 1'b0) | |
106 | -active (`TB_TOP.cpu.l2t0.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t0.ncu_l2t_ba01 == 1'b1) | |
107 | */ | |
108 | /* x0in assert -var (`TB_TOP.cpu.l2t1.l2clk == 1'b0) | |
109 | -active (`TB_TOP.cpu.l2t1.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t1.ncu_l2t_ba01 == 1'b1) | |
110 | */ | |
111 | /* x0in assert -var (`TB_TOP.cpu.l2t2.l2clk == 1'b0) | |
112 | -active (`TB_TOP.cpu.l2t2.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t2.ncu_l2t_ba23 == 1'b1) | |
113 | */ | |
114 | /* x0in assert -var (`TB_TOP.cpu.l2t3.l2clk == 1'b0) | |
115 | -active (`TB_TOP.cpu.l2t3.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t3.ncu_l2t_ba23 == 1'b1) | |
116 | */ | |
117 | /* x0in assert -var (`TB_TOP.cpu.l2t4.l2clk == 1'b0) | |
118 | -active (`TB_TOP.cpu.l2t4.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t4.ncu_l2t_ba45 == 1'b1) | |
119 | */ | |
120 | /* x0in assert -var (`TB_TOP.cpu.l2t5.l2clk == 1'b0) | |
121 | -active (`TB_TOP.cpu.l2t5.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t5.ncu_l2t_ba45 == 1'b1) | |
122 | */ | |
123 | /* x0in assert -var (`TB_TOP.cpu.l2t6.l2clk == 1'b0) | |
124 | -active (`TB_TOP.cpu.l2t6.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t6.ncu_l2t_ba67 == 1'b1) | |
125 | */ | |
126 | /* x0in assert -var (`TB_TOP.cpu.l2t7.l2clk == 1'b0) | |
127 | -active (`TB_TOP.cpu.l2t7.ncu_l2t_pm == 1'b1 && `TB_TOP.cpu.l2t7.ncu_l2t_ba67 == 1'b1) | |
128 | */ | |
129 | `endif | |
130 | ||
131 | /* x0in assert -var (pcx_l2t_data_px2[72:71] == 2'b00) | |
132 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b0001 ) | |
133 | -module l2t | |
134 | */ | |
135 | /* x0in assert -var (pcx_l2t_data_px2[72:71] == 2'b01) | |
136 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b0010 ) | |
137 | -module l2t | |
138 | */ | |
139 | /* x0in assert -var (pcx_l2t_data_px2[72] == 1'b0) | |
140 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b0011 ) | |
141 | -module l2t | |
142 | */ | |
143 | /* x0in assert -var (pcx_l2t_data_px2[72:71] == 2'b10) | |
144 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b0100 ) | |
145 | -module l2t | |
146 | */ | |
147 | /* x0in assert -var (pcx_l2t_data_px2[71] == 1'b0) | |
148 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b0101 ) | |
149 | -module l2t | |
150 | */ | |
151 | /* x0in assert -var (pcx_l2t_data_px2[72] == ~pcx_l2t_data_px2[71]) | |
152 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b0110 ) | |
153 | -module l2t | |
154 | */ | |
155 | /* x0in assert -var (pcx_l2t_data_px2[72:71] == 2'b11) | |
156 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b1000 ) | |
157 | -module l2t | |
158 | */ | |
159 | /* x0in assert -var (pcx_l2t_data_px2[72] == pcx_l2t_data_px2[71]) | |
160 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b1001 ) | |
161 | -module l2t | |
162 | */ | |
163 | /* x0in assert -var (pcx_l2t_data_px2[71] == 1'b1) | |
164 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b1010 ) | |
165 | -module l2t | |
166 | */ | |
167 | /* x0in assert -var (pcx_l2t_data_px2[72] == 1'b1) | |
168 | -active (ncu_l2t_pm == 1'b1 && AB == 4'b1100 ) | |
169 | -module l2t | |
170 | */ | |
171 | /* 0in assert -var ~(AB == 4'b0000) | |
172 | -active ((`TB_TOP.cpu.ncu_l2t_pm == 1'b1) & (`TB_TOP.flush_reset_complete == 1'b1)) | |
173 | -clock `TB_TOP.cpu.l2clk*/ | |
174 | /* 0in assert -var ~(AB == 4'b0111) | |
175 | -active (`TB_TOP.cpu.ncu_l2t_pm == 1'b1) | |
176 | -clock `TB_TOP.cpu.l2clk*/ | |
177 | /* 0in assert -var ~(AB == 4'b1011) | |
178 | -active (`TB_TOP.cpu.ncu_l2t_pm == 1'b1) | |
179 | -clock `TB_TOP.cpu.l2clk*/ | |
180 | /* 0in assert -var ~(AB == 4'b1101) | |
181 | -active (`TB_TOP.cpu.ncu_l2t_pm == 1'b1) | |
182 | -clock `TB_TOP.cpu.l2clk*/ | |
183 | /* 0in assert -var ~(AB == 4'b1110) | |
184 | -active (`TB_TOP.cpu.ncu_l2t_pm == 1'b1) | |
185 | -clock `TB_TOP.cpu.l2clk*/ | |
186 | /* 0in assert -var ~(AB == 4'b1111) | |
187 | -active (`TB_TOP.cpu.ncu_l2t_pm == 1'b1) | |
188 | -clock `TB_TOP.cpu.l2clk*/ | |
189 | ||
190 | ||
191 | ||
192 | ||
193 | ||
194 | //Check that every request is followed by a data rdy | |
195 | /* | |
196 | x0in assert_follower -leader `pcx_req0 | |
197 | -follower `pcx_valid0 | |
198 | -known_follower | |
199 | -min 1 | |
200 | -max_leader 64 | |
201 | -clock `clk | |
202 | */ | |
203 | ||
204 | ||
205 | //Check that the contents of the packet is valid | |
206 | /* | |
207 | 0in value -var `pcx_req0_type | |
208 | -val `LOAD `IFILL `STORE `CAS_1 `CAS_2 `SWAP `STRST `MMULD `STRLD | |
209 | -active (`pcx_valid0 & pcx_sctag0_data_rdy_px1_d1) | |
210 | -name pcx_req_valid_chk | |
211 | -message "pcx req has an invalid request type" | |
212 | -module cpu | |
213 | -clock `clk | |
214 | */ | |
215 | ||
216 | ||
217 | ||
218 | //Check that for cas/swap packets the nc bit is set to one | |
219 | /* | |
220 | 0in value -var `pcx_req0_nc | |
221 | -val 1'b1 | |
222 | -active (`pcx_valid0 & ((`pcx_req0_type == `CAS_1) | (`pcx_req0_type== `CAS_2) | (`pcx_req0_type == `SWAP))) | |
223 | -name pcx_cas_nc_chk | |
224 | -module cpu | |
225 | -clock `clk | |
226 | */ | |
227 | ||
228 | ||
229 | //Check that for dcache invalidate packets the nc bit is set to zero | |
230 | /* | |
231 | x0in value -var `pcx_req0_nc | |
232 | -val 1'b0 | |
233 | -active (`pcx_valid0 & ((`pcx_req0_type == `LOAD) & (`pcx_req0_inv == 1'b1) & (`pcx_req0_pf ==1'b0))) | |
234 | -name pcx_dcache_nc_chk | |
235 | -module cpu | |
236 | -clock `clk | |
237 | */ | |
238 | ||
239 | ||
240 | //Check that for icache invalidate packets the nc bit is set to zero | |
241 | /* | |
242 | 0in value -var `pcx_req0_nc | |
243 | -val 1'b0 | |
244 | -active (`pcx_valid0 & ((`pcx_req0_type == `IFILL) & (`pcx_req0_inv == 1'b1))) | |
245 | -name pcx_icache_nc_chk | |
246 | -module cpu | |
247 | -clock `clk | |
248 | */ | |
249 | ||
250 | //Check that for streamload and stream store nc bit is set to one | |
251 | /* | |
252 | 0in value -var `pcx_req0_nc | |
253 | -val 1'b1 | |
254 | -active (`pcx_valid0 & ((`pcx_req0_type == `STRST) | (`pcx_req0_type == `STRLD) | (`pcx_req0_type == `MMULD))) | |
255 | -name pcx_cas_nc_chk_str | |
256 | -module cpu | |
257 | -clock `clk | |
258 | */ | |
259 | ||
260 | //Check for block stores and block init stores the size has to be 8'hff | |
261 | ||
262 | //Bank steer check in 8 bank mode the Bank0 should be getting Bank0 pkts | |
263 | /* | |
264 | 0in value -var `pcx_req0_bnk_addr | |
265 | -val `BANK0 | |
266 | -active (`pcx_valid0 & (`pcx_req0_type == `STORE) & (`pcx_req0_bis == 1'b1) & ~(`partial_mode_bank0)) | |
267 | -name pcx_bank0_steer | |
268 | -module cpu | |
269 | -clock `clk | |
270 | */ | |
271 | ||
272 | //Check for skid window, 5 cycles from the time stall is asserted no req's should | |
273 | //be made to the l2t | |
274 | ||
275 | ||
276 | //In case of atomic transactions make sure that the two back to back packets have | |
277 | //the same semantics | |
278 | ||
279 | endmodule //end top level module protocol check | |
280 | ||
281 | /* | |
282 | module l2_pcx_protocol; | |
283 | /////////////////////////////////////////////////////////////////////////////// | |
284 | // These signals can be used to disable certain 0-In checkers at runtime, | |
285 | // so that testcases forcing interface errors don't die with checker firings. | |
286 | /////////////////////////////////////////////////////////////////////////////// | |
287 | //reg disable_l2_checks; | |
288 | reg req0_d, req1_d, req2_d, req3_d, req4_d, req5_d, req6_d, req7_d; | |
289 | reg cpu_id_d, cpu_id_dd; | |
290 | reg atm0_d, atm0_dd; | |
291 | reg atomic_broken; | |
292 | ||
293 | //0in set_clock -default `clk -module l2_pcx_protocol | |
294 | ||
295 | initial | |
296 | begin | |
297 | // disable_l2_checks = 1'b0; | |
298 | atomic_broken = 1'b0; | |
299 | end | |
300 | ||
301 | //task chkr_off; | |
302 | // input [1:0] chkr; | |
303 | //begin | |
304 | // case( chkr ) | |
305 | // 0: disable_l2_checks = 1'b1; | |
306 | // default: | |
307 | // $display("%m %t: invalid checker id %d \n", $time, chkr); | |
308 | // endcase | |
309 | // end | |
310 | //endtask // chkr_off | |
311 | ||
312 | ||
313 | always @(posedge `TB_TOP.cpu.l2clk) | |
314 | begin | |
315 | req0_d <= `req0; | |
316 | atm0_d <= `atm0; | |
317 | cpu_id_d <= `cpu_id0; | |
318 | cpu_id_dd <= cpu_id_d; | |
319 | atm0_dd <= atm0_d; | |
320 | end | |
321 | ||
322 | wire atm_req0; | |
323 | assign atm_req0 = `req0 & `atm0; | |
324 | ||
325 | wire non_atm_req0; | |
326 | assign non_atm_req0 = `req0 & ~(`atm0); | |
327 | ||
328 | wire non_atm_req_0d; | |
329 | assign non_atm_req_0d = req0_d & ~(atm0_d); | |
330 | ||
331 | wire atm_req_0d; | |
332 | assign atm_req_0d = req0_d & atm0_d; | |
333 | ||
334 | wire pcx_valid0_w; | |
335 | assign pcx_valid0_w = `pcx_valid0; //0in assert_follower -leader non_atm_req0 -follower pcx_valid0_w -min 1 -max 1 | |
336 | ||
337 | ||
338 | //check that non_atm req is always followed by valid pcx packet | |
339 | //x0in assert_follower -ldr non_atm_req0 -flwr pcx_valid0_w -min 1 -max 1 -module l2_pcx_protocol | |
340 | ||
341 | //check that atomic_req is always followed by valid pcx packet | |
342 | //0in assert_follower -ldr atm_req0 -flwr `pcx_valid0 -min 1 -max 1 | |
343 | ||
344 | ||
345 | ||
346 | ||
347 | //atomic transition state machine | |
348 | reg [3:0] atm_curr, atm_nxt; | |
349 | parameter [3:0] idle = 1, req = 2, atmReq0 = 4, atmReq1 = 8; | |
350 | always @( `req0 or `atm0 or `pcx_valid0 or atm_curr or `rst) | |
351 | begin | |
352 | case (atm_curr) | |
353 | idle: | |
354 | begin | |
355 | if( ~`rst ) | |
356 | atm_nxt = idle; | |
357 | if( `req0 & `atm0) | |
358 | atm_nxt = atmReq0; | |
359 | else if( `req0 & ~(`atm0) ) | |
360 | atm_nxt = req; | |
361 | else | |
362 | atm_nxt = atm_curr; | |
363 | end | |
364 | req: | |
365 | begin | |
366 | if( `req0 & `atm0) | |
367 | atm_nxt = atmReq0; | |
368 | else if ( `req0 & ~(`atm0) ) | |
369 | atm_nxt = req; | |
370 | else | |
371 | atm_nxt = idle; | |
372 | end | |
373 | atmReq0: | |
374 | begin | |
375 | if( `req0 & (~`atm0) ) | |
376 | atm_nxt = atmReq1; | |
377 | else | |
378 | atm_nxt = atm_curr; | |
379 | end | |
380 | atmReq1: | |
381 | begin | |
382 | if( `req0 & (~`atm0)) | |
383 | atm_nxt = req; | |
384 | else if ( `req0 & `atm0 ) | |
385 | atm_nxt = atmReq1; | |
386 | else | |
387 | atm_nxt = idle; | |
388 | end | |
389 | default: | |
390 | begin | |
391 | //0in fire -message " should never reach this state" | |
392 | end | |
393 | endcase | |
394 | end | |
395 | ||
396 | always @(posedge `clk or `rst ) | |
397 | begin | |
398 | if (~`rst) | |
399 | atm_curr = 2'b00; | |
400 | else | |
401 | atm_curr = atm_nxt; | |
402 | end | |
403 | ||
404 | //make sure that the pcx interface is not stuck | |
405 | //0in timeout -val 1000 -var atm_curr[2] | |
406 | //0in timeout -val 1000 -var atm_curr[3] | |
407 | ||
408 | //make sure that their no intervening transaction between atomic packets | |
409 | ||
410 | reg atomic_broken; | |
411 | ||
412 | always @( atm_curr[3] ) | |
413 | begin | |
414 | if( cpu_id_d != cpu_id_dd ) | |
415 | atomic_broken = 1'b1; //0in fire -message "atomicity broken on pcx to l2 atomic transaction" | |
416 | end | |
417 | ||
418 | ||
419 | endmodule | |
420 | */ |