../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: