# TL-UL Protocol Checker

## Overview

This document details the protocol checker tlul_assert.sv for TL-UL (TileLink Uncached Lightweight), based on TileLink specification version 1.7.1.

The next sections list the checks for each signal of TL-UL channels A and D. More details:

• The source fields (a_source and d_source) identify inflight transactions rather than physical agents. A single agent can use multiple source IDs to track multiple outstanding transactions. See spec section 5.4 “Source and Sink Identifiers” for more details.
• The source fields are TL_AIW bits wide (defined in tlul_pkg.sv). Therefore, there can be up to 2TL_AIW outstanding requests at the same time. To keep track of these outstanding requests, the protocol checker stores pending requests in the array pend_req of depth TL_AIW, and removes them once their corresponding response has been received.
• A request can be responded within the same cycle as the request message is accepted. Therefore, in each clock cycle, the protocol checker first processes requests and thereafter responses.
• The package tlul_pkg.sv defines the structs for channels A and D.
• In below tables, “known” means that a signal should have a value other than X.
• The protocol checker has a parameter EndpointType which can either be "Host" or "Device". The difference between the "Host" and "Device" variant is that some of the properties are formulated as SV assumptions in the former, whereas the same properties are formulated as SV assertions in the latter (and vice versa). The behavior of these two checkers in DV simulations is identical, but in formal verification, this distinction is needed (otherwise some of the assertions would have to be disabled).

## Request Channel (Channel A)

Below table lists all channel A signals and their checks. In "Device" mode some of these properties are assumptions (_M suffix) and in "Host" mode they are assertions (_A suffix).

## Response Channel (Channel D)

Below table lists all channel D signals and their checks. In "Device" mode some of these properties are assertions (_A suffix) and in "Host" mode they are assumptions (_M suffix).

 Signal Checks (assertion name: description) d_opcode respOpcode_[A/M]: If the original request was Get, then the corresponding response must be AccessAckData. Otherwise, the response must be AccessAck. See spec section 6.2. d_param legalDParam_[A/M]: This field is reserved, it must be 0. See spec section 6.2. d_size respSzEqReqSz_[A/M]: The response must have the same size as the original request. See spec section 6.2. d_source respMustHaveReq_[A/M]: For each response, there must have been a corresponding request with the same source ID value. See spec section 5.4. noOutstandingReqsAtEndOfSim_A: Make sure that there are no outstanding requests at the end of the simulation. dKnown_A: Make sure it's not X when d_valid is high. d_sink dKnown_A: Make sure it's not X when d_valid is high. d_data dDataKnown_[A/M]: d_data should not be X for AccessAckData. Bytes of d_data, whose corresponding mask bits of the original request are 0, can be X. See spec section 4.6. d_error dKnown_AMake sure it's not X when d_valid is high. d_user dKnown_AMake sure it's not X when d_valid is high. d_valid dKnown_A: Make sure it's not X (except during reset). d_ready dReadyKnown_AMake sure it's not X (except during reset).