// N = 4, BAUD = 1 fits the free depth of 10. With PRO: N = 8, BAUD = 4 at depth 50.
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module uart_tx #(parameter N = 4, parameter BAUD = 1) (input clk, input rst, input start, input [N-1:0] data,
                                                 output reg tx, output busy);
  // frame: start bit (0), N data bits LSB first, stop bit (1); each bit lasts BAUD clock cycles
  reg [N-1:0] sh;
  reg [4:0]   bitn;          // 0 = start bit, 1..N = data bits, N+1 = stop bit
  reg [7:0]   cnt;           // clocks left in the current bit
  reg         active;
  assign busy = active;
  always @(posedge clk)
    if (rst) begin
      active <= 1'b0; tx <= 1'b1;
    end else if (!active) begin
      tx <= 1'b1;
      if (start) begin active <= 1'b1; sh <= data; bitn <= 5'd0; cnt <= BAUD - 1; tx <= 1'b0; end
    end else if (cnt != 0) begin
      cnt <= cnt - 8'd1;
    end else begin
      cnt <= BAUD - 1;
      bitn <= bitn + 5'd1;
      if (bitn < N)       begin tx <= sh[N-1]; sh <= sh << 1; end   // bug: sends MSB first, the spec says LSB first
      else if (bitn == N) tx <= 1'b1;                               // stop bit
      else                begin active <= 1'b0; tx <= 1'b1; end
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the line is high whenever the transmitter is idle
  always @(*) if (!init && !busy) assert (tx == 1'b1);
  // reference model: count clocks since the start of the frame, and remember the data
  reg [7:0] t = 8'd0; reg [N-1:0] ref_d; reg on = 1'b0;
  always @(posedge clk)
    if (rst) on <= 1'b0;
    else if (!busy && start) begin on <= 1'b1; t <= 8'd0; ref_d <= data; end
    else if (on) begin t <= t + 8'd1; if (!busy) on <= 1'b0; end
  // a symbolic data bit index: the tool picks which bit to check
  (* anyconst *) reg [4:0] k;
  always @(*) assume (k < N);
  // start bit, data bit k, stop bit, each held for BAUD cycles
  always @(*) if (!init && on && busy && t < BAUD) assert (tx == 1'b0);
  always @(*) if (!init && on && busy && t >= BAUD * (k + 1) && t < BAUD * (k + 2)) assert (tx == ref_d[k]);
  always @(*) if (!init && on && busy && t >= BAUD * (N + 1) && t < BAUD * (N + 2)) assert (tx == 1'b1);
  // the frame takes exactly N + 2 bit times
  always @(posedge clk) if (!init && on && $past(busy) && !busy) assert (t == BAUD * (N + 2));
`endif
endmodule