projects / OpenSPARC-T2-DV / blame
? search:
summary | tags | clone url | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Initial commit of OpenSPARC T2 design and verification files.
[OpenSPARC-T2-DV] / verif / env / common / verilog / checkers / dmu / jdia_checkers.v
CommitLineData
86530b38
AT		 1// ========== Copyright Header Begin ==========================================
2//
3// OpenSPARC T2 Processor File: jdia_checkers.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 ============================================
35module jdia_checkers;
36
37`define jdia_top `CPU.dmu
38//`define jdia_clk `jdia_top.iol2clk
39`define jdia_clk `jdia_top.iol2clk
40//`define jdia_rst ~`jdia_top.rst_wmr_
41`define jdia_rst ~`jdia_top.wmr_
42
43
44////////////////////////
45// known/driven checkers
46
47`ifdef X_GUARD
48
49/* 0in known_driven -var `jdia_top.j2d_di_cmd_vld
50 -clock `jdia_clk -reset `jdia_rst */
51/* 0in known_driven -var `jdia_top.j2d_di_cmd
52 -active `jdia_top.j2d_di_cmd_vld
53 -clock `jdia_clk -reset `jdia_rst */
54/* 0in known_driven -var `jdia_top.j2d_di_ctag
55 -active `jdia_top.j2d_di_cmd_vld
56 -clock `jdia_clk -reset `jdia_rst */
57
58/* 0in known_driven -var `jdia_top.j2d_d_data_vld
59 -clock `jdia_clk -reset `jdia_rst */
60/* 0in known_driven -var `jdia_top.j2d_d_data
61 -active `jdia_top.j2d_d_data_vld
62 -clock `jdia_clk -reset `jdia_rst */
63/* 0in known_driven -var `jdia_top.j2d_d_data_par
64 -active `jdia_top.j2d_d_data_vld
65 -clock `jdia_clk -reset `jdia_rst */
66/* 0in known_driven -var `jdia_top.j2d_d_data_err
67 -active `jdia_top.j2d_d_data_vld
68 -clock `jdia_clk -reset `jdia_rst */
69
70/* 0in known_driven -var `jdia_top.j2d_d_wrack_vld
71 -clock `jdia_clk -reset `jdia_rst */
72/* 0in known_driven -var `jdia_top.j2d_d_wrack_tag
73 -active `jdia_top.j2d_d_wrack_vld
74 -clock `jdia_clk -reset `jdia_rst */
75
76/* 0in known_driven -var `jdia_top.j2d_p_cmd_vld
77 -clock `jdia_clk -reset `jdia_rst */
78/* 0in known_driven -var `jdia_top.j2d_p_cmd
79 -active `jdia_top.j2d_p_cmd_vld
80 -clock `jdia_clk -reset `jdia_rst */
81/* 0in known_driven -var `jdia_top.j2d_p_addr
82 -active `jdia_top.j2d_p_cmd_vld
83 -clock `jdia_clk -reset `jdia_rst */
84/* 0in known_driven -var `jdia_top.j2d_p_bmsk
85 -active `jdia_top.j2d_p_cmd_vld
86 -clock `jdia_clk -reset `jdia_rst */
87/* 0in known_driven -var `jdia_top.j2d_p_ctag
88 -active `jdia_top.j2d_p_cmd_vld
89 -clock `jdia_clk -reset `jdia_rst */
90
91/* 0in known_driven -var `jdia_top.d2j_cmd_vld
92 -clock `jdia_clk -reset `jdia_rst */
93/* 0in known_driven -var `jdia_top.d2j_cmd
94 -active `jdia_top.d2j_cmd_vld
95 -clock `jdia_clk -reset `jdia_rst */
96/* 0in known_driven -var `jdia_top.d2j_addr
97 -active `jdia_top.d2j_cmd_vld
98 -clock `jdia_clk -reset `jdia_rst */
99/* 0in known_driven -var `jdia_top.d2j_ctag
100 -active `jdia_top.d2j_cmd_vld
101 -clock `jdia_clk -reset `jdia_rst */
102
103/* 0in known_driven -var `jdia_top.d2j_data_vld
104 -clock `jdia_clk -reset `jdia_rst */
105/* 0in known_driven -var `jdia_top.d2j_data
106 -active `jdia_top.d2j_data_vld
107 -clock `jdia_clk -reset `jdia_rst */
108/* 0in known_driven -var `jdia_top.d2j_data_par
109 -active `jdia_top.d2j_data_vld
110 -clock `jdia_clk -reset `jdia_rst */
111/* 0in known_driven -var `jdia_top.d2j_bmsk
112 -active `jdia_top.d2j_data_vld
113 -clock `jdia_clk -reset `jdia_rst */
114
115/* 0in known_driven -var `jdia_top.d2j_p_wrack_vld
116 -clock `jdia_clk -reset `jdia_rst */
117/* 0in known_driven -var `jdia_top.d2j_p_wrack_tag
118 -active `jdia_top.d2j_p_wrack_vld
119 -clock `jdia_clk -reset `jdia_rst */
120
121/* 0in known_driven -var `jdia_top.j2d_mmu_addr_vld
122 -clock `jdia_clk -reset `jdia_rst */
123/* 0in known_driven -var `jdia_top.j2d_mmu_addr
124 -active `jdia_top.j2d_mmu_addr_vld
125 -clock `jdia_clk -reset `jdia_rst */
126
127`endif // `ifdef X_GUARD
128
129///////////////////////
130// valid value checkers
131
132/* 0in value -var `jdia_top.j2d_p_cmd
133 -val 4'h4 4'h5 4'h6 4'h7 4'hc 4'hd 4'he 4'hf
134 -active `jdia_top.j2d_p_cmd_vld
135 -clock `jdia_clk -reset `jdia_rst */
136
137/* 0in value -var `jdia_top.d2j_cmd
138 -val 4'h0 4'h1 4'h2 4'h3 4'h4 4'h8 4'ha 4'hb
139 -active `jdia_top.d2j_cmd_vld
140 -clock `jdia_clk -reset `jdia_rst */
141
142// d2j_ctag[15] = 0 for dma rd, 1 for dma rds, 0 for int
143
144
145//////////////////
146// parity checkers
147
148/* 0in value -var `jdia_top.j2d_d_data_par[3]
149 -val ~^(`jdia_top.j2d_d_data[127:96])
150 -active `jdia_top.j2d_d_data_vld
151 -clock `jdia_clk -reset `jdia_rst */
152/* 0in value -var `jdia_top.j2d_d_data_par[2]
153 -val ~^(`jdia_top.j2d_d_data[95:64])
154 -active `jdia_top.j2d_d_data_vld
155 -clock `jdia_clk -reset `jdia_rst */
156/* 0in value -var `jdia_top.j2d_d_data_par[1]
157 -val ~^(`jdia_top.j2d_d_data[63:32])
158 -active `jdia_top.j2d_d_data_vld
159 -clock `jdia_clk -reset `jdia_rst */
160/* 0in value -var `jdia_top.j2d_d_data_par[0]
161 -val ~^(`jdia_top.j2d_d_data[31:0])
162 -active `jdia_top.j2d_d_data_vld
163 -clock `jdia_clk -reset `jdia_rst */
164
165/* 0in value -var `jdia_top.j2d_p_data_par[3]
166 -val ~^(`jdia_top.j2d_p_data[127:96])
167 -active `jdia_top.j2d_p_data_vld
168 -clock `jdia_clk -reset `jdia_rst */
169/* 0in value -var `jdia_top.j2d_p_data_par[2]
170 -val ~^(`jdia_top.j2d_p_data[95:64])
171 -active `jdia_top.j2d_p_data_vld
172 -clock `jdia_clk -reset `jdia_rst */
173/* 0in value -var `jdia_top.j2d_p_data_par[1]
174 -val ~^(`jdia_top.j2d_p_data[63:32])
175 -active `jdia_top.j2d_p_data_vld
176 -clock `jdia_clk -reset `jdia_rst */
177/* 0in value -var `jdia_top.j2d_p_data_par[0]
178 -val ~^(`jdia_top.j2d_p_data[31:0])
179 -active `jdia_top.j2d_p_data_vld
180 -clock `jdia_clk -reset `jdia_rst */
181
182/* 0in value -var `jdia_top.d2j_data_par[4]
183 -val ~^(`jdia_top.d2j_data[127:96])
184 -active `jdia_top.d2j_data_vld
185 -clock `jdia_clk -reset `jdia_rst */
186/* 0in value -var `jdia_top.d2j_data_par[3]
187 -val ~^(`jdia_top.d2j_data[95:64])
188 -active `jdia_top.d2j_data_vld
189 -clock `jdia_clk -reset `jdia_rst */
190/* 0in value -var `jdia_top.d2j_data_par[2]
191 -val ~^(`jdia_top.d2j_data[63:32])
192 -active `jdia_top.d2j_data_vld
193 -clock `jdia_clk -reset `jdia_rst */
194/* 0in value -var `jdia_top.d2j_data_par[1]
195 -val ~^(`jdia_top.d2j_data[31:0])
196 -active `jdia_top.d2j_data_vld
197 -clock `jdia_clk -reset `jdia_rst */
198/* 0in value -var `jdia_top.d2j_data_par[0]
199 -val ~^(`jdia_top.d2j_bmsk)
200 -active `jdia_top.d2j_data_vld
201 -clock `jdia_clk -reset `jdia_rst */
202
203
204////////////////////
205// protocol checkers
206
207wire [63:0] dma_wr_current_fifo_entries,
208 dma_rd_current_fifo_entries,
209 interrupt_current_fifo_entries ;
210
211// dma full write / dma partial write
212/* 0in fifo -depth 16
213 -enq ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h0 )
214 | ( `jdia_top.d2j_cmd == 4'h1 ) ) )
215 -deq `jdia_top.j2d_d_wrack_vld
216 -current_fifo_entries dma_wr_current_fifo_entries
217 -name enq_deq_dmawr
218 -clock `jdia_clk
219 -reset `jdia_rst
220 */
221
222// dma read / dma read shared
223/* 0in fifo -depth 16
224 -enq ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h2 )
225 | ( `jdia_top.d2j_cmd == 4'h3 ) ) )
226 -deq ( `jdia_top.j2d_di_cmd_vld & ( ( `jdia_top.j2d_di_cmd == 2'h0 )
227 | ( `jdia_top.j2d_di_cmd == 2'h1 ) ) )
228 -current_fifo_entries dma_rd_current_fifo_entries
229 -name enq_deq_dmard
230 -clock `jdia_clk
231 -reset `jdia_rst
232 */
233
234// interrupt
235/* 0in fifo -depth 4
236 -enq ( `jdia_top.d2j_cmd_vld & ( `jdia_top.d2j_cmd == 4'b0100 ) )
237 -deq ( `jdia_top.j2d_di_cmd_vld & ( ( `jdia_top.j2d_di_cmd == 2'h2 )
238 | ( `jdia_top.j2d_di_cmd == 2'h3 ) ) )
239 -current_fifo_entries interrupt_current_fifo_entries
240 -name enq_deq_int
241 -clock `jdia_clk
242 -reset `jdia_rst
243 */
244
245// sum of dma rd/wr and interrupt entries does not exceed 16
246/* 0in max 16
247 -var ( dma_wr_current_fifo_entries +
248 dma_rd_current_fifo_entries +
249 interrupt_current_fifo_entries )
250 -clock `jdia_clk
251 -reset `jdia_rst
252 */
253
254wire [63:0] pio_wr_current_fifo_entries,
255 pio_rd_current_fifo_entries ;
256
257// pio read
258/* 0in fifo -depth 16
259 -enq ( `jdia_top.j2d_p_cmd_vld & ( ( `jdia_top.j2d_p_cmd == 4'hc )
260 | ( `jdia_top.j2d_p_cmd == 4'hd )
261 | ( `jdia_top.j2d_p_cmd == 4'he )
262 | ( `jdia_top.j2d_p_cmd == 4'hf ) ) )
263 -deq ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h8 )
264 | ( `jdia_top.d2j_cmd == 4'ha )
265 | ( `jdia_top.d2j_cmd == 4'hb ) ) )
266 -current_fifo_entries pio_rd_current_fifo_entries
267 -clock `jdia_clk
268 -reset `jdia_rst
269 */
270
271// pio write
272/* 0in fifo -depth 16
273 -enq ( `jdia_top.j2d_p_cmd_vld & ( ( `jdia_top.j2d_p_cmd == 4'h4 )
274 | ( `jdia_top.j2d_p_cmd == 4'h5 )
275 | ( `jdia_top.j2d_p_cmd == 4'h6 )
276 | ( `jdia_top.j2d_p_cmd == 4'h7 ) ) )
277 -deq `jdia_top.d2j_p_wrack_vld
278 -current_fifo_entries pio_wr_current_fifo_entries
279 -clock `jdia_clk
280 -reset `jdia_rst
281 */
282
283
284// sum of pio rd/wr entries does not exceed 16
285/* 0in max 16
286 -var ( pio_rd_current_fifo_entries +
287 pio_wr_current_fifo_entries )
288 -clock `jdia_clk
289 -reset `jdia_rst
290 */
291
292////////////////
293// data checkers
294
295// dma full write / dma partial write
296/* 0in assert_follower
297 -leader ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h0 )
298 | ( `jdia_top.d2j_cmd == 4'h1 ) ) )
299 -follower `jdia_top.d2j_data_vld
300 -clock `jdia_clk -reset `jdia_rst */
301/* 0in change_window
302 -start ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h0 )
303 | ( `jdia_top.d2j_cmd == 4'h1 ) ) )
304 -stop_count 3
305 -not_in `jdia_top.d2j_data_vld
306 -clock `jdia_clk -reset `jdia_rst */
307
308
309// dma read (no error)
310/* 0in assert_follower
311 -leader ( `jdia_top.j2d_di_cmd_vld & ( `jdia_top.j2d_di_cmd == 2'h0 ) )
312 -follower `jdia_top.j2d_d_data_vld
313 -clock `jdia_clk -reset `jdia_rst */
314/* 0in change_window
315 -start ( `jdia_top.j2d_di_cmd_vld & ( `jdia_top.j2d_di_cmd == 2'h0 ) )
316 -stop_count 3
317 -not_in `jdia_top.j2d_d_data_vld
318 -clock `jdia_clk -reset `jdia_rst */
319
320// pio write
321/* 0in assert_follower
322 -leader ( `jdia_top.j2d_p_cmd_vld & ( ( `jdia_top.j2d_p_cmd == 4'h4 )
323 | ( `jdia_top.j2d_p_cmd == 4'h5 )
324 | ( `jdia_top.j2d_p_cmd == 4'h6 )
325 | ( `jdia_top.j2d_p_cmd == 4'h7 ) ) )
326 -follower `jdia_top.j2d_p_data_vld
327 -clock `jdia_clk -reset `jdia_rst */
328
329// pio read
330/* 0in assert_follower
331 -leader ( `jdia_top.d2j_cmd_vld & ( `jdia_top.d2j_cmd == 4'h8 ) )
332 -follower `jdia_top.d2j_data_vld
333 -clock `jdia_clk -reset `jdia_rst */
334
335
336//////////////////////////
337// transaction id checkers
338
339// dma full write / dma partial write
340/* 0in bus_id
341 -req ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h0 )
342 | ( `jdia_top.d2j_cmd == 4'h1 ) ) )
343 -req_id `jdia_top.d2j_ctag[14:11]
344 -ret `jdia_top.j2d_d_wrack_vld
345 -ret_id `jdia_top.j2d_d_wrack_tag
346 -clock `jdia_clk -reset `jdia_rst */
347
348// dma read / dma read shared
349/* 0in bus_id
350 -req ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h2 )
351 | ( `jdia_top.d2j_cmd == 4'h3 ) ) )
352 -req_id `jdia_top.d2j_ctag[14:11]
353 -ret ( `jdia_top.j2d_di_cmd_vld & ( ( `jdia_top.j2d_di_cmd == 2'h0 )
354 | ( `jdia_top.j2d_di_cmd == 2'h1 ) ) )
355 -ret_id `jdia_top.j2d_di_ctag[14:11]
356 -clock `jdia_clk -reset `jdia_rst */
357
358// pio read
359/* 0in bus_id
360 -req ( `jdia_top.j2d_p_cmd_vld & ( ( `jdia_top.j2d_p_cmd == 4'hc )
361 | ( `jdia_top.j2d_p_cmd == 4'hd )
362 | ( `jdia_top.j2d_p_cmd == 4'he )
363 | ( `jdia_top.j2d_p_cmd == 4'hf ) ) )
364 -req_id `jdia_top.j2d_p_ctag[10:7]
365 -ret ( `jdia_top.d2j_cmd_vld & ( ( `jdia_top.d2j_cmd == 4'h8 )
366 | ( `jdia_top.d2j_cmd == 4'ha )
367 | ( `jdia_top.d2j_cmd == 4'hb ) ) )
368 -ret_id `jdia_top.d2j_ctag[11:8]
369 -clock `jdia_clk -reset `jdia_rst */
370
371// pio write
372/* 0in bus_id
373 -req ( `jdia_top.j2d_p_cmd_vld & ( ( `jdia_top.j2d_p_cmd == 4'h4 )
374 | ( `jdia_top.j2d_p_cmd == 4'h5 )
375 | ( `jdia_top.j2d_p_cmd == 4'h6 )
376 | ( `jdia_top.j2d_p_cmd == 4'h7 ) ) )
377 -req_id `jdia_top.j2d_p_ctag[10:7]
378 -ret `jdia_top.d2j_p_wrack_vld
379 -ret_id `jdia_top.d2j_p_wrack_tag
380 -clock `jdia_clk -reset `jdia_rst */
381
382// interrupt
383///* x0in bus_id
384// -req ( `jdia_top.d2j_cmd_vld & ( `jdia_top.d2j_cmd == 4'b0100 ) )
385// -req_id `jdia_top.d2j_ctag[14:11]
386// -ret ( `jdia_top.j2d_di_cmd_vld & ( ( `jdia_top.j2d_di_cmd == 2'h2 )
387 // | ( `jdia_top.j2d_di_cmd == 2'h3 ) ) )
388// -ret_id `jdia_top.j2d_di_ctag[14:11]
389// -clock `jdia_clk -reset `jdia_rst */
390
391
392endmodule // jdia_checkers
Full OpenSPARC design & verification tarball including full HDL.