blob: 7c42d77edd3a62f0eb5de44207cc973607b2208e [file] [log] [blame]
// Copyright lowRISC contributors.
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
// Protocol checker for TL-UL ports using assertions. Supports interface-widths
// up to 64bit.
`include "prim_assert.sv"
module tlul_assert #(
parameter EndpointType = "Device" // can be either "Host" or "Device"
) (
input clk_i,
input rst_ni,
// tile link ports
input tlul_pkg::tl_h2d_t h2d,
input tlul_pkg::tl_d2h_t d2h
);
`ifndef VERILATOR
`ifndef SYNTHESIS
`ifdef UVM
import uvm_pkg::*;
`endif
import tlul_pkg::*;
import top_pkg::*;
//////////////////////////////////
// check requests and responses //
//////////////////////////////////
// There are up to 2**TL_AIW possible source-IDs. Below array "pend_req" has one entry
// for each source-ID. Each entry has the following fields:
// - pend : is set to 1 to indicate up to 1 pending request for the source ID
// - opcode : "Get" requires "AccessAckData" response, "Put*" require "AccessAck"
// - size : d_size of response must match a_size of request
// - mask : is used to allow X for bytes whose mask bit is 0
typedef struct packed {
bit pend; // set to 1 to indicate a pending request
tl_a_op_e opcode;
logic [top_pkg::TL_SZW-1:0] size;
logic [top_pkg::TL_DBW-1:0] mask;
} pend_req_t;
pend_req_t [2**TL_AIW-1:0] pend_req;
// set `disable_sva` before testing TLUL error cases
bit disable_sva;
// d_error related SVA doesn't work for xbar, as it doesn't return d_error for protocol errors
// set this to disable the check
bit disable_d_error_sva;
logic [7:0] a_mask, d_mask;
logic [63:0] a_data, d_data;
assign a_mask = 8'(h2d.a_mask);
assign a_data = 64'(h2d.a_data);
assign d_mask = 8'(pend_req[d2h.d_source].mask);
assign d_data = 64'(d2h.d_data);
////////////////////////////////////
// keep track of pending requests //
////////////////////////////////////
// use negedge clk to avoid possible race conditions
always_ff @(negedge clk_i or negedge rst_ni) begin
if (!rst_ni) begin
pend_req <= '0;
end else begin
if (h2d.a_valid) begin
// store each request in pend_req array (we use blocking statements below so
// that we can handle the case where request and response for the same
// source-ID happen in the same cycle)
if (d2h.a_ready) begin
pend_req[h2d.a_source].pend <= 1;
pend_req[h2d.a_source].opcode <= h2d.a_opcode;
pend_req[h2d.a_source].size <= h2d.a_size;
pend_req[h2d.a_source].mask <= h2d.a_mask;
end
end // h2d.a_valid
if (d2h.d_valid) begin
// update pend_req array
if (h2d.d_ready) begin
pend_req[d2h.d_source].pend <= 0;
end
end //d2h.d_valid
end
end
/////////////////////////////////////////
// define sequences for request checks //
/////////////////////////////////////////
sequence h2d_pre_S;
h2d.a_valid;
endsequence
// a_opcode: only 3 opcodes are legal for requests
sequence legalAOpcode_S;
(h2d.a_opcode === PutFullData) ||
(h2d.a_opcode === Get) ||
(h2d.a_opcode === PutPartialData);
endsequence
// a_param is reserved
sequence legalAParam_S;
h2d.a_param === '0;
endsequence
// a_size: Size shouldn't be greater than the bus width in TL-UL (not in TL-UH)
// This assertion can be covered by below
// (a_size must less than or equal to ones of a_mask)
// a_size: 2**a_size must greater than or equal to $countones(a_mask) for PutPartial and Get
sequence sizeGTEMask_S;
(h2d.a_opcode == PutFullData) || ((1 << h2d.a_size) >= $countones(h2d.a_mask));
endsequence
// a_size: 2**a_size must equal to $countones(a_mask) for PutFull
sequence sizeMatchesMask_S;
(h2d.a_opcode inside {PutPartialData, Get}) ||
((1 << h2d.a_size) === $countones(h2d.a_mask));
endsequence
// a_source: there should be no more than one pending request per each source ID
sequence pendingReqPerSrc_S;
pend_req[h2d.a_source].pend == 0;
endsequence
// a_address must be aligned to a_size: a_address & ((1 << a_size) - 1) == 0
sequence addrSizeAligned_S;
(h2d.a_address & ((1 << h2d.a_size)-1)) == '0;
endsequence
// a_mask must be contiguous for Get and PutFullData requests
// the spec talks about "naturally aligned". Does this mean that bit [0] of
// mask is always 1? If that's true, then below code could be much simpler.
// However, the spec shows a timing diagram where bit 0 of mask is 0.
sequence contigMask_pre_S;
h2d.a_opcode != PutPartialData;
endsequence
sequence contigMask_S;
$countones(h2d.a_mask ^ {h2d.a_mask[$bits(h2d.a_mask)-2:0], 1'b0}) <= 2;
endsequence
// a_data must be known for opcode == Put*(depending on mask bits)
sequence aDataKnown_pre_S;
(h2d.a_opcode != Get);
endsequence
sequence aDataKnown_S;
// no check if this lane mask is inactive
((!a_mask[0]) || (a_mask[0] && !$isunknown(a_data[8*0 +: 8]))) &&
((!a_mask[1]) || (a_mask[1] && !$isunknown(a_data[8*1 +: 8]))) &&
((!a_mask[2]) || (a_mask[2] && !$isunknown(a_data[8*2 +: 8]))) &&
((!a_mask[3]) || (a_mask[3] && !$isunknown(a_data[8*3 +: 8]))) &&
((!a_mask[4]) || (a_mask[4] && !$isunknown(a_data[8*4 +: 8]))) &&
((!a_mask[5]) || (a_mask[5] && !$isunknown(a_data[8*5 +: 8]))) &&
((!a_mask[6]) || (a_mask[6] && !$isunknown(a_data[8*6 +: 8]))) &&
((!a_mask[7]) || (a_mask[7] && !$isunknown(a_data[8*7 +: 8])));
endsequence
/////////////////////////////////////////
// define sequences for request checks //
/////////////////////////////////////////
sequence d2h_pre_S;
d2h.d_valid;
endsequence
// d_opcode: if request was Get, then response must be AccessAckData
sequence respOpcode_S;
d2h.d_opcode === ((pend_req[d2h.d_source].opcode == Get) ? AccessAckData : AccessAck);
endsequence
// d_param is reserved
sequence legalDParam_S;
d2h.d_param === '0;
endsequence
// d_size must equal the a_size of the corresponding request
sequence respSzEqReqSz_S;
d2h.d_size === pend_req[d2h.d_source].size;
endsequence
// d_source: each response should have a pending request using same source ID
sequence respMustHaveReq_S;
pend_req[d2h.d_source].pend;
endsequence
// d_data must be known for AccessAckData (depending on mask bits)
sequence dDataKnown_pre_S;
d2h.d_opcode == AccessAckData;
endsequence
sequence dDataKnown_S;
// no check if this lane mask is inactive
((!d_mask[0]) || (d_mask[0] && !$isunknown(d_data[8*0 +: 8]))) &&
((!d_mask[1]) || (d_mask[1] && !$isunknown(d_data[8*1 +: 8]))) &&
((!d_mask[2]) || (d_mask[2] && !$isunknown(d_data[8*2 +: 8]))) &&
((!d_mask[3]) || (d_mask[3] && !$isunknown(d_data[8*3 +: 8]))) &&
((!d_mask[4]) || (d_mask[4] && !$isunknown(d_data[8*4 +: 8]))) &&
((!d_mask[5]) || (d_mask[5] && !$isunknown(d_data[8*5 +: 8]))) &&
((!d_mask[6]) || (d_mask[6] && !$isunknown(d_data[8*6 +: 8]))) &&
((!d_mask[7]) || (d_mask[7] && !$isunknown(d_data[8*7 +: 8])));
endsequence
/////////////////////////////////////////
// define sequences for d_error checks //
/////////////////////////////////////////
sequence d_error_pre_S;
h2d.a_valid && d2h.a_ready;
endsequence
sequence legalAOpcodeErr_S;
!(h2d.a_opcode inside {PutFullData, Get, PutPartialData});
endsequence
sequence sizeGTEMaskErr_S;
(1 << h2d.a_size) < $countones(h2d.a_mask);
endsequence
sequence sizeMatchesMaskErr_S;
(h2d.a_opcode == PutFullData) && ((1 << h2d.a_size) != $countones(h2d.a_mask));
endsequence
sequence addrSizeAlignedErr_S;
(h2d.a_address & ((1 << h2d.a_size)-1)) != '0;
endsequence
///////////////////////////////////
// assemble properties and check //
///////////////////////////////////
// note: use negedge clk to avoid possible race conditions
// in this case all signals coming from the device side have an assumed property
if (EndpointType == "Host") begin : gen_host
// h2d
`ASSERT(legalAOpcode_A, h2d_pre_S |-> legalAOpcode_S, !clk_i, !rst_ni || disable_sva)
`ASSERT(legalAParam_A, h2d_pre_S |-> legalAParam_S, !clk_i, !rst_ni)
`ASSERT(sizeGTEMask_A, h2d_pre_S |-> sizeGTEMask_S, !clk_i, !rst_ni || disable_sva)
`ASSERT(sizeMatchesMask_A, h2d_pre_S |-> sizeMatchesMask_S, !clk_i, !rst_ni || disable_sva)
`ASSERT(pendingReqPerSrc_A, h2d_pre_S |-> pendingReqPerSrc_S, !clk_i, !rst_ni)
`ASSERT(addrSizeAligned_A, h2d_pre_S |-> addrSizeAligned_S, !clk_i, !rst_ni || disable_sva)
`ASSERT(contigMask_A, h2d_pre_S and contigMask_pre_S |-> contigMask_S,
!clk_i, !rst_ni || disable_sva)
`ASSERT(aDataKnown_A, h2d_pre_S and aDataKnown_pre_S |-> aDataKnown_S, !clk_i, !rst_ni)
// d2h
`ASSUME(respOpcode_M, d2h_pre_S |-> respOpcode_S, !clk_i, !rst_ni)
`ASSUME(legalDParam_M, d2h_pre_S |-> legalDParam_S, !clk_i, !rst_ni)
`ASSUME(respSzEqReqSz_M, d2h_pre_S |-> respSzEqReqSz_S, !clk_i, !rst_ni)
`ASSUME(respMustHaveReq_M, d2h_pre_S |-> respMustHaveReq_S, !clk_i, !rst_ni)
`ASSUME(dDataKnown_M, d2h_pre_S and dDataKnown_pre_S |-> dDataKnown_S,
!clk_i, !rst_ni || disable_sva)
// in this case all signals coming from the host side have an assumed property
end else if (EndpointType == "Device") begin : gen_device
// h2d
`ASSUME(legalAParam_M, h2d_pre_S |-> legalAParam_S, !clk_i, !rst_ni)
`ASSUME(pendingReqPerSrc_M, h2d_pre_S |-> pendingReqPerSrc_S, !clk_i, !rst_ni)
`ASSUME(aDataKnown_M, h2d_pre_S and aDataKnown_pre_S |-> aDataKnown_S, !clk_i, !rst_ni)
`ASSUME(contigMask_M, h2d_pre_S and contigMask_pre_S |-> contigMask_S,
!clk_i, !rst_ni || disable_sva)
// d2h
`ASSERT(respOpcode_A, d2h_pre_S |-> respOpcode_S, !clk_i, !rst_ni)
`ASSERT(legalDParam_A, d2h_pre_S |-> legalDParam_S, !clk_i, !rst_ni)
`ASSERT(respSzEqReqSz_A, d2h_pre_S |-> respSzEqReqSz_S, !clk_i, !rst_ni)
`ASSERT(respMustHaveReq_A, d2h_pre_S |-> respMustHaveReq_S, !clk_i, !rst_ni)
`ASSERT(dDataKnown_A, d2h_pre_S and dDataKnown_pre_S |-> dDataKnown_S,
!clk_i, !rst_ni || disable_sva)
// d2h error cases
`ASSERT(legalAOpcodeErr_A, d_error_pre_S and legalAOpcodeErr_S |=>
s_eventually (d2h.d_valid && d2h.d_error), , !rst_ni || disable_d_error_sva)
`ASSERT(sizeGTEMaskErr_A, d_error_pre_S and sizeGTEMaskErr_S |=>
s_eventually (d2h.d_valid && d2h.d_error), , !rst_ni || disable_d_error_sva)
`ASSERT(sizeMatchesMaskErr_A, d_error_pre_S and sizeMatchesMaskErr_S |=>
s_eventually (d2h.d_valid && d2h.d_error), , !rst_ni || disable_d_error_sva)
`ASSERT(addrSizeAlignedErr_A, d_error_pre_S and addrSizeAlignedErr_S |=>
s_eventually (d2h.d_valid && d2h.d_error), , !rst_ni || disable_d_error_sva)
end else begin : gen_unknown
initial begin : p_unknonw
`ASSERT_I(unknownConfig_A, 0 == 1)
end
end
initial begin : p_dbw
// widths up to 64bit / 8 Byte are supported
`ASSERT_I(TlDbw_A, TL_DBW <= 8)
end
// make sure all "pending" bits are 0 at the end of the sim
for (genvar ii = 0; ii < 2**TL_AIW; ii++) begin : gen_assert_final
`ASSERT_FINAL(noOutstandingReqsAtEndOfSim_A, (pend_req[ii].pend == 0))
end
////////////////////////////////////
// additional checks for X values //
////////////////////////////////////
// a_* should be known when a_valid == 1 (a_opcode and a_param are already covered above)
// This also covers ASSERT_KNOWN of a_valid
`ASSERT_KNOWN_IF(aKnown_A, {h2d.a_size, h2d.a_source, h2d.a_address, h2d.a_mask, h2d.a_user},
h2d.a_valid)
// d_* should be known when d_valid == 1 (d_opcode, d_param, d_size already covered above)
// This also covers ASSERT_KNOWN of d_valid
`ASSERT_KNOWN_IF(dKnown_A, {d2h.d_source, d2h.d_sink, d2h.d_error, d2h.d_user}, d2h.d_valid)
// make sure ready is not X after reset
`ASSERT_KNOWN(aReadyKnown_A, d2h.a_ready)
`ASSERT_KNOWN(dReadyKnown_A, h2d.d_ready)
////////////////////////////////////
// SVA coverage //
////////////////////////////////////
`define TLUL_COVER(SEQ) `COVER(``SEQ``_C, ``SEQ``_S, !clk_i, !rst_ni || disable_sva)
// host sends back2back requests
sequence b2bReq_S;
h2d.a_valid && d2h.a_ready ##1 h2d.a_valid;
endsequence
// device sends back2back responses
sequence b2bRsp_S;
d2h.d_valid && h2d.d_ready ##1 d2h.d_valid;
endsequence
// host sends back2back requests with same address
// UVM RAL can't issue this scenario, add this cover to make sure it's tested in some other seq
sequence b2bReqWithSameAddr_S;
bit [top_pkg::TL_AW-1:0] pre_addr;
(h2d.a_valid && d2h.a_ready, pre_addr = h2d.a_address)
##1 h2d.a_valid && pre_addr == h2d.a_address;
endsequence
// a_valid is dropped without a_ready
sequence aValidNotAccepted_S;
h2d.a_valid && !d2h.a_ready ##1 !h2d.a_valid;
endsequence
// d_valid is dropped without a_ready
sequence dValidNotAccepted_S;
d2h.d_valid && !h2d.d_ready ##1 !d2h.d_valid;
endsequence
// host uses same source for back2back items
sequence b2bSameSource_S;
bit [top_pkg::TL_AIW-1:0] pre_source;
(h2d.a_valid && d2h.a_ready, pre_source = h2d.a_source) ##1 h2d.a_valid[->1]
##0 pre_source == h2d.a_source;
endsequence
// a channal content is changed without being accepted
`define TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(NAME) \
sequence a_``NAME``ChangedNotAccepted_S; \
int pre; \
(h2d.a_valid && !d2h.a_ready, pre = h2d.a_``NAME``) ##1 h2d.a_valid[->1] \
##0 pre != h2d.a_``NAME``; \
endsequence \
`TLUL_COVER(a_``NAME``ChangedNotAccepted)
// d channal content is changed without being accepted
`define TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(NAME) \
sequence d_``NAME``ChangedNotAccepted_S; \
int pre; \
(d2h.d_valid && !h2d.d_ready, pre = d2h.d_``NAME``) ##1 d2h.d_valid[->1] \
##0 pre != d2h.d_``NAME``; \
endsequence \
`TLUL_COVER(d_``NAME``ChangedNotAccepted)
if (EndpointType == "Host") begin : gen_host_cov // DUT is host
`TLUL_COVER(b2bRsp)
`TLUL_COVER(dValidNotAccepted)
`TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(data)
`TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(opcode)
`TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(size)
`TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(source)
`TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(sink)
`TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED(error)
end else if (EndpointType == "Device") begin : gen_device_cov // DUT is device
`TLUL_COVER(b2bReq)
`TLUL_COVER(b2bReqWithSameAddr)
`TLUL_COVER(aValidNotAccepted)
`TLUL_COVER(b2bSameSource)
`TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(address)
`TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(data)
`TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(opcode)
`TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(size)
`TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(source)
`TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED(mask)
end else begin : gen_unknown_cov
initial begin : p_unknonw_cov
`ASSERT_I(unknownConfig_A, 0 == 1)
end
end
`ifdef UVM
initial forever begin
bit tlul_assert_en;
uvm_config_db#(bit)::wait_modified(null, "%m", "tlul_assert_en");
if (!uvm_config_db#(bit)::get(null, "%m", "tlul_assert_en", tlul_assert_en)) begin
`uvm_fatal("tlul_assert", "Can't find tlul_assert_en")
end
disable_sva = !tlul_assert_en;
end
initial forever begin
bit tlul_assert_en;
uvm_config_db#(bit)::wait_modified(null, "%m", "tlul_d_error_assert_en");
if (!uvm_config_db#(bit)::get(null, "%m", "tlul_d_error_assert_en", tlul_assert_en)) begin
`uvm_fatal("tlul_assert", "Can't find tlul_d_error_assert_en")
end
disable_d_error_sva = !tlul_assert_en;
end
`endif
`undef TLUL_COVER
`undef TLUL_A_CHAN_CONTENT_CHANGED_WO_ACCEPTED
`undef TLUL_D_CHAN_CONTENT_CHANGED_WO_ACCEPTED
`endif
`endif
endmodule : tlul_assert