TL-UL Protocol Checker

TileLink-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 in-flight 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 2^TL_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).