Capstone: End-to-End Proof of a Packet Router

module rtr22(input clk, rst,
  input s0_tvalid, input [7:0] s0_tdata, input s0_tdest, output s0_tready,
  input s1_tvalid, input [7:0] s1_tdata, input s1_tdest, output s1_tready,
  output m0_tvalid, output [7:0] m0_tdata, output m0_tid, input m0_tready,
  output m1_tvalid, output [7:0] m1_tdata, output m1_tid, input m1_tready);
  reg [8:0] q0_0 = 0, q0_1 = 0, q1_0 = 0, q1_1 = 0;   // {tid, tdata}; _0 is the head
  reg [1:0] n0 = 0, n1 = 0;                            // entries in each queue
  reg rr0 = 0, rr1 = 0;                                // 1: input 1 goes first at that output
  wire w00 = s0_tvalid && !s0_tdest, w01 = s0_tvalid && s0_tdest;   // input i wants output k
  wire w10 = s1_tvalid && !s1_tdest, w11 = s1_tvalid && s1_tdest;
  // output 0: grant, queue, pop
  wire g00 = w00;                       // bug: input 0 always wins
  wire g10 = w10 && !w00;
  wire p0 = (g00 || g10) && n0 != 2'd2;          // a packet enters queue 0
  wire [8:0] d0 = g00 ? {1'b0, s0_tdata} : {1'b1, s1_tdata};
  wire o0 = m0_tvalid && m0_tready;                  // a packet leaves output 0
  assign m0_tvalid = n0 != 2'd0;
  assign {m0_tid, m0_tdata} = q0_0;
  always @(posedge clk)
    if (rst) begin n0 <= 0; rr0 <= 0; end
    else begin
      if (o0) q0_0 <= q0_1;
      if (p0) begin if (n0 - o0 == 2'd0) q0_0 <= d0; else q0_1 <= d0; end
      if (p0) rr0 <= g00;                           // the other input goes first next time
      n0 <= n0 + p0 - o0;
    end
  // output 1: grant, queue, pop
  wire g01 = w01;                       // bug: input 0 always wins
  wire g11 = w11 && !w01;
  wire p1 = (g01 || g11) && n1 != 2'd2;          // a packet enters queue 1
  wire [8:0] d1 = g01 ? {1'b0, s0_tdata} : {1'b1, s1_tdata};
  wire o1 = m1_tvalid && m1_tready;                  // a packet leaves output 1
  assign m1_tvalid = n1 != 2'd0;
  assign {m1_tid, m1_tdata} = q1_0;
  always @(posedge clk)
    if (rst) begin n1 <= 0; rr1 <= 0; end
    else begin
      if (o1) q1_0 <= q1_1;
      if (p1) begin if (n1 - o1 == 2'd0) q1_0 <= d1; else q1_1 <= d1; end
      if (p1) rr1 <= g01;                           // the other input goes first next time
      n1 <= n1 + p1 - o1;
    end
  assign s0_tready = g00 && n0 != 2'd2 || g01 && n1 != 2'd2;
  assign s1_tready = g10 && n0 != 2'd2 || g11 && n1 != 2'd2;
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire a0 = s0_tvalid && s0_tready, a1 = s1_tvalid && s1_tready;   // a packet is accepted at input i
  // registered copies of the inputs, and the AXI-Stream source rules (IHI 0051B 2.2): TVALID holds, payload stable
  reg h0 = 0, h1 = 0, e0 = 0, e1 = 0;
  reg [7:0] t0 = 0, t1 = 0;
  always @(posedge clk) begin
    h0 <= !rst && s0_tvalid && !s0_tready; h1 <= !rst && s1_tvalid && !s1_tready;
    t0 <= s0_tdata; t1 <= s1_tdata; e0 <= s0_tdest; e1 <= s1_tdest;
  end
  always @(posedge clk) if (!rst) begin
    if (h0) assume(s0_tvalid && s0_tdata == t0 && s0_tdest == e0);
    if (h1) assume(s1_tvalid && s1_tdata == t1 && s1_tdest == e1);
  end
  // packets owed per flow (source i to output k): accepted, not yet left
  reg [1:0] fl00 = 0, fl01 = 0, fl10 = 0, fl11 = 0;
  always @(posedge clk)
    if (rst) begin fl00 <= 0; fl01 <= 0; fl10 <= 0; fl11 <= 0; end
    else begin
      fl00 <= fl00 + (a0 && !s0_tdest) - (o0 && !m0_tid);
      fl01 <= fl01 + (a0 && s0_tdest) - (o1 && !m1_tid);
      fl10 <= fl10 + (a1 && !s1_tdest) - (o0 && m0_tid);
      fl11 <= fl11 + (a1 && s1_tdest) - (o1 && m1_tid);
    end
  // the tracked packet: any accepted packet of input f_src, at a moment the solver picks
  wire f_src = $anyconst;
  wire f_pick = $anyseq;
  reg f_in = 0, f_done = 0, f_dest = 0;
  reg [7:0] f_data = 0;
  reg [1:0] f_ahead = 0;                                   // packets of its flow in front of it
  wire f_acc = f_src ? a1 : a0;
  wire f_tdest = f_src ? s1_tdest : s0_tdest;
  wire [1:0] f_flow = f_src ? (f_tdest ? fl11 : fl10) : (f_tdest ? fl01 : fl00);
  wire f_leave_now = f_tdest ? o1 && m1_tid == f_src : o0 && m0_tid == f_src;
  wire f_lv = f_dest ? o1 && m1_tid == f_src : o0 && m0_tid == f_src;   // a packet of its flow leaves
  wire [7:0] f_out = f_dest ? m1_tdata : m0_tdata;
  wire [1:0] f_room = f_dest ? n1 : n0;
  always @(posedge clk)
    if (rst) begin f_in <= 0; f_done <= 0; end
    else if (!f_in && !f_done && f_acc && f_pick) begin
      f_in <= 1; f_dest <= f_tdest; f_data <= f_src ? s1_tdata : s0_tdata; f_ahead <= f_flow - f_leave_now;
    end else if (f_in && f_lv) begin
      if (f_ahead == 2'd0) begin f_in <= 0; f_done <= 1; end
      else f_ahead <= f_ahead - 2'd1;
    end
  always @(posedge clk) if (!rst) begin
    if (f_in) a_inside: assert(f_room > f_ahead);                        // no drop: still inside
    if (f_in && f_lv && f_ahead == 2'd0) a_turn: assert(f_out == f_data); // its turn: it leaves, unchanged
    a_owed0: assert(!(o0 && (m0_tid ? fl10 : fl00) == 2'd0));            // nothing leaves output 0 unowed
    a_owed1: assert(!(o1 && (m1_tid ? fl11 : fl01) == 2'd0));            // nothing leaves output 1 unowed
  end
`endif
endmodule