XON/XOFF Software Flow Control and Its Limits

receiver's buffer fills past its threshold
    -> it TRANSMITS 0x13 on its own transmit line
    -> the far end's software or driver recognises it
    -> the far end stops sending payload

receiver's buffer drains past its resume threshold
    -> it TRANSMITS 0x11
    -> the far end resumes

// Synthesizable SystemVerilog — the receive-side detector. It watches
// completed characters and pauses the local transmitter.

module uart_xon_xoff #(
    parameter logic [7:0] XON  = 8'h11,   // DC1
    parameter logic [7:0] XOFF = 8'h13    // DC3
) (
    input  logic       clk,
    input  logic       rst_n,
    input  logic       rx_char_valid_i,
    input  logic [7:0] rx_char_data_i,
    input  logic       sw_flow_en_i,      // only interpret when ENABLED
    output logic       tx_paused_o,
    output logic       consume_char_o     // this byte was control, not payload
);
    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            tx_paused_o    <= 1'b0;
            consume_char_o <= 1'b0;
        end else begin
            consume_char_o <= 1'b0;
            if (sw_flow_en_i && rx_char_valid_i) begin
                if (rx_char_data_i == XOFF) begin
                    tx_paused_o    <= 1'b1;
                    consume_char_o <= 1'b1;
                end else if (rx_char_data_i == XON) begin
                    tx_paused_o    <= 1'b0;
                    consume_char_o <= 1'b1;
                end
            end
        end
    end
endmodule

// Conceptual SystemVerilog — the two mechanisms combine as an AND of
// permissions. Either can withhold; neither overrides the other.
assign launch_allowed = !cts_sync_q          // hardware, Chapter 10.5
                     && !tx_paused_q         // software, this chapter
                     && !tx_fifo_empty;

HARDWARE:  decide -> drive pin -> far end recognises -> in-flight bytes arrive
SOFTWARE:  decide -> QUEUE the control byte -> TRANSMIT it (a full frame time)
                  -> far end receives and recognises -> in-flight bytes arrive
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                     this stage does not exist for a pin

P(a given byte is a control value)  =  2/256  =  0.781 %

//===========================================================================
//  uart_xon_xoff_v — Synthesizable Verilog-2001
//
//  The receive-side detector. It watches COMPLETED characters, which is why
//  it sits after the receiver rather than on the wire: XOFF is a byte in the
//  data stream, and the only way to recognise it is to have decoded it.
//
//  consume_char_o says "this byte was control, not payload" -- the flag that
//  keeps a control character out of the application's data.
//===========================================================================
module uart_xon_xoff_v #(
    parameter [7:0] XON  = 8'h11,    // DC1
    parameter [7:0] XOFF = 8'h13     // DC3
) (
    input  wire       clk,
    input  wire       rst_n,
    input  wire       rx_char_valid_i,
    input  wire [7:0] rx_char_data_i,
    input  wire       sw_flow_en_i,   // only interpret when ENABLED
    output reg        tx_paused_o,
    output reg        consume_char_o
);
    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            tx_paused_o    <= 1'b0;
            consume_char_o <= 1'b0;
        end else begin
            consume_char_o <= 1'b0;                 // default: one-cycle pulse
            if (sw_flow_en_i && rx_char_valid_i) begin
                if (rx_char_data_i == XOFF) begin
                    tx_paused_o    <= 1'b1;
                    consume_char_o <= 1'b1;
                end else if (rx_char_data_i == XON) begin
                    tx_paused_o    <= 1'b0;
                    consume_char_o <= 1'b1;
                end
            end
        end
    end
endmodule

--==========================================================================
--  uart_xon_xoff -- Synthesizable VHDL-2008
--
--  The receive-side detector. It watches COMPLETED characters, which is why
--  it sits after the receiver rather than on the wire: XOFF is a byte in the
--  data stream and can only be recognised once decoded.
--==========================================================================
library ieee;
use ieee.std_logic_1164.all;

entity uart_xon_xoff is
    generic (
        XON  : std_logic_vector(7 downto 0) := x"11";   -- DC1
        XOFF : std_logic_vector(7 downto 0) := x"13"    -- DC3
    );
    port (
        clk             : in  std_logic;
        rst_n           : in  std_logic;
        rx_char_valid_i : in  std_logic;
        rx_char_data_i  : in  std_logic_vector(7 downto 0);
        sw_flow_en_i    : in  std_logic;    -- only interpret when ENABLED
        tx_paused_o     : out std_logic;
        consume_char_o  : out std_logic     -- control byte, not payload
    );
end entity uart_xon_xoff;

architecture rtl of uart_xon_xoff is
begin
    process (clk, rst_n)
    begin
        if rst_n = '0' then
            tx_paused_o    <= '0';
            consume_char_o <= '0';
        elsif rising_edge(clk) then
            consume_char_o <= '0';                  -- default: one-cycle pulse
            if sw_flow_en_i = '1' and rx_char_valid_i = '1' then
                if rx_char_data_i = XOFF then
                    tx_paused_o    <= '1';
                    consume_char_o <= '1';
                elsif rx_char_data_i = XON then
                    tx_paused_o    <= '0';
                    consume_char_o <= '1';
                end if;
            end if;
        end if;
    end process;
end architecture rtl;

// enabled: 0x13 is a command
rx_char(XOFF);  check(paused === 1'b1, "XOFF pauses the local transmitter");

// disabled: the SAME byte is data and must pass through untouched
sw_en = 1'b0;
rx_char(XOFF);  check(n_consume == base, "disabled: XOFF/XON are payload");

//===========================================================================
//  tb_uart_xon_xoff_v — self-checking Verilog-2001 testbench
//
//  The block's whole difficulty is that a control character is INDISTIN-
//  GUISHABLE from payload that happens to have the same value. The tests
//  therefore cover both readings: with software flow control enabled the
//  byte is a command and is consumed; with it disabled the identical byte is
//  data and must pass through untouched.
//===========================================================================
`timescale 1ns/1ps

module tb_uart_xon_xoff_v;

    localparam [7:0] XON = 8'h11, XOFF = 8'h13;

    reg clk = 1'b0, rst_n = 1'b0;
    always #5 clk = ~clk;

    reg        rx_valid = 1'b0, sw_en = 1'b1;
    reg  [7:0] rx_data  = 8'h00;
    wire       paused, consume;

    uart_xon_xoff_v #(.XON(XON), .XOFF(XOFF)) dut (
        .clk(clk), .rst_n(rst_n),
        .rx_char_valid_i(rx_valid), .rx_char_data_i(rx_data),
        .sw_flow_en_i(sw_en),
        .tx_paused_o(paused), .consume_char_o(consume));

    integer checks = 0, failures = 0;

    task check;
        input cond;
        input [8*58-1:0] name;
        begin
            checks = checks + 1;
            if (cond) $display("  PASS %0s", name);
            else begin failures = failures + 1; $display("  FAIL %0s", name); end
        end
    endtask

    integer n_consume = 0, consume_wide = 0;
    reg     consume_prev = 1'b0;
    always @(posedge clk) if (rst_n) begin
        if (consume) begin
            n_consume = n_consume + 1;
            if (consume_prev) consume_wide = consume_wide + 1;
        end
        consume_prev = consume;
    end

    task rx_char;
        input [7:0] d;
        begin
            @(negedge clk) rx_data = d; rx_valid = 1'b1;
            @(negedge clk) rx_valid = 1'b0;
            @(negedge clk);
        end
    endtask

    task settle; begin repeat (2) @(negedge clk); end endtask

    integer base, i;

    initial begin
        #300_000;
        $display("  FAIL watchdog: simulation did not finish");
        $display("== %0d checks, %0d failures ==", checks+1, failures+1);
        $display("   RESULT: VERILOG XON/XOFF TESTS FAILED (timeout)");
        $finish;
    end

    initial begin
        $display("== uart_xon_xoff_v : self-checking Verilog testbench ==");

        rst_n = 1'b0; sw_en = 1'b1;
        repeat (4) @(negedge clk);
        check(paused === 1'b0 && consume === 1'b0, "reset: not paused, no consume");
        @(negedge clk) rst_n = 1'b1;
        @(negedge clk);

        // ---- ordinary payload passes through ------------------------------
        base = n_consume;
        rx_char(8'h41); rx_char(8'hA5); rx_char(8'h00); rx_char(8'hFF);
        settle;
        check(n_consume == base, "four ordinary bytes: none consumed");
        check(paused === 1'b0,   "four ordinary bytes: still not paused");

        // ---- XOFF pauses ---------------------------------------------------
        base = n_consume;
        rx_char(XOFF);
        settle;
        check(paused === 1'b1,       "XOFF pauses the local transmitter");
        check(n_consume == base + 1, "XOFF is consumed, exactly once");

        // ---- the pause persists across unrelated traffic -------------------
        rx_char(8'h42); rx_char(8'h43);
        check(paused === 1'b1, "pause survives intervening payload");

        // ---- a second XOFF is idempotent ------------------------------------
        base = n_consume;
        rx_char(XOFF);
        settle;
        check(paused === 1'b1,       "second XOFF: still paused");
        check(n_consume == base + 1, "second XOFF is still consumed");

        // ---- XON resumes ----------------------------------------------------
        base = n_consume;
        rx_char(XON);
        settle;
        check(paused === 1'b0,       "XON resumes the local transmitter");
        check(n_consume == base + 1, "XON is consumed too");

        // ---- XON when not paused --------------------------------------------
        base = n_consume;
        rx_char(XON);
        settle;
        check(paused === 1'b0,       "XON while running: stays running");
        check(n_consume == base + 1, "and is still consumed as a control byte");

        // ---- THE ambiguity: the same byte with the feature DISABLED ---------
        // 0x13 is a legitimate data value. With software flow control off it
        // is payload and must not be touched. This is the cost the chapter
        // names: the feature steals two values from the data space.
        @(negedge clk) sw_en = 1'b0;
        base = n_consume;
        rx_char(XOFF); rx_char(XON);
        settle;
        check(n_consume == base, "disabled: XOFF/XON are payload, not consumed");
        check(paused === 1'b0,   "disabled: transmitter never pauses");

        // ---- re-enabling mid-stream ------------------------------------------
        @(negedge clk) sw_en = 1'b1;
        base = n_consume;
        rx_char(XOFF);
        settle;
        check(paused === 1'b1,       "re-enabled: XOFF is a command again");
        check(n_consume == base + 1, "re-enabled: and is consumed");

        // ---- disabling WHILE paused -------------------------------------------
        // The pause is state, not a live decode. Disabling the feature does
        // not resume the transmitter -- only an XON or a reset does.
        @(negedge clk) sw_en = 1'b0;
        repeat (4) @(negedge clk);
        check(paused === 1'b1, "disabling while paused does NOT resume");
        @(negedge clk) sw_en = 1'b1;
        rx_char(XON);
        check(paused === 1'b0, "XON still resumes after re-enabling");

        // ---- a byte with no valid strobe is not seen --------------------------
        base = n_consume;
        @(negedge clk) rx_data = XOFF; rx_valid = 1'b0;
        repeat (4) @(negedge clk);
        check(n_consume == base, "data without rx_char_valid is ignored");
        check(paused === 1'b0,   "and does not pause");

        // ---- reset while paused ------------------------------------------------
        rx_char(XOFF);
        check(paused === 1'b1, "paused before reset");
        @(negedge clk) rst_n = 1'b0;
        repeat (2) @(negedge clk);
        check(paused === 1'b0, "reset resumes the transmitter");
        @(negedge clk) rst_n = 1'b1;
        @(negedge clk);

        check(consume_wide == 0, "consume pulse never wider than one clock");

        $display("== %0d checks, %0d failures ==", checks, failures);
        if (failures == 0) $display("   RESULT: ALL VERILOG XON/XOFF TESTS PASSED");
        else               $display("   RESULT: VERILOG XON/XOFF TESTS FAILED");
        $finish;
    end
endmodule

//===========================================================================
//  tb_uart_xon_xoff_sv — self-checking Verilog-2001 testbench
//
//  The block's whole difficulty is that a control character is INDISTIN-
//  GUISHABLE from payload that happens to have the same value. The tests
//  therefore cover both readings: with software flow control enabled the
//  byte is a command and is consumed; with it disabled the identical byte is
//  data and must pass through untouched.
//===========================================================================
`timescale 1ns/1ps

module tb_uart_xon_xoff_sv;

    localparam [7:0] XON = 8'h11, XOFF = 8'h13;

    logic clk = 1'b0, rst_n = 1'b0;
    always #5ns clk = ~clk;

    logic rx_valid = 1'b0, sw_en = 1'b1;
    logic [7:0] rx_data  = 8'h00;
    logic paused, consume;

    uart_xon_xoff #(.XON(XON), .XOFF(XOFF)) dut (
        .clk(clk), .rst_n(rst_n),
        .rx_char_valid_i(rx_valid), .rx_char_data_i(rx_data),
        .sw_flow_en_i(sw_en),
        .tx_paused_o(paused), .consume_char_o(consume));

    int unsigned checks = 0, failures = 0;

    task automatic check(input bit cond, input string name);
        checks++;
        if (cond) $display("  PASS %0s", name);
        else begin failures++; $display("  FAIL %0s", name); end
    endtask

    int n_consume = 0, consume_wide = 0;
    logic consume_prev = 1'b0;
    always @(posedge clk) if (rst_n) begin
        if (consume) begin
            n_consume = n_consume + 1;
            if (consume_prev) consume_wide = consume_wide + 1;
        end
        consume_prev = consume;
    end

    task automatic rx_char(input logic [7:0] d);
        @(negedge clk) rx_data = d; rx_valid = 1'b1;
        @(negedge clk) rx_valid = 1'b0;
        @(negedge clk);
    endtask

    task automatic settle(); repeat (2) @(negedge clk); endtask

    int base, i;

    initial begin
        #300us;
        $display("  FAIL watchdog: simulation did not finish");
        $display("== %0d checks, %0d failures ==", checks+1, failures+1);
        $display("   RESULT: SYSTEMVERILOG XON/XOFF TESTS FAILED (timeout)");
        $finish;
    end

    initial begin
        $display("== uart_xon_xoff : self-checking Verilog testbench ==");

        rst_n = 1'b0; sw_en = 1'b1;
        repeat (4) @(negedge clk);
        check(paused === 1'b0 && consume === 1'b0, "reset: not paused, no consume");
        @(negedge clk) rst_n = 1'b1;
        @(negedge clk);

        // ---- ordinary payload passes through ------------------------------
        base = n_consume;
        rx_char(8'h41); rx_char(8'hA5); rx_char(8'h00); rx_char(8'hFF);
        settle();
        check(n_consume == base, "four ordinary bytes: none consumed");
        check(paused === 1'b0,   "four ordinary bytes: still not paused");

        // ---- XOFF pauses ---------------------------------------------------
        base = n_consume;
        rx_char(XOFF);
        settle();
        check(paused === 1'b1,       "XOFF pauses the local transmitter");
        check(n_consume == base + 1, "XOFF is consumed, exactly once");

        // ---- the pause persists across unrelated traffic -------------------
        rx_char(8'h42); rx_char(8'h43);
        check(paused === 1'b1, "pause survives intervening payload");

        // ---- a second XOFF is idempotent ------------------------------------
        base = n_consume;
        rx_char(XOFF);
        settle();
        check(paused === 1'b1,       "second XOFF: still paused");
        check(n_consume == base + 1, "second XOFF is still consumed");

        // ---- XON resumes ----------------------------------------------------
        base = n_consume;
        rx_char(XON);
        settle();
        check(paused === 1'b0,       "XON resumes the local transmitter");
        check(n_consume == base + 1, "XON is consumed too");

        // ---- XON when not paused --------------------------------------------
        base = n_consume;
        rx_char(XON);
        settle();
        check(paused === 1'b0,       "XON while running: stays running");
        check(n_consume == base + 1, "and is still consumed as a control byte");

        // ---- THE ambiguity: the same byte with the feature DISABLED ---------
        // 0x13 is a legitimate data value. With software flow control off it
        // is payload and must not be touched. This is the cost the chapter
        // names: the feature steals two values from the data space.
        @(negedge clk) sw_en = 1'b0;
        base = n_consume;
        rx_char(XOFF); rx_char(XON);
        settle();
        check(n_consume == base, "disabled: XOFF/XON are payload, not consumed");
        check(paused === 1'b0,   "disabled: transmitter never pauses");

        // ---- re-enabling mid-stream ------------------------------------------
        @(negedge clk) sw_en = 1'b1;
        base = n_consume;
        rx_char(XOFF);
        settle();
        check(paused === 1'b1,       "re-enabled: XOFF is a command again");
        check(n_consume == base + 1, "re-enabled: and is consumed");

        // ---- disabling WHILE paused -------------------------------------------
        // The pause is state, not a live decode. Disabling the feature does
        // not resume the transmitter -- only an XON or a reset does.
        @(negedge clk) sw_en = 1'b0;
        repeat (4) @(negedge clk);
        check(paused === 1'b1, "disabling while paused does NOT resume");
        @(negedge clk) sw_en = 1'b1;
        rx_char(XON);
        check(paused === 1'b0, "XON still resumes after re-enabling");

        // ---- a byte with no valid strobe is not seen --------------------------
        base = n_consume;
        @(negedge clk) rx_data = XOFF; rx_valid = 1'b0;
        repeat (4) @(negedge clk);
        check(n_consume == base, "data without rx_char_valid is ignored");
        check(paused === 1'b0,   "and does not pause");

        // ---- reset while paused ------------------------------------------------
        rx_char(XOFF);
        check(paused === 1'b1, "paused before reset");
        @(negedge clk) rst_n = 1'b0;
        repeat (2) @(negedge clk);
        check(paused === 1'b0, "reset resumes the transmitter");
        @(negedge clk) rst_n = 1'b1;
        @(negedge clk);

        check(consume_wide == 0, "consume pulse never wider than one clock");

        $display("== %0d checks, %0d failures ==", checks, failures);
        if (failures == 0) $display("   RESULT: ALL SYSTEMVERILOG XON/XOFF TESTS PASSED");
        else               $display("   RESULT: SYSTEMVERILOG XON/XOFF TESTS FAILED");
        $finish;
    end
endmodule

--==========================================================================
--  tb_uart_xon_xoff -- self-checking VHDL-2008 testbench
--  Same 23 checks. Both readings of the ambiguous byte are covered: enabled
--  it is a command, disabled it is payload.
--==========================================================================
library ieee;
use ieee.std_logic_1164.all;
use std.env.finish;

entity tb_uart_xon_xoff is
end entity tb_uart_xon_xoff;

architecture sim of tb_uart_xon_xoff is
    constant XONC  : std_logic_vector(7 downto 0) := x"11";
    constant XOFFC : std_logic_vector(7 downto 0) := x"13";
    constant CLK_PERIOD : time := 10 ns;

    signal clk, rst_n, done : std_logic := '0';
    signal rx_valid : std_logic := '0';
    signal sw_en    : std_logic := '1';
    signal rx_data  : std_logic_vector(7 downto 0) := (others => '0');
    signal paused, consume : std_logic;
    signal n_consume, consume_wide : natural := 0;
begin
    clk <= not clk after CLK_PERIOD/2 when done = '0' else '0';

    dut : entity work.uart_xon_xoff
        generic map (XON => XONC, XOFF => XOFFC)
        port map (clk => clk, rst_n => rst_n,
                  rx_char_valid_i => rx_valid, rx_char_data_i => rx_data,
                  sw_flow_en_i => sw_en,
                  tx_paused_o => paused, consume_char_o => consume);

    obs : process (clk)
        variable n, w : natural := 0;
        variable prev : std_logic := '0';
    begin
        if rising_edge(clk) and rst_n = '1' then
            if consume = '1' then
                n := n + 1;
                if prev = '1' then w := w + 1; end if;
            end if;
            prev := consume;
            n_consume <= n; consume_wide <= w;
        end if;
    end process obs;

    watchdog : process
    begin
        wait for 300 us;
        report "   RESULT: VHDL XON/XOFF TESTS FAILED (timeout)" severity failure;
        wait;
    end process watchdog;

    stim : process
        variable checks, failures, base : natural := 0;
        procedure check(cond : boolean; name : string) is
        begin
            checks := checks + 1;
            if cond then report "  PASS " & name;
            else failures := failures + 1; report "  FAIL " & name severity error; end if;
        end procedure;
        procedure rx_char(d : std_logic_vector) is
        begin
            wait until falling_edge(clk); rx_data <= d; rx_valid <= '1';
            wait until falling_edge(clk); rx_valid <= '0';
            wait until falling_edge(clk);
        end procedure;
        procedure settle is
        begin
            for i in 0 to 1 loop wait until falling_edge(clk); end loop;
        end procedure;
    begin
        report "== uart_xon_xoff (VHDL) : self-checking testbench ==";
        rst_n <= '0'; sw_en <= '1';
        for i in 0 to 3 loop wait until falling_edge(clk); end loop;
        check(paused = '0' and consume = '0', "reset: not paused, no consume");
        rst_n <= '1'; wait until falling_edge(clk);

        base := n_consume;
        rx_char(x"41"); rx_char(x"A5"); rx_char(x"00"); rx_char(x"FF");
        settle;
        check(n_consume = base, "four ordinary bytes: none consumed");
        check(paused = '0',     "four ordinary bytes: still not paused");

        base := n_consume; rx_char(XOFFC); settle;
        check(paused = '1',       "XOFF pauses the local transmitter");
        check(n_consume = base+1, "XOFF is consumed, exactly once");

        rx_char(x"42"); rx_char(x"43");
        check(paused = '1', "pause survives intervening payload");

        base := n_consume; rx_char(XOFFC); settle;
        check(paused = '1',       "second XOFF: still paused");
        check(n_consume = base+1, "second XOFF is still consumed");

        base := n_consume; rx_char(XONC); settle;
        check(paused = '0',       "XON resumes the local transmitter");
        check(n_consume = base+1, "XON is consumed too");

        base := n_consume; rx_char(XONC); settle;
        check(paused = '0',       "XON while running: stays running");
        check(n_consume = base+1, "and is still consumed as a control byte");

        wait until falling_edge(clk); sw_en <= '0';
        base := n_consume; rx_char(XOFFC); rx_char(XONC); settle;
        check(n_consume = base, "disabled: XOFF/XON are payload, not consumed");
        check(paused = '0',     "disabled: transmitter never pauses");

        wait until falling_edge(clk); sw_en <= '1';
        base := n_consume; rx_char(XOFFC); settle;
        check(paused = '1',       "re-enabled: XOFF is a command again");
        check(n_consume = base+1, "re-enabled: and is consumed");

        wait until falling_edge(clk); sw_en <= '0';
        for i in 0 to 3 loop wait until falling_edge(clk); end loop;
        check(paused = '1', "disabling while paused does NOT resume");
        wait until falling_edge(clk); sw_en <= '1';
        rx_char(XONC);
        check(paused = '0', "XON still resumes after re-enabling");

        base := n_consume;
        wait until falling_edge(clk); rx_data <= XOFFC; rx_valid <= '0';
        for i in 0 to 3 loop wait until falling_edge(clk); end loop;
        check(n_consume = base, "data without rx_char_valid is ignored");
        check(paused = '0',     "and does not pause");

        rx_char(XOFFC);
        check(paused = '1', "paused before reset");
        wait until falling_edge(clk); rst_n <= '0';
        for i in 0 to 1 loop wait until falling_edge(clk); end loop;
        check(paused = '0', "reset resumes the transmitter");
        wait until falling_edge(clk); rst_n <= '1';
        wait until falling_edge(clk);

        check(consume_wide = 0, "consume pulse never wider than one clock");

        report "== " & integer'image(checks) & " checks, " &
               integer'image(failures) & " failures ==";
        if failures = 0 then report "   RESULT: ALL VHDL XON/XOFF TESTS PASSED";
        else report "   RESULT: VHDL XON/XOFF TESTS FAILED" severity error; end if;
        done <= '1'; finish;
    end process stim;
end architecture sim;

== uart_xon_xoff_v : self-checking Verilog testbench ==
  PASS four ordinary bytes: none consumed
  PASS XOFF pauses the local transmitter
  PASS XOFF is consumed, exactly once
  PASS pause survives intervening payload
  PASS second XOFF: still paused
  PASS XON resumes the local transmitter
  PASS XON while running: stays running
  PASS disabled: XOFF/XON are payload, not consumed
  PASS re-enabled: XOFF is a command again
  PASS disabling while paused does NOT resume
  PASS data without rx_char_valid is ignored
  PASS reset resumes the transmitter
  PASS consume pulse never wider than one clock
== 23 checks, 0 failures ==
   RESULT: ALL VERILOG XON/XOFF TESTS PASSED

// Assertion — a pause change requires an enabled control character.
// Nothing else may alter the pause state.
property p_pause_needs_control;
    @(posedge clk) disable iff (!rst_n)
        $changed(tx_paused_o) |-> $past(sw_flow_en_i && rx_char_valid_i);
endproperty
assert property (p_pause_needs_control);

// Assertion — with software flow control disabled, control VALUES are
// ordinary payload. This is the transparency contract.
property p_disabled_is_transparent;
    @(posedge clk) disable iff (!rst_n)
        !sw_flow_en_i |=> (!consume_char_o && $stable(tx_paused_o));
endproperty
assert property (p_disabled_is_transparent);

// Assertion — a consumed character is always one of the two control values.
property p_consume_only_control;
    @(posedge clk) disable iff (!rst_n)
        consume_char_o |-> ($past(rx_char_data_i) inside {XON, XOFF});
endproperty
assert property (p_consume_only_control);

// Published as SystemVerilog Assertions. Icarus Verilog 13.0 supports
// neither named properties nor $past, so what was EXECUTED is the
// procedural equivalent inside each testbench.

// p_level_bounded -- catches a width or update error in the occupancy
// counter. A level that can exceed DEPTH makes `full` meaningless and a
// level that cannot reach DEPTH makes it unreachable.
property p_level_bounded;
    @(posedge clk) disable iff (!rst_n) level_o <= CNT_W'(DEPTH);
endproperty

// p_empty_full_exclusive -- catches the two flags being derived from
// different quantities. They are both functions of one counter and can
// never both be true unless DEPTH is zero.
property p_empty_full_exclusive;
    @(posedge clk) disable iff (!rst_n) !(empty_o && full_o);
endproperty

// p_no_overflow_on_handoff -- catches the `push && !full` formulation.
// A push that coincides with a pop must be accepted, and reporting an
// overflow there is a lost byte at exactly the moment the consumer was
// keeping up.
property p_no_overflow_on_handoff;
    @(posedge clk) disable iff (!rst_n)
        (push_i && pop_i && full_o) |=> !overflow_evt_o;
endproperty

// p_hysteresis_holds -- catches a single-threshold flow controller. Between
// the two levels the decision must not change, whatever occupancy does.
property p_hysteresis_holds;
    @(posedge clk) disable iff (!rst_n)
        (level_i > RESUME_LEVEL && level_i < STOP_LEVEL) |=> $stable(allow_remote_o);
endproperty

// p_cts_two_flops -- catches a synchroniser shortened to one stage. The
// output must not respond to cts_n_i in fewer than two clocks.
property p_cts_two_flops;
    @(posedge clk) disable iff (!rst_n)
        $changed(cts_n_i) |=> $stable(launch_allowed_o);
endproperty

// p_consume_is_a_pulse -- catches a control-byte strobe held as a level,
// which makes a downstream consumer discard more than one byte.
property p_consume_is_a_pulse;
    @(posedge clk) disable iff (!rst_n) consume_char_o |=> !consume_char_o;
endproperty