Skip to content

Latest commit

 

History

History
222 lines (210 loc) · 6.71 KB

TlulProtocolChecker.md

File metadata and controls

222 lines (210 loc) · 6.71 KB
Raw

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 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).

Signal Checks (assertion name: description)
a_opcode legalAOpcode_[M/A]: Only the following 3 opcodes are legal: Get, PutFullData, PutPartialData. See spec section 6.2.
a_param legalAParam_[M/A]: This field is reserved, it must be 0. See spec section 6.2.
a_size sizeMatchesMask_[M/A]: a_size can be calculated from a_mask as follows: 2a_size must equal $countones(a_mask). See spec section 4.6.

aKnown_A: Make sure it's not X when a_valid is high.

a_source pendingReqPerSrc_[M/A]: There should be no more than one pending request per each source ID. See spec section 5.4.

aKnown_A: Make sure it's not X when a_valid is high.

a_address addrSizeAligned_[M/A]: a_address must be aligned to a_size: a_address & ((1 << a_size) - 1) == 0. See spec section 4.6.

aKnown_AMake sure it's not X when a_valid is high.

a_mask contigMask_[M/A]: a_mask must be contiguous for Get and PutFullData (but not for PutPartialData). See spec sections 4.6 and 6.2.

sizeMatchesMask_[M/A]: See a_size above.

aKnown_AMake sure it's not X when a_valid is high.

a_data aDataKnown_[M/A]: a_data should not be X for opcodes PutFullData and PutPartialData (it can be X for Get). Bytes of a_data, whose corresponding a_mask bits are 0, can be X. See spec section 4.6.
a_user aKnown_AMake sure it's not X when a_valid is high.
a_valid aKnown_A: Make sure it's not X (except during reset).
a_ready aReadyKnown_A: Make sure it's not X (except during reset).

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).