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