// svGolf task `sorter`, reference: a streaming insertion-cell sorter ("cell sort"), adapted from a
// real-world design.
//
// PROVENANCE. Adapted from andrewpeck/cell-sort, https://github.com/andrewpeck/cell-sort, commit
// cfc46709eaa911858136c2300327ca73bf1eb9a0, files cell_sort.sv and unit_cell.sv, MIT License,
// Copyright (c) 2024-2025 Andrew Peck (the notice is kept below, as the license requires). Kept
// from upstream: the cell rule. On an input, a cell takes its upper neighbour's value when that
// neighbour is pushed (input > neighbour), else the input when the input beats its own value
// (input > own), else it holds; the top ("best") cell is never pushed into; the reset clears every
// cell to 0, written after the cell's other writes so that it overrides them. CHANGES, with reasons:
//  1. One module `sorter #(N, W)` with the C8 ports (Spec.lean): DEPTH -> N, SORTB -> W,
//     data_i -> in_data, dav_i -> in_valid. METAB/metadata and REV are dropped: they are not in the
//     interface, and REV = 0 is the ascending order. `start` is not read (TIMING below).
//  2. unit_cell is inlined into a generate family of cells 0 .. N-2 plus the top cell N-1, cell k's
//     value at data[k*W +: W] of one flat vector: the statement is about flat designs, and ls-sv's
//     extractor refuses the upstream's unpacked port and wire arrays (measured).
//  3. The wires `comparator`, `neighbor_push_o` and the continuous assigns are inlined into the
//     always_ff bodies: the clock-step theorem's FF-only profile has always_ff processes only.
//  4. NEW streaming output (upstream: all cells in parallel on data_o[DEPTH]; C8 streams). When
//     in_valid = 0 every cell takes its upper neighbour's value and the top cell takes 0, the
//     upstream's empty value: the minimum leaves through cell 0 into out_data, one per cycle.
//  5. NEW valid token tok[k], one bit per cell, shifted down every cycle with in_valid entering at
//     the top: out_valid is in_valid delayed by N cycles. Upstream has no output valid.
//  6. Dropped: `updating` (a net assigned in always_ff, a slang error, and connected out of range
//     at updating[DEPTH]) and `resetall (refused by the source gate).
//
// INVARIANT. Let a start be sampled at entry s and x_0 .. x_{N-1} be in_data at entries s+1 .. s+N.
// Read the cells bottom-up (cell 0 first) as a list B of N values.
//  - Load: after the edge of entry s+t (0 <= t <= N), B = [0]^(N-t) ++ sortAsc [x_{t-1}, .., x_0].
//    Inserting x at that edge gives B' = tail (insertAsc x B): with q = #{k : B[k] < x}, cells
//    k < q-1 take B[k+1], cell q-1 takes x, cells k >= q hold; the dropped head is a padding 0 while
//    t < N, and x = 0 changes nothing, as tail (insertAsc 0 B) = B. The ties land where Spec.lean's
//    insertAsc puts them (before the first element the new value is <= to), so the step is
//    insertAsc itself; sortAsc (reverse xs) = sortAsc xs (insertions commute) closes the load.
//  - Drain: after the edge of entry s+N+j (1 <= j <= N), out_valid = 1, out_data = S[j-1] and
//    B = S[j..N) ++ [0]^j, where S = sortAsc [x_0, .., x_{N-1}]. So after s+2N every cell is 0.
//  - Token: tok[k] after the edge of entry c is in_valid at entry c-(N-1-k) (0 before that, from
//    the reset), and out_valid after the edge of entry c is in_valid at entry c-N.
//  - Known: reset writes every cell, token and out_valid; out_data is loaded from cell 0 at every
//    edge; every other write reads known state and in_valid/in_data, which the rely makes known.
//
// TIMING. lat(N, W) = 2N. out_valid = 1 exactly at snapshots s+N+1 .. s+2N, consecutive, carrying
// S in order. It is tight for this design: every transaction's last output is at s+2N. Any design
// needs at least 2N-1 (the minimum depends on x_{N-1}, sampled at entry s+N); this one spends one
// cycle on the registered out_data. `start` is not read: under the rely, in_valid = 1 exactly at
// the N entries after each start. Back-to-back (C2/C4, CONTRACT.md point 7): the earliest legal
// next start is entry s+2N+1, and by then the state is the reset state (cells 0, tokens 0), so
// back-to-back starts need nothing. A start during the drain is not Idle (a rely violation, no
// claim); this design would insert its values into the partly drained array.
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule