RTL Review Checklist

    SIMULATION ASKS   does this design do what the testbench expects?
    A REVIEW ASKS     is the testbench expecting the right things, and is
                      there a reachable situation nobody has expected yet?

    [ ] check reset
    [ ] check the FSM
    [ ] check timing
    [ ] check assertions

    CONTRACT, as submitted
    ----------------------
    PURPOSE     accumulate accepted packets into a transfer, decide when
                the transfer is complete, honour the endpoint halt, and
                hand the completion to firmware

    COMPLETION  a transfer ends on a SHORT PACKET -- one strictly shorter
                than the endpoint maximum -- or when the accumulated byte
                count reaches the length firmware asked for

    INPUTS      clk, rst_n, usb_reset
                cfg_we, cfg_maxpkt, cfg_limit     firmware configuration
                pkt_valid, pkt_len                from the packet layer
                halt_set, halt_clr                from the control endpoint
                fw_ack                            firmware consumed it

    OUTPUTS     halted, ep_busy, xfer_done, xfer_bytes, short_pkt
                n_xfer, n_halt                    observation

// =====================================================================
//  usb_ep_xfer -- AS SUBMITTED FOR REVIEW.
//
//  An OUT endpoint's TRANSFER controller: the layer above packet
//  acceptance. It accumulates accepted packets into a USB transfer,
//  decides when the transfer is complete, honours the endpoint halt
//  condition, and hands the completion to firmware.
//
//  CLASSIFICATION: simplified synthesisable teaching RTL, and it is
//  DELIBERATELY DEFECTIVE. This is the version a reviewer receives.
//  It compiles, it lints clean, and it passes the testbench that was
//  submitted with it. Chapter 30.1 works through what is wrong with it;
//  chapter 30.2 works through why the testbench did not say so.
//
//  Do not copy this module. The reviewed version is in section 7.
// =====================================================================
module usb_ep_xfer_before (
  input  wire        clk,
  input  wire        rst_n,
  input  wire        usb_reset,      // one cycle, from the SE0 detector

  // ---- firmware configuration ----
  input  wire        cfg_we,
  input  wire [6:0]  cfg_maxpkt,     // 8, 16, 32 or 64 for full-speed bulk
  input  wire [15:0] cfg_limit,      // the transfer length firmware expects

  // ---- from the packet layer ----
  input  wire        pkt_valid,      // one cycle: a packet was accepted
  input  wire [6:0]  pkt_len,        // 0 .. maxpkt

  // ---- from the control endpoint ----
  input  wire        halt_set,       // SET_FEATURE(ENDPOINT_HALT)
  input  wire        halt_clr,       // CLEAR_FEATURE(ENDPOINT_HALT)

  // ---- to firmware ----
  input  wire        fw_ack,
  output wire        halted,
  output wire        ep_busy,
  output wire        xfer_done,
  output wire [15:0] xfer_bytes,
  output wire        short_pkt,

  output wire [15:0] n_xfer,
  output wire [15:0] n_halt
);

  reg [6:0]  maxpkt;
  reg [15:0] limit;
  reg [15:0] acc;
  reg        halt_r;
  reg        done_r;
  reg        short_r;
  reg [15:0] bytes_r;
  reg [15:0] c_xfer, c_halt;

  wire accept = pkt_valid && !halt_r && (pkt_len != 7'd0);

  wire [15:0] acc_next  = acc + {9'd0, pkt_len};
  wire        is_short  = (pkt_len < maxpkt);
  wire        hit_limit = (acc_next >= limit);
  wire        complete  = accept && (is_short || hit_limit);

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      maxpkt  <= 7'd64;
      limit   <= 16'd0;
      acc     <= 16'd0;
      halt_r  <= 1'b0;
      done_r  <= 1'b0;
      short_r <= 1'b0;
      bytes_r <= 16'd0;
      c_xfer  <= 16'd0;
      c_halt  <= 16'd0;
    end else if (usb_reset) begin
      maxpkt  <= 7'd64;
      limit   <= 16'd0;
      acc     <= 16'd0;
      halt_r  <= 1'b0;
      done_r  <= 1'b0;
      short_r <= 1'b0;
      bytes_r <= 16'd0;
    end else begin
      if (cfg_we) begin
        maxpkt <= cfg_maxpkt;
        limit  <= cfg_limit;
      end

      if (halt_set) begin
        halt_r <= 1'b1;
        c_halt <= c_halt + 16'd1;
      end else if (halt_clr) begin
        halt_r <= 1'b0;
        acc    <= 16'd0;
      end

      if (accept) begin
        if (complete) begin
          bytes_r <= acc_next;
          short_r <= is_short;
          done_r  <= 1'b1;
          acc     <= 16'd0;
          c_xfer  <= c_xfer + 16'd1;
        end else begin
          acc <= acc_next;
        end
      end

      if (fw_ack) done_r <= 1'b0;
    end
  end

  assign halted     = halt_r;
  assign ep_busy    = (bytes_r != 16'd0);
  assign xfer_done  = done_r;
  assign xfer_bytes = bytes_r;
  assign short_pkt  = short_r;
  assign n_xfer     = c_xfer;
  assign n_halt     = c_halt;

endmodule

    INVARIANT          every architectural fact has ONE register that holds
                       it, and every other signal that mentions it is
                       derived from that register
    EVIDENCE           read every output assignment and ask what it is a
                       function of; anything that is a function of two
                       things that "should agree" is the finding
    FAILURE SIGNATURE  the two copies disagree for one cycle, or in one
                       corner, and the symptom is somewhere else entirely
    FALSE CONFIDENCE   "they are always the same" -- which is a claim about
                       every reachable state, and is what needs proving
    NEXT               if they can disagree, ask which one the rest of the
                       design believes

  assign ep_busy    = (bytes_r != 16'd0);

    INVARIANT          a USB bus reset returns the endpoint's DATA state to
                       default and leaves firmware's CONFIGURATION alone
    EVIDENCE           read the reset branch as a LIST and compare it to the
                       state list. Every register is in exactly one of three
                       categories: cleared by both, cleared by one, cleared
                       by neither -- and every one needs a reason.
    FAILURE SIGNATURE  too long: the device loses its configuration on every
                       host suspend/resume, and the failure is attributed to
                       the host
                       too short: stale state survives a reset the host
                       believes has cleaned everything, and the device goes
                       deaf after re-enumeration
    FALSE CONFIDENCE   "the reset list matches the declaration list" -- which
                       checks that nothing was forgotten, not that nothing
                       was added
    NEXT               ask who WROTE each surviving register, and whether
                       that agent knows the reset happened

    end else if (usb_reset) begin
      maxpkt  <= 7'd64;
      limit   <= 16'd0;

    INVARIANT          every simultaneous pair resolves the way the
                       ARCHITECTURE requires, and the resolution appears in
                       exactly one place in the source
    EVIDENCE           enumerate the pairs -- there are not many -- and for
                       each one find the line that decides it
    FAILURE SIGNATURE  rare, load-dependent, and irreproducible on the bench
                       because the bench does one thing per cycle
    FALSE CONFIDENCE   "the if/else covers it" -- an if/else always produces
                       AN answer; the question is whether anybody chose it
    NEXT               if the priority is accidental, ask what the other
                       order would do, and whether anything tests it

    halt_set + halt_clr     BOTH can arrive together: the host can send
                            SET_FEATURE and CLEAR_FEATURE back to back and
                            the control endpoint can present them adjacently.
                            The submitted code writes:

                                if (halt_set) ... else if (halt_clr) ...

                            so SET wins. Nothing says that was chosen, and it
                            is the wrong way round: CLEAR_FEATURE is the
                            host's explicit recovery action, so a halt that
                            coincides with it is stale.   FINDING F5

    pkt_valid + fw_ack      can arrive together, and they touch the same
                            register from opposite directions. The submitted
                            code sets done_r in one branch and clears it in a
                            later statement, so the CLEAR wins -- which here
                            happens to be harmless, because the completion
                            being acknowledged is the one being replaced.
                            Harmless and undocumented is still a finding, at
                            LOW: the next person to touch it has no way to
                            know it was considered.

    INVARIANT          every comparison in the design has been evaluated at
                       both sides of its threshold, and every counted
                       quantity has been evaluated at zero and at its
                       maximum
    EVIDENCE           list the comparisons; there are usually fewer than
                       ten. For each, name the value that makes it flip.
    FAILURE SIGNATURE  size-dependent. Works for every transfer except the
                       ones that are an exact multiple of something.
    FALSE CONFIDENCE   "random testing covers it" -- uniform random over
                       0..64 spends 1.5% of its packets on the two values
                       that matter
    NEXT               if a boundary value is not reachable, ask why, and
                       whether the reason is a configuration constraint
                       nobody has written down

  wire accept = pkt_valid && !halt_r && (pkt_len != 7'd0);

    INVARIANT          every architectural resource that can be occupied is
                       eventually released, and every producer that is
                       blocked is told so rather than ignored
    EVIDENCE           a progress property with a DERIVED bound, plus a
                       scenario that creates the contention. Data checks
                       cannot supply this: a starved path corrupts nothing.
    FAILURE SIGNATURE  works on the bench, fails under sustained load, and
                       the change that exposed it is unrelated to the change
                       that caused it
    FALSE CONFIDENCE   "every byte that went in came out" -- true, and
                       compatible with half of them never going in
    NEXT               ask what the producer does when the consumer is not
                       ready, and whether "nothing" is one of the answers

    BACKPRESSURE   ep_busy tells the packet layer not to offer. The contract
                   gains a sentence, and the layer below gains an obligation.
    A RECORD       a packet offered anyway is dropped and COUNTED. The
                   contract says that cannot happen, so a non-zero count is
                   a bug somewhere else -- which is exactly why it is a port
                   and not an assertion. An assertion is not present in the
                   field.

    INVARIANT          every contract violation BY ANOTHER BLOCK is
                       recorded, because a violation by somebody else is
                       the hardest kind of failure to attribute
    EVIDENCE           read the contract's "must not" sentences and check
                       that each one has a counter or a sticky bit
    FAILURE SIGNATURE  an escalation that takes a week and ends in "we
                       cannot reproduce it"
    FALSE CONFIDENCE   "there is an assertion for it" -- assertions are not
                       present in silicon
    NEXT               ask who reads the counter, and whether any firmware
                       does

    BLOCKER  can corrupt architectural state or violate the protocol. The
             design cannot tape out.
    HIGH     can lose data, deadlock or starve under a reachable condition.
    MEDIUM   reduces observability, or makes a correct behaviour depend on
             an assumption nobody has written down.
    LOW      maintainability, with no demonstrated functional consequence.

    ID  SEV      FINDING                                        REVIEW ITEM
    --  -------  ---------------------------------------------  -----------
    F1  BLOCKER  a USB bus reset clears maxpkt and limit, which  Q3 reset
                 firmware wrote and the host's reset does not
                 revoke. The endpoint silently reverts to a
                 64-byte maximum and a zero limit.

    F2  BLOCKER  a zero-length packet is not accepted, so a       Q6 boundary
                 transfer whose length is an exact multiple of
                 maxpkt never terminates.

    F3  HIGH     a completion is overwritten if firmware has not  Q7 liveness
                 acknowledged the previous one. No backpressure   Q8 observ.
                 and no record.

    F4  HIGH     clearing a halt abandons the accumulator but     Q2 state
                 leaves the pending completion and its byte
                 count behind, so the next transfer can report
                 the abandoned one's length.

    F5  MEDIUM   halt_set and halt_clr in the same cycle resolve  Q5 collision
                 by coding order rather than by decision, and
                 the order is the wrong one.

    F6  MEDIUM   ep_busy is derived from bytes_r rather than      Q2 state
                 from the authoritative done_r. Masked by F2;
                 becomes reachable when F2 is fixed.

// =====================================================================
//  usb_ep_xfer -- AFTER REVIEW.
//
//  The same hardware contract as the submitted version, with the six
//  findings of chapter 30.1 closed. Every change carries the [Fn] of
//  the finding it answers, so the diff reads as a review record.
//
//  CLASSIFICATION: simplified synthesisable teaching RTL. It is not a
//  USB endpoint. There is no packet RAM, no serial interface engine, no
//  data toggle (29.5 owns that) and no IN direction. It is the TRANSFER
//  layer: the part that turns a sequence of accepted packets into one
//  event firmware is told about.
//
//  THE CONTRACT
//  ------------
//  PURPOSE     accumulate accepted packets into a transfer, decide when
//              the transfer is complete, honour the endpoint halt, and
//              hand the completion to firmware exactly once
//
//  COMPLETION  a transfer ends on a SHORT PACKET -- one strictly shorter
//              than the endpoint maximum, and a zero-length packet is
//              the canonical case -- or when the accumulated byte count
//              reaches the length firmware asked for. First one wins.
//
//  OWNERSHIP   a completion is held until fw_ack. While one is held the
//              endpoint asserts ep_busy and the packet layer must not
//              offer another packet. A packet offered anyway is a
//              contract violation BY THE LAYER BELOW: it is dropped and
//              counted, never allowed to overwrite unread data.
//
//  RESET       rst_n      everything, configuration included
//              usb_reset  the data state only. NOT maxpkt/limit, which
//                         firmware wrote and the host's reset does not
//                         revoke; NOT the counters, which are
//                         diagnostics rather than state.
//
//  PRIORITY    rst_n beats everything; usb_reset beats every input;
//              halt_clr beats halt_set. See the assignment for why.
//
//  ASSUMPTION  cfg_limit + cfg_maxpkt - 1 must fit in 16 bits, i.e.
//              cfg_limit <= 65472 at the largest full-speed bulk
//              maximum. NOTHING IN THIS MODULE CHECKS THAT. It is
//              recorded here because an undocumented constraint is the
//              seventh finding in 30.1 -- and it is not a defect, it is
//              a missing sentence.
// =====================================================================
module usb_ep_xfer (
  input  wire        clk,
  input  wire        rst_n,
  input  wire        usb_reset,

  input  wire        cfg_we,
  input  wire [6:0]  cfg_maxpkt,
  input  wire [15:0] cfg_limit,

  input  wire        pkt_valid,
  input  wire [6:0]  pkt_len,

  input  wire        halt_set,
  input  wire        halt_clr,

  input  wire        fw_ack,
  output wire        halted,
  output wire        ep_busy,
  output wire        xfer_done,
  output wire [15:0] xfer_bytes,
  output wire        short_pkt,

  output wire [15:0] n_xfer,
  output wire [15:0] n_halt,
  // [F3] A packet arrived while a completion was still pending. The
  // contract says the layer below must not do that, so a non-zero value
  // here is a bug SOMEWHERE ELSE -- which is exactly why it is a port
  // and not an assertion.
  output wire [15:0] n_lost
);

  reg [6:0]  maxpkt;
  reg [15:0] limit;
  reg [15:0] acc;
  reg        halt_r;
  reg        done_r;
  reg        short_r;
  reg [15:0] bytes_r;
  reg [15:0] c_xfer, c_halt, c_lost;

  // [F6] Busy IS the completion flag. Deriving it from bytes_r != 0 is
  // a second source of truth for one fact, and the two disagree exactly
  // when a transfer completes with zero bytes -- which, once [F2] is
  // fixed, is an ordinary transfer rather than an impossibility.
  // ONE name for "a completion is pending", and everything -- the
  // output port, the accept gate and the drop detector -- reads it.
  wire busy_i = done_r;
  assign ep_busy = busy_i;

  // [F2] A zero-length packet is a PACKET. It is how a transfer whose
  // length is an exact multiple of the maximum packet size is
  // terminated, and dropping it hangs that transfer forever.
  wire offered = pkt_valid && !halt_r;
  wire accept  = offered && !busy_i;
  wire dropped = offered &&  busy_i;

  wire [15:0] acc_next  = acc + {9'd0, pkt_len};
  wire        is_short  = (pkt_len < maxpkt);
  wire        hit_limit = (acc_next >= limit);
  wire        complete  = accept && (is_short || hit_limit);

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      maxpkt  <= 7'd64;
      limit   <= 16'd0;
      acc     <= 16'd0;
      halt_r  <= 1'b0;
      done_r  <= 1'b0;
      short_r <= 1'b0;
      bytes_r <= 16'd0;
      c_xfer  <= 16'd0;
      c_halt  <= 16'd0;
      c_lost  <= 16'd0;
    end else if (usb_reset) begin
      // [F1] maxpkt and limit are absent from this list on purpose.
      acc     <= 16'd0;
      halt_r  <= 1'b0;
      done_r  <= 1'b0;
      short_r <= 1'b0;
      bytes_r <= 16'd0;
    end else begin
      if (cfg_we) begin
        maxpkt <= cfg_maxpkt;
        limit  <= cfg_limit;
      end

      // [F5] The collision is resolved once, in one place, and in the
      // direction the architecture requires: CLEAR_FEATURE is the host's
      // explicit recovery action, so a halt request arriving in the same
      // cycle is stale and loses. Written the other way round the
      // priority is whatever the author typed first, and nobody reading
      // it can tell that a decision was made.
      if (halt_clr) begin
        // [F4] Clearing a halt abandons the whole transfer, which means
        // the PENDING COMPLETION as well as the accumulator. Leaving
        // bytes_r and done_r behind lets the next transfer report the
        // abandoned one's length.
        halt_r  <= 1'b0;
        acc     <= 16'd0;
        done_r  <= 1'b0;
        short_r <= 1'b0;
        bytes_r <= 16'd0;
      end else if (halt_set) begin
        halt_r  <= 1'b1;
        c_halt  <= c_halt + 16'd1;
      end else begin
        if (accept) begin
          if (complete) begin
            bytes_r <= acc_next;
            short_r <= is_short;
            done_r  <= 1'b1;
            acc     <= 16'd0;
            c_xfer  <= c_xfer + 16'd1;
          end else begin
            acc <= acc_next;
          end
        end
        // [F3] A completion is never overwritten. fw_ack releases the
        // slot; a packet offered while it is occupied is dropped and
        // recorded rather than silently replacing data firmware has not
        // read yet.
        if (fw_ack)  done_r <= 1'b0;
        if (dropped) c_lost <= c_lost + 16'd1;
      end
    end
  end

  assign halted     = halt_r;
  assign xfer_done  = done_r;
  assign xfer_bytes = bytes_r;
  assign short_pkt  = short_r;
  assign n_xfer     = c_xfer;
  assign n_halt     = c_halt;
  assign n_lost     = c_lost;

endmodule

// =====================================================================
//  usb_ep_xfer_sv -- AFTER REVIEW, in SystemVerilog.
//
//  Identical hardware contract to usb_ep_xfer.v: same ports, same
//  completion rule, same reset scopes, same same-cycle priorities, same
//  one-clock latency.
//
//  The reason this version exists in a REVIEW chapter is that one of
//  the six findings stops being possible here. Finding F1 -- a USB bus
//  reset that also clears the endpoint configuration -- is a reset list
//  with one line too many. Gather exactly the fields a bus reset clears
//  into a type, and there is no list to get wrong:
//
//      d <= '0;
//
//  maxpkt and limit are not members, so they cannot be cleared here by
//  accident. A reviewer reading this file does not have to check a list
//  against another list; they have to check one type declaration.
//
//  This is worth stating precisely, because the opposite claim is a
//  common and damaging one: a stronger type removes a CLASS OF MISTAKE
//  from the code. It does not verify the design. F2 through F6 are all
//  still perfectly expressible here.
// =====================================================================
module usb_ep_xfer_sv (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        usb_reset,

  input  logic        cfg_we,
  input  logic [6:0]  cfg_maxpkt,
  input  logic [15:0] cfg_limit,

  input  logic        pkt_valid,
  input  logic [6:0]  pkt_len,

  input  logic        halt_set,
  input  logic        halt_clr,

  input  logic        fw_ack,
  output logic        halted,
  output logic        ep_busy,
  output logic        xfer_done,
  output logic [15:0] xfer_bytes,
  output logic        short_pkt,

  output logic [15:0] n_xfer,
  output logic [15:0] n_halt,
  output logic [15:0] n_lost
);

  // Exactly the state a USB bus reset returns to default, and nothing
  // else. Every field resets to zero, which is why the whole reset is
  // one assignment.
  typedef struct packed {
    logic [15:0] acc;
    logic [15:0] bytes;
    logic        halt;
    logic        done;
    logic        short_f;
  } ep_data_t;

  localparam int EP_DATA_W = 16 + 16 + 3;

  ep_data_t    d;
  logic [6:0]  maxpkt;       // NOT in ep_data_t: firmware owns it
  logic [15:0] limit;        // NOT in ep_data_t
  logic [15:0] c_xfer, c_halt, c_lost;

  logic        busy_i, offered, accept, dropped, is_short, hit_limit, complete;
  logic [15:0] acc_next;

  // [F6] ONE name for "a completion is pending", read by the output
  // port, the accept gate and the drop detector alike.
  assign busy_i    = d.done;
  assign ep_busy   = busy_i;
  assign offered   = pkt_valid && !d.halt;
  assign accept    = offered && !busy_i;           // [F2] no length guard
  assign dropped   = offered &&  busy_i;           // [F3]
  assign acc_next  = d.acc + {9'd0, pkt_len};
  assign is_short  = (pkt_len < maxpkt);
  assign hit_limit = (acc_next >= limit);
  assign complete  = accept && (is_short || hit_limit);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      d      <= '0;
      maxpkt <= 7'd64;
      limit  <= '0;
      c_xfer <= '0; c_halt <= '0; c_lost <= '0;
    end else if (usb_reset) begin
      d <= '0;                                     // [F1] nothing to get wrong
    end else begin
      if (cfg_we) begin
        maxpkt <= cfg_maxpkt;
        limit  <= cfg_limit;
      end

      // [F5] one expression, and the clear wins because CLEAR_FEATURE is
      // the host's explicit recovery action.
      if (halt_clr) begin
        // [F4] the pending completion is part of the abandoned transfer
        d <= '0;
      end else if (halt_set) begin
        d.halt <= 1'b1;
        c_halt <= c_halt + 16'd1;
      end else begin
        if (accept) begin
          if (complete) begin
            d.bytes   <= acc_next;
            d.short_f <= is_short;
            d.done    <= 1'b1;
            d.acc     <= '0;
            c_xfer    <= c_xfer + 16'd1;
          end else begin
            d.acc <= acc_next;
          end
        end
        if (fw_ack)  d.done <= 1'b0;
        if (dropped) c_lost <= c_lost + 16'd1;
      end
    end
  end

  assign halted     = d.halt;
  assign xfer_done  = d.done;
  assign xfer_bytes = d.bytes;
  assign short_pkt  = d.short_f;
  assign n_xfer     = c_xfer;
  assign n_halt     = c_halt;
  assign n_lost     = c_lost;

`ifdef SVA_ON
  // ---------------------------------------------------------------
  //  Nine properties, each written against ONE review question from
  //  chapter 30.1. Icarus Verilog 13.0 rejects concurrent assertions,
  //  so under Icarus each is enforced by the named procedural check.
  // ---------------------------------------------------------------

  // [F3] SAFETY -- "can unread data be overwritten?"
  property p_no_overwrite;
    @(posedge clk) disable iff (!rst_n) accept |-> !d.done;
  endproperty
  a_no_overwrite: assert property (p_no_overwrite);

  // [F3] SAFETY -- a packet offered into a full slot is recorded, not
  // silently absorbed. The counter is the evidence the FIELD will have.
  property p_drop_is_recorded;
    @(posedge clk) disable iff (!rst_n)
      dropped |=> (c_lost == $past(c_lost) + 16'd1);
  endproperty
  a_drop_is_recorded: assert property (p_drop_is_recorded);

  // [F6] CONSISTENCY -- "is this derived, or is it a second copy?"
  property p_busy_is_done;
    @(posedge clk) disable iff (!rst_n) ep_busy == xfer_done;
  endproperty
  a_busy_is_done: assert property (p_busy_is_done);

  // [F2] BOUNDARY -- a zero-length packet is a packet, and it always
  // terminates the transfer because zero is shorter than every legal
  // maximum. This is the assertion that fails on the submitted design.
  property p_zlp_completes;
    @(posedge clk) disable iff (!rst_n)
      (accept && pkt_len == 7'd0) |=> d.done;
  endproperty
  a_zlp_completes: assert property (p_zlp_completes);

  // [F1] RESET SCOPE -- two obligations, and the second is the one that
  // gets left out: what a bus reset must NOT touch.
  property p_bus_reset_scope;
    @(posedge clk) disable iff (!rst_n)
      usb_reset |=> (d == {EP_DATA_W{1'b0}}) &&
                    (maxpkt == $past(maxpkt)) && (limit == $past(limit));
  endproperty
  a_bus_reset_scope: assert property (p_bus_reset_scope);

  // [F5] COLLISION -- the priority is a property, not a coding order.
  property p_clear_beats_set;
    @(posedge clk) disable iff (!rst_n)
      (halt_set && halt_clr) |=> !d.halt;
  endproperty
  a_clear_beats_set: assert property (p_clear_beats_set);

  // [F4] RESIDUE -- clearing a halt abandons the whole transfer.
  property p_unhalt_abandons_all;
    @(posedge clk) disable iff (!rst_n)
      halt_clr |=> (d.acc == '0) && (d.bytes == '0) && !d.done;
  endproperty
  a_unhalt_abandons_all: assert property (p_unhalt_abandons_all);

  // STABILITY -- a completion firmware has not read does not change
  // underneath it.
  property p_completion_stable;
    @(posedge clk) disable iff (!rst_n)
      (d.done && !fw_ack && !halt_clr && !usb_reset) |=> $stable(d.bytes);
  endproperty
  a_completion_stable: assert property (p_completion_stable);

  // PROGRESS -- the slot is released by the acknowledgement, in one
  // cycle, so a firmware that acknowledges cannot be blocked by this
  // module. Note the antecedent: it does not claim firmware WILL
  // acknowledge, which is not this module's obligation.
  property p_ack_releases;
    @(posedge clk) disable iff (!rst_n)
      (d.done && fw_ack && !halt_clr && !usb_reset) |=> !d.done;
  endproperty
  a_ack_releases: assert property (p_ack_releases);

  // COVER -- so that none of the above can pass by never happening.
  c_zlp:        cover property (@(posedge clk) accept && pkt_len == 7'd0);
  c_maxpkt:     cover property (@(posedge clk) accept && pkt_len == maxpkt);
  c_limit_end:  cover property (@(posedge clk) complete && !is_short);
  c_drop:       cover property (@(posedge clk) dropped);
  c_collision:  cover property (@(posedge clk) halt_set && halt_clr);
  c_zero_xfer:  cover property (@(posedge clk) complete && acc_next == '0);
  c_busreset:   cover property (@(posedge clk) usb_reset && (maxpkt != 7'd64));
`endif

endmodule

-- =====================================================================
--  usb_ep_xfer (VHDL-2008) -- AFTER REVIEW.
--
--  Identical hardware contract to the Verilog-2005 and SystemVerilog
--  versions: same ports, same completion rule, same reset scopes, same
--  same-cycle priorities, same one-clock latency.
--
--  Two things VHDL contributes to a REVIEW that the other two do not.
--
--  The data state is a RECORD with a single default constant, so the
--  bus-reset scope is one assignment and finding F1 has no line to hide
--  in -- the same argument as the SystemVerilog struct, reached by a
--  different construct.
--
--  The byte accumulator is a RANGE-CONSTRAINED value. The contract in
--  the Verilog header records an assumption -- that cfg_limit plus
--  cfg_maxpkt minus one fits in sixteen bits -- and records that nothing
--  checks it. Here the range is declared, so the assumption is checked
--  by the simulator at the instant it is violated rather than wrapping
--  quietly. That is the seventh finding of 30.1 answered by a type.
-- =====================================================================
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity usb_ep_xfer is
  port (
    clk        : in  std_logic;
    rst_n      : in  std_logic;
    usb_reset  : in  std_logic;

    cfg_we     : in  std_logic;
    cfg_maxpkt : in  unsigned(6 downto 0);
    cfg_limit  : in  unsigned(15 downto 0);

    pkt_valid  : in  std_logic;
    pkt_len    : in  unsigned(6 downto 0);

    halt_set   : in  std_logic;
    halt_clr   : in  std_logic;

    fw_ack     : in  std_logic;
    halted     : out std_logic;
    ep_busy    : out std_logic;
    xfer_done  : out std_logic;
    xfer_bytes : out unsigned(15 downto 0);
    short_pkt  : out std_logic;

    n_xfer     : out unsigned(15 downto 0);
    n_halt     : out unsigned(15 downto 0);
    n_lost     : out unsigned(15 downto 0)
  );
end entity usb_ep_xfer;

architecture rtl of usb_ep_xfer is

  -- Exactly the state a USB bus reset returns to default, and nothing
  -- else. maxpkt and limit are declared separately, below, because
  -- firmware owns them and the host's reset does not revoke them.
  type ep_data_t is record
    acc     : unsigned(15 downto 0);
    bytes   : unsigned(15 downto 0);
    halt    : std_logic;
    done    : std_logic;
    short_f : std_logic;
  end record ep_data_t;

  constant EP_DATA_RESET : ep_data_t := (
    acc     => (others => '0'),
    bytes   => (others => '0'),
    halt    => '0',
    done    => '0',
    short_f => '0'
  );

  signal d      : ep_data_t := EP_DATA_RESET;
  signal maxpkt : unsigned(6 downto 0)  := to_unsigned(64, 7);
  signal limit  : unsigned(15 downto 0) := (others => '0');

  signal c_xfer, c_halt, c_lost : unsigned(15 downto 0) := (others => '0');

  signal busy_i, offered, accept_s, dropped : std_logic;
  signal is_short, hit_limit, complete  : std_logic;
  -- Seventeen bits so the SUM is representable even when the assumption
  -- in the header is violated; the assertion below is what reports it.
  signal acc_next : unsigned(16 downto 0);

begin

  -- [F6] ONE name for "a completion is pending", read by the output
  -- port, the accept gate and the drop detector alike.
  busy_i   <= d.done;
  ep_busy  <= busy_i;

  offered  <= pkt_valid and (not d.halt);
  accept_s <= offered and (not busy_i);     -- [F2] no length guard
  dropped  <= offered and busy_i;           -- [F3]

  acc_next <= ('0' & d.acc) + resize(pkt_len, 17);

  is_short  <= '1' when pkt_len < maxpkt else '0';
  hit_limit <= '1' when acc_next >= resize(limit, 17) else '0';
  complete  <= accept_s and (is_short or hit_limit);

  seq : process (clk, rst_n)
  begin
    if rst_n = '0' then
      d      <= EP_DATA_RESET;
      maxpkt <= to_unsigned(64, 7);
      limit  <= (others => '0');
      c_xfer <= (others => '0');
      c_halt <= (others => '0');
      c_lost <= (others => '0');
    elsif rising_edge(clk) then
      if usb_reset = '1' then
        d <= EP_DATA_RESET;                 -- [F1] nothing to get wrong
      else
        if cfg_we = '1' then
          maxpkt <= cfg_maxpkt;
          limit  <= cfg_limit;
        end if;

        -- [F5] one decision, one place, and the clear wins because
        -- CLEAR_FEATURE is the host's explicit recovery action.
        if halt_clr = '1' then
          d <= EP_DATA_RESET;               -- [F4] the whole transfer goes
        elsif halt_set = '1' then
          d.halt <= '1';
          c_halt <= c_halt + 1;
        else
          if accept_s = '1' then
            if complete = '1' then
              -- The assumption from the contract, checked rather than
              -- assumed. A limit set too close to the top of the range
              -- stops the simulation here instead of wrapping.
              assert acc_next <= 65535
                report "usb_ep_xfer: cfg_limit + cfg_maxpkt - 1 exceeds 16 bits"
                severity failure;
              d.bytes   <= acc_next(15 downto 0);
              d.short_f <= is_short;
              d.done    <= '1';
              d.acc     <= (others => '0');
              c_xfer    <= c_xfer + 1;
            else
              d.acc <= acc_next(15 downto 0);
            end if;
          end if;
          if fw_ack = '1' then
            d.done <= '0';
          end if;
          if dropped = '1' then
            c_lost <= c_lost + 1;
          end if;
        end if;
      end if;
    end if;
  end process seq;

  halted     <= d.halt;
  xfer_done  <= d.done;
  xfer_bytes <= d.bytes;
  short_pkt  <= d.short_f;
  n_xfer     <= c_xfer;
  n_halt     <= c_halt;
  n_lost     <= c_lost;

end architecture rtl;

              assert acc_next <= 65535
                report "usb_ep_xfer: cfg_limit + cfg_maxpkt - 1 exceeds 16 bits"
                severity failure;

    iverilog -g2005 -DUSE_BEFORE -o bad \
             usb_ep_xfer_before.v usb_ep_xfer.v tb_usb_ep_xfer.v

    ** F1 config survives the bus reset: got 1 expected 0
    ** F2 the ZLP completes it:          got 0 expected 1
    ** F2 byte count:                    got 0 expected 32
    ** F2 reported as short:             got 0 expected 1
    ** F3 first is still there:          got 6 expected 4
    ** F3 the offer was recorded:        got 0 expected 1
    ** F3 slot released:                 got 1 expected 0
    ** F4 completion abandoned too:      got 1 expected 0
    ** F4 byte count cleared:            got 5 expected 0
    ** F5 the clear wins:                got 1 expected 0
    ** F6 zero-byte transfer completed:  got 0 expected 1
    ** F6 and still looks busy:          got 0 expected 1

    phase 1 findings   : 241 checks,    39 errors
    DIRECTED-ONLY      : 2,433 checks, 160 errors
    TOTAL              : 34,449 checks, 19,199 errors

    MUT     REVIEW ITEM                       V-DIR   SV-DIR   VH-DIR    V-ALL
    A-M1    Q3  reset scope                       6        6        6    8,229
    A-M2    Q6  boundary: the ZLP                86       86       86    9,324
    A-M3    Q7  liveness: overwrite              29       29       29    5,398
    A-M4    Q2  residue on abandonment            6        6        6   10,120
    A-M5    Q5  collision: which wins              3        3        3   14,171
    A-M6    Q2  authoritative state             106      106      106   11,046

    1  ARCHITECTURE AND CONTRACT
       [ ] is there a written contract, or only code?
       [ ] does it say what the block ASSUMES about its neighbours?
       [ ] does it say what it deliberately does NOT do?

    2  AUTHORITATIVE STATE
       [ ] one register per architectural fact
       [ ] every output is a function of registers, not of other outputs
       [ ] no signal that "should always agree" with another
       [ ] name the single source of truth so everything reads the same one

    3  RESET SCOPE
       [ ] list every register; put each in: cleared by both / by one / by
           neither, and give a reason for each
       [ ] the bus-reset list is checked in BOTH directions -- too long
           loses configuration, too short leaves stale state
       [ ] who wrote each surviving register, and do they know?

    4  DATA MOVEMENT
       [ ] every value has one path from input to output
       [ ] widths are explicit at every capture
       [ ] every conversion between a number and a bit vector is written

    5  PRIORITY AND COLLISIONS
       [ ] enumerate the input pairs that can arrive together
       [ ] for each: what wins, why, and WHERE is it decided
       [ ] the decision appears exactly once in the source
       [ ] a set and a clear of the same bit COMPOSE rather than race

    6  BOUNDARIES
       [ ] zero, one, max-1, max, max+1 for every counted quantity
       [ ] both sides of every comparison
       [ ] empty, full, one-before-full, one-after-release
       [ ] a zero-length or zero-count case is a CASE, not an absence

    7  LIVENESS
       [ ] every occupiable resource is eventually released
       [ ] every blocked producer is TOLD, not ignored
       [ ] fixed priorities have a bound, or a reason they need none
       [ ] a progress property exists, with a DERIVED bound

    8  OBSERVABILITY
       [ ] every "must not happen" in the contract has a counter
       [ ] the counter survives the reset that does not clear the cause
       [ ] somebody's firmware reads it

    9  EVIDENCE
       [ ] the directed suite passes without random stimulus
       [ ] the suite has been run against a design known to be wrong
       [ ] each finding has a scenario, and each scenario has been shown
           to be the one that catches it

    1  SEVERITY
       Re-rank F1 to F6 for a device that is bus-powered, has no firmware
       update path, and ships in a medical instrument. Which changes, and
       which does not? Justify each move by CONSEQUENCE, not by effort.

    2  THE MASKED FINDING
       F6 is unreachable while F2 is present. Find another pair in the
       submitted module where fixing one changes the reachability of
       another, and say which order a team should fix them in.

    3  THE SEVENTH ITEM
       Write the one sentence that belongs in the module header for the
       undocumented configuration constraint. Then write the assertion.
       Then say which of the two you would insist on in review, and why.

    4  VERILOG
       Add a second completion slot so that one transfer can complete while
       firmware still holds the previous one. State first what ep_busy now
       means, then what n_lost now means, then write it.

    5  SYSTEMVERILOG
       Implement the same two-slot contract. Does the struct still make F1
       impossible? Does it make anything else impossible that it did not
       before?

    6  VHDL
       Implement it, and declare the range of every new counter. Then
       deliberately configure a limit that violates the header's assumption
       and confirm the simulation stops at the violation.

    7  COLLISION AUDIT
       The two-slot version has input pairs the one-slot version does not.
       Enumerate them, decide each one, and say which are new.

    8  REVIEW WRITE-UP
       Write F3 as it would appear in a review tool: question, invariant,
       evidence, failure signature, false confidence, severity, and the
       specific change requested. One screen, no more.

    9  MUTATION PREDICTION
       For each of A-M1 to A-M6, predict whether it is caught by the
       findings phase, the exhaustive sweep, the stream phase, or only by
       random. Then check three. A-M2 and A-M6 are the surprising ones.

    THE PROCEDURE
    o  nine questions, in an order that has dependencies -- architecture,
       state, reset, data, collisions, boundaries, liveness, observability,
       evidence
    o  every item has six parts, and FALSE CONFIDENCE is the one that does
       the work
    o  severity is a claim about consequence, not about effort

    THE FINDINGS THAT GENERALISE
    o  two signals that "should always agree" is a finding; the useful
       question is exactly when they disagree
    o  a reset list is wrong in two directions and both are shipping bugs
    o  an if/else always produces an answer, which is how it hides the
       question of whether anybody chose it
    o  a zero-length case is a CASE, not an absence
    o  a starved path corrupts nothing, so nothing that compares data can
       find it
    o  every "must not happen" in a contract deserves a counter, because an
       assertion is not present in silicon
    o  a constraint that is documented is an assumption; a constraint that
       is checked is not

    THE METHOD
    o  FIXING ONE FINDING CAN REVEAL ANOTHER -- F6 is unreachable until F2
       is fixed -- so review the whole block before changing any of it, and
       record the interaction
    o  a stronger type removes a CLASS of mistake and no more: the struct
       makes F1 unwritable and leaves five findings untouched
    o  run the suite against a design known to be wrong; a checker never
       shown to fail has not been validated
    o  an exhaustive sweep is exhaustive over the axes it HAS, and
       "two things in one cycle" is rarely one of them
    o  a scenario that is the sole detector of a finding is load-bearing,
       measured by deleting it: A-M5 goes from 3 to 0