TLP Generation — One Packet, One Owner, Until EOP

// SYNTHESIZABLE. Normalized internal request and packet metadata.
// NOT a wire layout -- Chapter 11.3 §2 owns the field map. These are the
// values this block freezes at accept and guarantees until EOP.
package tlpgen_pkg;
 
  parameter int ADDR_W = 64;
  parameter int DATA_W = 256;                 // datapath width, bits
  parameter int BYTES  = DATA_W/8;
  parameter int KEEP_W = BYTES;
  parameter int LEN_W  = 13;                  // payload bytes in one packet
  parameter int OFF_W  = (LEN_W > 1) ? LEN_W : 2;
  parameter int TAG_W  = 8;
  parameter int RID_W  = 16;
 
  typedef enum logic [2:0] {
    REQ_MEM_RD = 3'd0,
    REQ_MEM_WR = 3'd1,
    REQ_OTHER  = 3'd2                          // deliberately unsupported (§10)
  } req_kind_e;
 
  typedef struct packed {
    req_kind_e         kind;
    logic [ADDR_W-1:0] addr;
    logic [LEN_W-1:0]  byte_count;
    logic [RID_W-1:0]  requester_id;
    logic [TAG_W-1:0]  tag;
    logic [2:0]        tc;
    logic [3:0]        first_be;               // CARRIED, not derived (§6)
    logic [3:0]        last_be;
  } req_t;
 
  // Guarded so BYTES = 1 is legal: the mask for n bytes, n in 1..BYTES.
  function automatic logic [KEEP_W-1:0] keep_mask(input int unsigned n);
    logic [KEEP_W-1:0] m;
    m = '0;
    for (int i = 0; i < KEEP_W; i++) if (i < n) m[i] = 1'b1;
    return m;
  endfunction
 
  function automatic bit carries_payload(input req_kind_e k);
    return (k == REQ_MEM_WR);
  endfunction
 
endpackage

import tlpgen_pkg::*;
 
// SYNTHESIZABLE. Classification and the encodability precondition (§5).
// This block REPORTS rather than repairs: a byte count that cannot be
// encoded, or a kind this generator does not support, produces an error
// and NO packet -- never a silently rounded or defaulted one.
module tlp_classifier (
  input  req_t  req,
  input  logic  req_present,
 
  output logic  supported,
  output logic  encodable,
  output logic  needs_payload,
  output logic  err_unsupported,
  output logic  err_unencodable
);
  // Chapter 11.3 §5 owns what Length means. What is owned HERE is the
  // precondition: the byte count arriving at this boundary must already
  // be legal. Rounding 6 bytes up to 8 writes two bytes nobody asked for.
  localparam int unsigned MAX_PAYLOAD_BYTES = (1 << LEN_W) - 1;
 
  assign supported     = req_present && (req.kind inside {REQ_MEM_RD, REQ_MEM_WR});
  assign needs_payload = supported && carries_payload(req.kind);
  assign encodable     = supported
                      && (req.byte_count != '0)
                      && (req.byte_count <= LEN_W'(MAX_PAYLOAD_BYTES))
                      && ((req.byte_count[1:0] == 2'b00) || (req.first_be != 4'hF)
                                                          || (req.last_be != 4'hF));
  assign err_unsupported = req_present && !supported;
  assign err_unencodable = supported && !encodable;
endmodule

import tlpgen_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK. The packet owner and header snapshot.
// §12 Model 6: 68.6% of packets experience a stall while a new request is
// already pending upstream. A combinational header takes the NEW values in
// every one of those cycles; this one cannot.
module tlp_packet_owner (
  input  logic clk,
  input  logic rst_n,
 
  input  logic  req_valid,
  output logic  req_ready,
  input  req_t  req,
 
  input  logic  hdr_accepted,          // the header beat transferred
  input  logic  eop_accepted,          // the final payload beat transferred
  input  logic  abort,                 // classifier rejected it
 
  output logic  owner_lock,
  output req_t  pkt,                   // THE SNAPSHOT -- immutable while owned
  output logic  pkt_has_payload,
  output logic  hdr_pending
);
  req_t pkt_q;
  logic own_q, hdr_q;
 
  assign pkt             = pkt_q;
  assign owner_lock      = own_q;
  assign hdr_pending     = hdr_q;
  assign pkt_has_payload = carries_payload(pkt_q.kind);
  // ONE packet at a time (§3). A second request cannot be accepted while
  // this one is owned, which is what makes the snapshot meaningful.
  assign req_ready       = !own_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin own_q <= 1'b0; hdr_q <= 1'b0; pkt_q <= '0; end
    else begin
      if (!own_q) begin
        if (req_valid) begin
          pkt_q <= req;                        // EVERY field, at once
          own_q <= 1'b1;
          hdr_q <= 1'b1;
        end
      end else begin
        if (hdr_accepted) hdr_q <= 1'b0;
        // Released on the ACCEPTED end-of-packet -- not on tx_last being
        // merely asserted (mutation 19), and not on abort mid-packet.
        if (eop_accepted || (abort && hdr_q)) begin
          own_q <= 1'b0; hdr_q <= 1'b0;
        end
      end
      // Nothing above can write pkt_q while own_q is high: the snapshot is
      // immutable by construction, and P3-P9 prove it.
    end
  end
endmodule

import tlpgen_pkg::*;
 
// SYNTHESIZABLE. Multi-beat payload streamer (§7).
// Two measured bugs live here: an all-ones mask on the final beat injected
// 15.5 phantom bytes per packet, and decrementing on `valid` terminated
// 79.1% of stalled packets early. Both are prevented structurally.
module tlp_payload_streamer (
  input  logic clk,
  input  logic rst_n,
 
  input  logic             start,          // header accepted, payload follows
  input  logic [LEN_W-1:0] total_bytes,    // from the SNAPSHOT, not the request
 
  output logic             dat_valid,
  input  logic             dat_ready,
  output logic [KEEP_W-1:0] dat_keep,
  output logic             dat_first,
  output logic             dat_last,
  output logic [OFF_W-1:0] dat_offset,     // byte offset into the payload
 
  output logic             busy,
  output logic             eop_accepted,
  output logic             err_underflow   // sticky
);
  logic [LEN_W-1:0] rem_q;
  logic [OFF_W-1:0] off_q;
  logic             busy_q, first_q, e_q;
  logic [LEN_W-1:0] this_beat;
 
  // The beat is min(remaining, BYTES) -- so the final beat is exactly the
  // tail, and the mask is built from that count rather than defaulted.
  always_comb this_beat = (rem_q > LEN_W'(BYTES)) ? LEN_W'(BYTES) : rem_q;
 
  assign busy         = busy_q;
  assign dat_valid    = busy_q && (rem_q != '0);
  assign dat_keep     = keep_mask(int'(this_beat));      // EXACT, never all-ones
  assign dat_first    = first_q;
  assign dat_last     = busy_q && (rem_q == this_beat);
  assign dat_offset   = off_q;
  assign eop_accepted = dat_valid && dat_ready && dat_last;
  assign err_underflow = e_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rem_q <= '0; off_q <= '0; busy_q <= 1'b0; first_q <= 1'b0; e_q <= 1'b0;
    end else begin
      if (!busy_q) begin
        if (start && (total_bytes != '0)) begin
          rem_q <= total_bytes; off_q <= '0; busy_q <= 1'b1; first_q <= 1'b1;
        end
      end else if (dat_valid && dat_ready) begin
        // ON THE HANDSHAKE ONLY. Decrementing on `valid` ended 79.1% of
        // stalled packets early (§12 Model 7).
        rem_q   <= rem_q - this_beat;
        off_q   <= off_q + OFF_W'(this_beat);
        first_q <= 1'b0;
        if (rem_q == this_beat) busy_q <= 1'b0;
      end
      if (busy_q && (rem_q == '0)) e_q <= 1'b1;    // cannot happen: prove it
    end
  end
endmodule

import tlpgen_pkg::*;
 
// SYNTHESIZABLE. The FSM of Figure 1. It sequences the packet's phases and
// owns nothing else -- the snapshot lives in the owner, the counters live
// in the streamer. Same separation as Chapter 23.3 §3, one level down.
module tlp_gen_fsm (
  input  logic clk,
  input  logic rst_n,
 
  input  logic req_valid,
  input  logic supported,
  input  logic encodable,
  input  logic needs_payload,
  input  logic hdr_accepted,
  input  logic payload_eop_accepted,
 
  output logic hdr_valid,
  output logic payload_start,
  output logic abort,
  output logic err_reported,
  output logic [2:0] state
);
  typedef enum logic [2:0] {
    S_IDLE=3'd0, S_OWN=3'd1, S_HDR=3'd2, S_DATA=3'd3, S_RETIRE=3'd4, S_ERR=3'd5
  } st_e;
  st_e st_q;
 
  assign state         = st_q;
  assign hdr_valid     = (st_q == S_HDR);
  assign payload_start = (st_q == S_HDR) && hdr_accepted && needs_payload;
  assign abort         = (st_q == S_ERR);
  assign err_reported  = (st_q == S_ERR);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) st_q <= S_IDLE;
    else unique case (st_q)
      S_IDLE:   if (req_valid) st_q <= S_OWN;
      // ERROR never passes through the send states: no partial packet (§5).
      S_OWN:    st_q <= (supported && encodable) ? S_HDR : S_ERR;
      S_HDR:    if (hdr_accepted) st_q <= needs_payload ? S_DATA : S_RETIRE;
      S_DATA:   if (payload_eop_accepted) st_q <= S_RETIRE;
      S_RETIRE: st_q <= S_IDLE;
      S_ERR:    st_q <= S_IDLE;
      default:  st_q <= S_IDLE;
    endcase
  end
endmodule

import tlpgen_pkg::*;
 
// VERIFICATION-ONLY. Byte-for-byte payload oracle. It reconstructs what
// left the interface and compares against what the request asked for --
// deliberately from the ACCEPTED beats only, so a design that emits extra
// bytes on a stalled beat cannot hide.
module tlp_payload_oracle (
  input logic clk, rst_n,
  input logic              start,
  input logic [LEN_W-1:0]  total_bytes,
  input logic              dat_valid, dat_ready, dat_last,
  input logic [KEEP_W-1:0] dat_keep,
 
  output logic [LEN_W+4:0] bytes_emitted,
  output logic             err_byte_count,
  output logic             err_extra_beat,
  output logic             err_last_count
);
  logic [LEN_W+4:0] acc_q, exp_q;
  logic [7:0]       lastcnt_q;
  logic             active_q;
 
  assign bytes_emitted = acc_q;
 
  always_comb begin
    err_byte_count = !active_q && (exp_q != '0) && (acc_q != exp_q);
    err_extra_beat = active_q && (acc_q > exp_q);
    err_last_count = (lastcnt_q > 8'd1);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin acc_q<='0; exp_q<='0; lastcnt_q<='0; active_q<=1'b0; end
    else begin
      if (start) begin acc_q<='0; exp_q<={4'd0,total_bytes}; lastcnt_q<='0; active_q<=1'b1; end
      if (dat_valid && dat_ready) begin
        acc_q <= acc_q + ($countones(dat_keep));      // ACCEPTED beats only
        if (dat_last) begin lastcnt_q <= lastcnt_q + 8'd1; active_q <= 1'b0; end
      end
    end
  end
endmodule

// ==================================================================
// OWNERSHIP (§3) -- one packet, one owner, until accepted EOP.
// ==================================================================
 
// P1: the packet is captured exactly once, on the accepted request.
property p_captured_once;
  @(posedge clk) disable iff (!rst_n)
    (pkt != $past(pkt)) |-> $past(req_valid && req_ready);
endproperty
 
// P2: no second request is accepted while a packet is owned.
property p_no_accept_while_owned;
  @(posedge clk) disable iff (!rst_n)
    owner_lock |-> !req_ready;
endproperty
 
// ==================================================================
// HEADER IMMUTABILITY (§4) -- §12 Model 6: 68.6% of packets exposed.
// ==================================================================
 
// P3: the address is stable for the life of the packet.
property p_addr_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> $stable(pkt.addr);
endproperty
 
// P4: the kind is stable -- a packet does not change type mid-flight.
property p_kind_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> $stable(pkt.kind);
endproperty
 
// P5: the byte count is stable.
property p_len_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> $stable(pkt.byte_count);
endproperty
 
// P6: the Requester ID is stable -- it cannot come from the next request.
property p_rid_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> $stable(pkt.requester_id);
endproperty
 
// P7: the Tag is stable. A Tag changing mid-packet breaks correlation for
// the whole transaction (Chapter 11.3 §6).
property p_tag_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> $stable(pkt.tag);
endproperty
 
// P8: byte enables are stable -- they are CARRIED, not re-derived (§6).
property p_be_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> ($stable(pkt.first_be) && $stable(pkt.last_be));
endproperty
 
// P9: traffic class is stable.
property p_tc_stable;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && $past(owner_lock)) |-> $stable(pkt.tc);
endproperty
 
// ==================================================================
// CLASSIFICATION (§5) -- report, never repair.
// ==================================================================
 
// P10: a supported kind is one of the bounded set; anything else errors.
property p_unsupported_reported;
  @(posedge clk) disable iff (!rst_n)
    (req_present && !(req.kind inside {REQ_MEM_RD, REQ_MEM_WR})) |-> err_unsupported;
endproperty
 
// P11: an unencodable byte count is REPORTED, never rounded (§5).
property p_unencodable_reported;
  @(posedge clk) disable iff (!rst_n)
    (supported && !encodable) |-> err_unencodable;
endproperty
 
// P12: an errored request emits NO packet at all -- no partial TLP.
property p_no_partial_packet_on_error;
  @(posedge clk) disable iff (!rst_n)
    (state == 3'd5) |-> (!hdr_valid && !dat_valid);
endproperty
 
// P13: the error state never passes through the send states.
property p_error_bypasses_send;
  @(posedge clk) disable iff (!rst_n)
    ($past(state == 3'd1) && (state == 3'd5)) |-> !$past(hdr_valid);
endproperty
 
// ==================================================================
// PAYLOAD STREAMING (§7).
// ==================================================================
 
// P14: a stalled beat changes nothing.
property p_beat_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (dat_valid && !dat_ready) |=>
      (dat_valid && $stable(dat_keep) && $stable(dat_offset) && $stable(dat_last));
endproperty
 
// P15: remaining decrements ONLY on the handshake. §12 Model 7: on `valid`
// terminated 79.1% of stalled packets early.
property p_offset_on_transfer_only;
  @(posedge clk) disable iff (!rst_n)
    (dat_offset != $past(dat_offset)) |-> $past(dat_valid && dat_ready);
endproperty
 
// P16: the byte-valid mask is EXACT -- never all-ones on a partial beat.
// §12 Model 5: an all-ones final mask injected 15.5 phantom bytes/packet.
property p_keep_exact;
  @(posedge clk) disable iff (!rst_n)
    dat_valid |-> ($countones(dat_keep) == ((rem_q > LEN_W'(BYTES)) ? BYTES : int'(rem_q)));
endproperty
 
// P17: `last` asserts exactly once per packet.
property p_last_once;
  @(posedge clk) disable iff (!rst_n)
    !err_last_count;
endproperty
 
// P18: no beat is emitted after the final one.
property p_no_beat_after_last;
  @(posedge clk) disable iff (!rst_n)
    (dat_valid && dat_ready && dat_last) |=> !dat_valid;
endproperty
 
// P19: the emitted byte count equals the requested byte count, exactly.
property p_byte_conservation;
  @(posedge clk) disable iff (!rst_n)
    !err_byte_count && !err_extra_beat;
endproperty
 
// P20: the owner releases only on the ACCEPTED end of packet.
property p_release_on_accepted_eop;
  @(posedge clk) disable iff (!rst_n)
    $fell(owner_lock) |-> $past(eop_accepted || abort);
endproperty
 
// P21: a read carries no payload phase at all (Chapter 12.1).
property p_read_has_no_payload;
  @(posedge clk) disable iff (!rst_n)
    (owner_lock && (pkt.kind == REQ_MEM_RD)) |-> !dat_valid;
endproperty
 
// ==================================================================
// RESET AND PARAMETERS.
// ==================================================================
 
// P22: reset clears ownership and drives nothing.
property p_reset_clears_owner;
  @(posedge clk)
    (!rst_n) |=> (!owner_lock && !dat_valid && !hdr_valid);
endproperty
 
// P23: a zero byte count never starts a payload phase (it is unencodable).
property p_zero_length_no_payload;
  @(posedge clk) disable iff (!rst_n)
    (start && (total_bytes == '0)) |=> !dat_valid;
endproperty
 
// P24: the streamer never claims to be busy with nothing remaining.
property p_no_busy_with_zero_remaining;
  @(posedge clk) disable iff (!rst_n)
    !err_underflow;
endproperty
 
// P25: the oracle never drives the datapath.
property p_oracle_non_functional;
  @(posedge clk) disable iff (!rst_n)
    $stable({dat_valid, dat_keep}) or !$stable(bytes_emitted);
endproperty