../src/lowrisc_tlul_common_0.1/rtl/tlul_assert.sv Cov: 100%
1: // Copyright lowRISC contributors.
2: // Licensed under the Apache License, Version 2.0, see LICENSE for details.
3: // SPDX-License-Identifier: Apache-2.0
4:
5: // Protocol checker for TL-UL ports using assertions. Supports interface-widths
6: // up to 64bit.
7:
8: `include "prim_assert.sv"
9:
10: module tlul_assert #(
11: parameter EndpointType = "Device" // can be either "Host" or "Device"
12: ) (
13: input clk_i,
14: input rst_ni,
15:
16: // tile link ports
17: input tlul_pkg::tl_h2d_t h2d,
18: input tlul_pkg::tl_d2h_t d2h
19: );
20:
21: `ifndef VERILATOR
22: `ifndef SYNTHESIS
23:
24: `ifdef UVM
25: import uvm_pkg::*;
26: `endif
27: import tlul_pkg::*;
28: import top_pkg::*;
29:
30: //////////////////////////////////
31: // check requests and responses //
32: //////////////////////////////////
33:
34: // There are up to 2**TL_AIW possible source-IDs. Below array "pend_req" has one entry
35: // for each source-ID. Each entry has the following fields:
36: // - pend : is set to 1 to indicate up to 1 pending request for the source ID
37: // - opcode : "Get" requires "AccessAckData" response, "Put*" require "AccessAck"
38: // - size : d_size of response must match a_size of request
39: // - mask : is used to allow X for bytes whose mask bit is 0
40: typedef struct packed {
41: bit pend; // set to 1 to indicate a pending request
42: tl_a_op_e opcode;
43: logic [top_pkg::TL_SZW-1:0] size;
44: logic [top_pkg::TL_DBW-1:0] mask;
45: } pend_req_t;
46:
47: pend_req_t [2**TL_AIW-1:0] pend_req;
48:
49: bit disable_sva;
50:
51: logic [7:0] a_mask, d_mask;
52: logic [63:0] a_data, d_data;
53: assign a_mask = 8'(h2d.a_mask);
54: assign a_data = 64'(h2d.a_data);
55: assign d_mask = 8'(pend_req[d2h.d_source].mask);
56: assign d_data = 64'(d2h.d_data);
57:
58: ////////////////////////////////////
59: // keep track of pending requests //
60: ////////////////////////////////////
61:
62: // use negedge clk to avoid possible race conditions
63: always_ff @(negedge clk_i or negedge rst_ni) begin
64: if (!rst_ni) begin
65: pend_req <= '0;
66: end else begin
67: if (h2d.a_valid) begin
68: // store each request in pend_req array (we use blocking statements below so
69: // that we can handle the case where request and response for the same
70: // source-ID happen in the same cycle)
71: if (d2h.a_ready) begin
72: pend_req[h2d.a_source].pend <= 1;
73: pend_req[h2d.a_source].opcode <= h2d.a_opcode;
74: pend_req[h2d.a_source].size <= h2d.a_size;
75: pend_req[h2d.a_source].mask <= h2d.a_mask;
76: end
77: end // h2d.a_valid
78:
79: if (d2h.d_valid) begin
80: // update pend_req array
81: if (h2d.d_ready) begin
82: pend_req[d2h.d_source].pend <= 0;
83: end
84: end //d2h.d_valid
85: end
86: end
87:
88: /////////////////////////////////////////
89: // define sequences for request checks //
90: /////////////////////////////////////////
91:
92: sequence h2d_pre_S;
93: h2d.a_valid;
94: endsequence
95:
96: // a_opcode: only 3 opcodes are legal for requests
97: sequence legalAOpcode_S;
98: (h2d.a_opcode === PutFullData) ||
99: (h2d.a_opcode === Get) ||
100: (h2d.a_opcode === PutPartialData);
101: endsequence
102:
103: // a_param is reserved
104: sequence legalAParam_S;
105: h2d.a_param === '0;
106: endsequence
107:
108: // a_size: Size shouldn't be greater than the bus width in TL-UL (not in TL-UH)
109: // This assertion can be covered by below
110: // (a_size must less than or equal to ones of a_mask)
111:
112: // a_size: 2**a_size must greater than or equal to $countones(a_mask) for PutPartial and Get
113: sequence sizeGTEMask_S;
114: (h2d.a_opcode == PutFullData) || ((1 << h2d.a_size) >= $countones(h2d.a_mask));
115: endsequence
116:
117: // a_size: 2**a_size must equal to $countones(a_mask) for PutFull
118: sequence sizeMatchesMask_S;
119: (h2d.a_opcode inside {PutPartialData, Get}) ||
120: ((1 << h2d.a_size) === $countones(h2d.a_mask));
121: endsequence
122:
123: // a_source: there should be no more than one pending request per each source ID
124: sequence pendingReqPerSrc_S;
125: pend_req[h2d.a_source].pend == 0;
126: endsequence
127:
128: // a_address must be aligned to a_size: a_address & ((1 << a_size) - 1) == 0
129: sequence addrSizeAligned_S;
130: (h2d.a_address & ((1 << h2d.a_size)-1)) == '0;
131: endsequence
132:
133: // a_mask must be contiguous for Get and PutFullData requests
134: // the spec talks about "naturally aligned". Does this mean that bit [0] of
135: // mask is always 1? If that's true, then below code could be much simpler.
136: // However, the spec shows a timing diagram where bit 0 of mask is 0.
137: sequence contigMask_pre_S;
138: h2d.a_opcode != PutPartialData;
139: endsequence
140:
141: sequence contigMask_S;
142: $countones(h2d.a_mask ^ {h2d.a_mask[$bits(h2d.a_mask)-2:0], 1'b0}) <= 2;
143: endsequence
144:
145: // a_data must be known for opcode == Put*(depending on mask bits)
146: sequence aDataKnown_pre_S;
147: (h2d.a_opcode != Get);
148: endsequence
149:
150: sequence aDataKnown_S;
151: // no check if this lane mask is inactive
152: ((!a_mask[0]) || (a_mask[0] && !$isunknown(a_data[8*0 +: 8]))) &&
153: ((!a_mask[1]) || (a_mask[1] && !$isunknown(a_data[8*1 +: 8]))) &&
154: ((!a_mask[2]) || (a_mask[2] && !$isunknown(a_data[8*2 +: 8]))) &&
155: ((!a_mask[3]) || (a_mask[3] && !$isunknown(a_data[8*3 +: 8]))) &&
156: ((!a_mask[4]) || (a_mask[4] && !$isunknown(a_data[8*4 +: 8]))) &&
157: ((!a_mask[5]) || (a_mask[5] && !$isunknown(a_data[8*5 +: 8]))) &&
158: ((!a_mask[6]) || (a_mask[6] && !$isunknown(a_data[8*6 +: 8]))) &&
159: ((!a_mask[7]) || (a_mask[7] && !$isunknown(a_data[8*7 +: 8])));
160: endsequence
161:
162: /////////////////////////////////////////
163: // define sequences for request checks //
164: /////////////////////////////////////////
165:
166: sequence d2h_pre_S;
167: d2h.d_valid;
168: endsequence
169:
170: // d_opcode: if request was Get, then response must be AccessAckData
171: sequence respOpcode_S;
172: d2h.d_opcode === ((pend_req[d2h.d_source].opcode == Get) ? AccessAckData : AccessAck);
173: endsequence
174:
175: // d_param is reserved
176: sequence legalDParam_S;
177: d2h.d_param === '0;
178: endsequence
179:
180: // d_size must equal the a_size of the corresponding request
181: sequence respSzEqReqSz_S;
182: d2h.d_size === pend_req[d2h.d_source].size;
183: endsequence
184:
185: // d_source: each response should have a pending request using same source ID
186: sequence respMustHaveReq_S;
187: pend_req[d2h.d_source].pend;
188: endsequence
189:
190: // d_data must be known for AccessAckData (depending on mask bits)
191: sequence dDataKnown_pre_S;
192: d2h.d_opcode == AccessAckData;
193: endsequence
194:
195: sequence dDataKnown_S;
196: // no check if this lane mask is inactive
197: ((!d_mask[0]) || (d_mask[0] && !$isunknown(d_data[8*0 +: 8]))) &&
198: ((!d_mask[1]) || (d_mask[1] && !$isunknown(d_data[8*1 +: 8]))) &&
199: ((!d_mask[2]) || (d_mask[2] && !$isunknown(d_data[8*2 +: 8]))) &&
200: ((!d_mask[3]) || (d_mask[3] && !$isunknown(d_data[8*3 +: 8]))) &&
201: ((!d_mask[4]) || (d_mask[4] && !$isunknown(d_data[8*4 +: 8]))) &&
202: ((!d_mask[5]) || (d_mask[5] && !$isunknown(d_data[8*5 +: 8]))) &&
203: ((!d_mask[6]) || (d_mask[6] && !$isunknown(d_data[8*6 +: 8]))) &&
204: ((!d_mask[7]) || (d_mask[7] && !$isunknown(d_data[8*7 +: 8])));
205: endsequence
206:
207: ///////////////////////////////////
208: // assemble properties and check //
209: ///////////////////////////////////
210:
211: // note: use negedge clk to avoid possible race conditions
212: // in this case all signals coming from the device side have an assumed property
213: if (EndpointType == "Host") begin : gen_host
214: // h2d
215: `ASSERT(legalAOpcode_A, h2d_pre_S |-> legalAOpcode_S, !clk_i, !rst_ni || disable_sva)
216: `ASSERT(legalAParam_A, h2d_pre_S |-> legalAParam_S, !clk_i, !rst_ni)
217: `ASSERT(sizeGTEMask_A, h2d_pre_S |-> sizeGTEMask_S, !clk_i, !rst_ni || disable_sva)
218: `ASSERT(sizeMatchesMask_A, h2d_pre_S |-> sizeMatchesMask_S, !clk_i, !rst_ni || disable_sva)
219: `ASSERT(pendingReqPerSrc_A, h2d_pre_S |-> pendingReqPerSrc_S, !clk_i, !rst_ni)
220: `ASSERT(addrSizeAligned_A, h2d_pre_S |-> addrSizeAligned_S, !clk_i, !rst_ni || disable_sva)
221: `ASSERT(contigMask_A, h2d_pre_S and contigMask_pre_S |-> contigMask_S,
222: !clk_i, !rst_ni || disable_sva)
223: `ASSERT(aDataKnown_A, h2d_pre_S and aDataKnown_pre_S |-> aDataKnown_S, !clk_i, !rst_ni)
224: // d2h
225: `ASSUME(respOpcode_M, d2h_pre_S |-> respOpcode_S, !clk_i, !rst_ni)
226: `ASSUME(legalDParam_M, d2h_pre_S |-> legalDParam_S, !clk_i, !rst_ni)
227: `ASSUME(respSzEqReqSz_M, d2h_pre_S |-> respSzEqReqSz_S, !clk_i, !rst_ni)
228: `ASSUME(respMustHaveReq_M, d2h_pre_S |-> respMustHaveReq_S, !clk_i, !rst_ni)
229: `ASSUME(dDataKnown_M, d2h_pre_S and dDataKnown_pre_S |-> dDataKnown_S,
230: !clk_i, !rst_ni || disable_sva)
231: // in this case all signals coming from the host side have an assumed property
232: end else if (EndpointType == "Device") begin : gen_device
233: // h2d
234: `ASSUME(legalAOpcode_M, h2d_pre_S |-> legalAOpcode_S, !clk_i, !rst_ni || disable_sva)
235: `ASSUME(legalAParam_M, h2d_pre_S |-> legalAParam_S, !clk_i, !rst_ni)
236: `ASSUME(sizeGTEMask_M, h2d_pre_S |-> sizeGTEMask_S, !clk_i, !rst_ni || disable_sva)
237: `ASSUME(sizeMatchesMask_M, h2d_pre_S |-> sizeMatchesMask_S, !clk_i, !rst_ni || disable_sva)
238: `ASSUME(pendingReqPerSrc_M, h2d_pre_S |-> pendingReqPerSrc_S, !clk_i, !rst_ni)
239: `ASSUME(addrSizeAligned_M, h2d_pre_S |-> addrSizeAligned_S, !clk_i, !rst_ni || disable_sva)
240: `ASSUME(contigMask_M, h2d_pre_S and contigMask_pre_S |-> contigMask_S,
241: !clk_i, !rst_ni || disable_sva)
242: `ASSUME(aDataKnown_M, h2d_pre_S and aDataKnown_pre_S |-> aDataKnown_S, !clk_i, !rst_ni)
243: // d2h
244: `ASSERT(respOpcode_A, d2h_pre_S |-> respOpcode_S, !clk_i, !rst_ni)
245: `ASSERT(legalDParam_A, d2h_pre_S |-> legalDParam_S, !clk_i, !rst_ni)
246: `ASSERT(respSzEqReqSz_A, d2h_pre_S |-> respSzEqReqSz_S, !clk_i, !rst_ni)
247: `ASSERT(respMustHaveReq_A, d2h_pre_S |-> respMustHaveReq_S, !clk_i, !rst_ni)
248: `ASSERT(dDataKnown_A, d2h_pre_S and dDataKnown_pre_S |-> dDataKnown_S,
249: !clk_i, !rst_ni || disable_sva)
250: end else begin : gen_unknown
251: initial begin : p_unknonw
252: `ASSERT_I(unknownConfig_A, 0 == 1)
253: end
254: end
255:
256: initial begin : p_dbw
257: // widths up to 64bit / 8 Byte are supported
258: `ASSERT_I(TlDbw_A, TL_DBW <= 8);
259: end
260:
261: // make sure all "pending" bits are 0 at the end of the sim
262: for (genvar ii = 0; ii < 2**TL_AIW; ii++) begin : gen_assert_final
263: `ASSERT_FINAL(noOutstandingReqsAtEndOfSim_A, (pend_req[ii].pend == 0))
264: end
265:
266: ////////////////////////////////////
267: // additional checks for X values //
268: ////////////////////////////////////
269:
270: // a_* should be known when a_valid == 1 (a_opcode and a_param are already covered above)
271: // This also covers ASSERT_KNOWN of a_valid
272: `ASSERT_KNOWN_IF(aKnown_A, {h2d.a_size, h2d.a_source, h2d.a_address, h2d.a_mask, h2d.a_user},
273: h2d.a_valid)
274:
275: // d_* should be known when d_valid == 1 (d_opcode, d_param, d_size already covered above)
276: // This also covers ASSERT_KNOWN of d_valid
277: `ASSERT_KNOWN_IF(dKnown_A, {d2h.d_source, d2h.d_sink, d2h.d_error, d2h.d_user}, d2h.d_valid)
278:
279: // make sure ready is not X after reset
280: `ASSERT_KNOWN(aReadyKnown_A, d2h.a_ready)
281: `ASSERT_KNOWN(dReadyKnown_A, h2d.d_ready)
282:
283: `ifdef UVM
284: initial forever begin
285: bit tlul_assert_en;
286: uvm_config_db#(bit)::wait_modified(null, "%m", "tlul_assert_en");
287: if (!uvm_config_db#(bit)::get(null, "%m", "tlul_assert_en", tlul_assert_en)) begin
288: `uvm_fatal("tlul_assert", "Can't find tlul_assert_en")
289: end
290: disable_sva = !tlul_assert_en;
291: end
292: `endif
293: `endif
294: `endif
295: endmodule : tlul_assert
296: