The End-of-Transfer NACK

   Per byte, nine bit slots:

     slots 1..8   SDA driven by the SLAVE   (the data)        master: read-only
     slot  9      SDA driven by the MASTER  (the acknowledge) master: 1 bit

   So a master-receiver's entire outbound bandwidth during a read is:

       1 bit per byte  =  1 bit per 9 bit slots  =  11.1% of the bus

   and it must carry the only message the master needs to send:

       ACK   = "another byte, please"
       NACK  = "that was the last one"

   One bit, two meanings, and the second one is a TERMINATION. The specification
   lists it as the fifth reason a NACK occurs:

       "A master-receiver must signal the end of the transfer to the slave
        transmitter."

   Note the word MUST. This is not a convention or an optimisation -- it is the
   defined mechanism, and there is no alternative.

   // A master-receiver's acknowledge policy. The specification makes it condition 5
   // of the five NACK conditions: "A master-receiver must signal the end of the
   // transfer to the slave transmitter." So the master acknowledges every byte it
   // wants another after, and NACKs the last one -- the NACK is how it says "stop".
   module i2c_master_rx_ack_sequencer #(
       parameter int CNT_W = 8
   )(
       input  logic clk,
       input  logic rst_n,
       input  logic start_read,              // pulse: begin a read of n_bytes
       input  logic [CNT_W-1:0] n_bytes,     // how many bytes to read; zero is illegal
       input  logic byte_received,           // pulse: a data byte has arrived
       output logic send_ack,                // what to drive in the ninth slot
       output logic read_active,
       output logic request_stop,            // pulse: issue the STOP now
       output logic [CNT_W-1:0] remaining,
       output logic cfg_error                // a zero-length read was requested
   );
       // A zero-byte read is not a short read, it is a contradiction: the master would
       // have to answer a byte it never asked the slave to send. Refuse it rather than
       // silently reading one byte, which is what a design that clamps would do.
       assign cfg_error = (n_bytes == '0);

       // ACK every byte except the last. `remaining` still holds the count INCLUDING
       // the byte currently on the bus, so the last byte is the one where it reads 1 --
       // which is why this is a comparison against 1 and not against 0.
       assign send_ack = read_active && (remaining > {{(CNT_W-1){1'b0}}, 1'b1});

       always_ff @(posedge clk) begin
           if (!rst_n) begin
               read_active  <= 1'b0;
               remaining    <= '0;
               request_stop <= 1'b0;
           end else begin
               request_stop <= 1'b0;

               if (start_read && !cfg_error) begin
                   read_active <= 1'b1;
                   remaining   <= n_bytes;
               end else if (read_active && byte_received) begin
                   if (remaining <= {{(CNT_W-1){1'b0}}, 1'b1}) begin
                       // That was the last byte. It was NACKed, and a NACK must be
                       // followed by a STOP or a repeated START -- never by more clocks.
                       read_active  <= 1'b0;
                       remaining    <= '0;
                       request_stop <= 1'b1;
                   end else begin
                       remaining <= remaining - 1'b1;
                   end
               end
           end
       end
   endmodule

   module i2c_master_rx_ack_sequencer_tb;
       localparam int CNT_W = 8;

       logic clk = 1'b0, rst_n, start_read, byte_received;
       logic [CNT_W-1:0] n_bytes;
       logic send_ack, read_active, request_stop, cfg_error;
       logic [CNT_W-1:0] remaining;
       int errors = 0;

       i2c_master_rx_ack_sequencer #(.CNT_W(CNT_W)) dut (.*);

       always #5 clk = ~clk;
       initial begin #40000; $display("FAIL: watchdog expired"); $finish; end

       int n_stop = 0;
       always @(posedge clk) if (rst_n && request_stop) n_stop++;

       // Record the acknowledge decision for every byte of a read, so the whole
       // PATTERN can be checked rather than just the final byte.
       logic ack_log [0:15];
       int   n_logged;
       // Module scope: an initialised declaration inside a loop block is static in
       // SystemVerilog, and overriding the lifetime is not portable across tools.
       logic expect_ack;

       task automatic do_read(input int count);
           n_logged = 0;
           n_bytes = count[CNT_W-1:0];
           start_read = 1'b1; @(negedge clk); start_read = 1'b0; @(negedge clk);
           for (int b = 0; b < count; b++) begin
               // Sample the decision at the moment the acknowledge slot would use it,
               // BEFORE the byte is declared received.
               ack_log[n_logged] = send_ack; n_logged++;
               byte_received = 1'b1; @(negedge clk); byte_received = 1'b0; @(negedge clk);
           end
       endtask

       task automatic check_pattern(input int count, input int step);
           // Expected: ACK for every byte but the last, NACK for the last.
           for (int i = 0; i < count; i++) begin
               expect_ack = (i < count - 1);
               if (ack_log[i] !== expect_ack) begin
                   $display("FAIL: step %0d -- byte %0d of %0d: send_ack %0b, expected %0b",
                            step, i + 1, count, ack_log[i], expect_ack);
                   errors++;
               end
           end
           if (n_logged != count) begin
               $display("FAIL: step %0d -- logged %0d decisions for %0d bytes", step, n_logged, count);
               errors++;
           end
       endtask

       initial begin
           rst_n = 1'b0; start_read = 1'b0; byte_received = 1'b0; n_bytes = 8'd0;
           repeat (3) @(negedge clk);
           if (read_active !== 1'b0) begin $display("FAIL: read_active out of reset"); errors++; end
           rst_n = 1'b1; @(negedge clk);

           // 1 -- a ONE-byte read. The only byte is the last byte, so it is NACKed
           //      immediately. There is no ACK at all in a single-byte read.
           do_read(1);
           check_pattern(1, 1);
           if (n_stop != 1) begin $display("FAIL: expected one STOP request, saw %0d", n_stop); errors++; end
           if (read_active !== 1'b0) begin $display("FAIL: still active after a one-byte read"); errors++; end

           // 2 -- a THREE-byte read: ACK, ACK, NACK.
           n_stop = 0;
           do_read(3);
           check_pattern(3, 2);
           if (n_stop != 1) begin $display("FAIL: expected one STOP after three bytes"); errors++; end

           // 3 -- a FIVE-byte read, to show the pattern is not hard-coded to a length.
           n_stop = 0;
           do_read(5);
           check_pattern(5, 3);
           if (n_stop != 1) begin $display("FAIL: expected one STOP after five bytes"); errors++; end

           // 4 -- a ZERO-byte read is a contradiction and must be refused outright.
           n_bytes = 8'd0;
           @(negedge clk);
           if (cfg_error !== 1'b1) begin $display("FAIL: a zero-byte read was not flagged"); errors++; end
           n_stop = 0;
           start_read = 1'b1; @(negedge clk); start_read = 1'b0; repeat (3) @(negedge clk);
           if (read_active !== 1'b0) begin
               $display("FAIL: began a zero-byte read"); errors++; end
           if (n_stop != 0) begin $display("FAIL: a refused read still requested a STOP"); errors++; end

           // 5 -- no acknowledge decision leaks out when no read is active. A master
           //      that acknowledged outside a read would answer somebody else's byte.
           if (send_ack !== 1'b0) begin
               $display("FAIL: send_ack asserted while idle"); errors++; end

           // 6 -- back-to-back reads must not inherit state from each other.
           n_stop = 0;
           do_read(2); check_pattern(2, 6);
           do_read(4); check_pattern(4, 6);
           if (n_stop != 2) begin
               $display("FAIL: expected two STOP requests over two reads, saw %0d", n_stop); errors++; end

           if (errors == 0)
               $display("PASS: ACK every byte but the last, NACK the last, STOP after it; zero-length refused");
           else $display("FAIL: %0d error(s)", errors);
           $finish;
       end
   endmodule

   // A master-receiver's acknowledge policy. The specification makes it condition 5
   // of the five NACK conditions: "A master-receiver must signal the end of the
   // transfer to the slave transmitter." So the master acknowledges every byte it
   // wants another after, and NACKs the last one -- the NACK is how it says "stop".
   module i2c_master_rx_ack_sequencer #(
       parameter integer CNT_W = 8
   )(
       input  wire clk,
       input  wire rst_n,
       input  wire start_read,              // pulse: begin a read of n_bytes
       input  wire [CNT_W-1:0] n_bytes,     // how many bytes to read; zero is illegal
       input  wire byte_received,           // pulse: a data byte has arrived
       output wire send_ack,                // what to drive in the ninth slot
       output reg  read_active,
       output reg  request_stop,            // pulse: issue the STOP now
       output reg  [CNT_W-1:0] remaining,
       output wire cfg_error                // a zero-length read was requested
   );
       // A zero-byte read is a contradiction, not a short read: the master would have
       // to answer a byte it never asked for. Refuse rather than silently clamp.
       assign cfg_error = (n_bytes == {CNT_W{1'b0}});

       // ACK every byte except the last. `remaining` still INCLUDES the byte currently
       // on the bus, so the last byte is the one where it reads 1.
       assign send_ack = read_active && (remaining > {{(CNT_W-1){1'b0}}, 1'b1});

       always @(posedge clk) begin
           if (!rst_n) begin
               read_active  <= 1'b0;
               remaining    <= {CNT_W{1'b0}};
               request_stop <= 1'b0;
           end else begin
               request_stop <= 1'b0;

               if (start_read && !cfg_error) begin
                   read_active <= 1'b1;
                   remaining   <= n_bytes;
               end else if (read_active && byte_received) begin
                   if (remaining <= {{(CNT_W-1){1'b0}}, 1'b1}) begin
                       // That was the last byte. It was NACKed, and a NACK must be
                       // followed by a STOP or a repeated START -- never by more clocks.
                       read_active  <= 1'b0;
                       remaining    <= {CNT_W{1'b0}};
                       request_stop <= 1'b1;
                   end else begin
                       remaining <= remaining - 1'b1;
                   end
               end
           end
       end
   endmodule

   module i2c_master_rx_ack_sequencer_tb;
       localparam integer CNT_W = 8;

       reg clk, rst_n, start_read, byte_received;
       reg [CNT_W-1:0] n_bytes;
       wire send_ack, read_active, request_stop, cfg_error;
       wire [CNT_W-1:0] remaining;
       integer errors, n_stop, n_logged, b, i;

       i2c_master_rx_ack_sequencer #(.CNT_W(CNT_W)) dut (.clk(clk), .rst_n(rst_n),
           .start_read(start_read), .n_bytes(n_bytes), .byte_received(byte_received),
           .send_ack(send_ack), .read_active(read_active), .request_stop(request_stop),
           .remaining(remaining), .cfg_error(cfg_error));

       initial clk = 1'b0;
       always #5 clk = ~clk;
       initial begin #40000; $display("FAIL: watchdog expired"); $finish; end

       always @(posedge clk) if (rst_n && request_stop) n_stop = n_stop + 1;

       // Record the acknowledge decision for every byte of a read, so the whole
       // PATTERN can be checked rather than just the final byte.
       reg ack_log [0:15];
       reg expect_ack;

       task do_read; input integer count; begin
           n_logged = 0;
           n_bytes = count[CNT_W-1:0];
           start_read = 1'b1; @(negedge clk); start_read = 1'b0; @(negedge clk);
           for (b = 0; b < count; b = b + 1) begin
               // Sample the decision at the moment the acknowledge slot would use it,
               // BEFORE the byte is declared received.
               ack_log[n_logged] = send_ack; n_logged = n_logged + 1;
               byte_received = 1'b1; @(negedge clk); byte_received = 1'b0; @(negedge clk);
           end
       end endtask

       task check_pattern; input integer count; input integer step; begin
           // Expected: ACK for every byte but the last, NACK for the last.
           for (i = 0; i < count; i = i + 1) begin
               expect_ack = (i < count - 1);
               if (ack_log[i] !== expect_ack) begin
                   $display("FAIL: step %0d -- byte %0d of %0d: send_ack %0b, expected %0b",
                            step, i + 1, count, ack_log[i], expect_ack);
                   errors = errors + 1;
               end
           end
           if (n_logged != count) begin
               $display("FAIL: step %0d -- logged %0d decisions for %0d bytes", step, n_logged, count);
               errors = errors + 1;
           end
       end endtask

       initial begin
           errors = 0; n_stop = 0; n_logged = 0;
           rst_n = 1'b0; start_read = 1'b0; byte_received = 1'b0; n_bytes = 8'd0;
           repeat (3) @(negedge clk);
           if (read_active !== 1'b0) begin $display("FAIL: read_active out of reset"); errors = errors + 1; end
           rst_n = 1'b1; @(negedge clk);

           // 1 -- a ONE-byte read. The only byte is the last byte, so it is NACKed
           //      immediately. There is no ACK at all in a single-byte read.
           do_read(1);
           check_pattern(1, 1);
           if (n_stop != 1) begin $display("FAIL: expected one STOP request, saw %0d", n_stop); errors = errors + 1; end
           if (read_active !== 1'b0) begin $display("FAIL: still active after a one-byte read"); errors = errors + 1; end

           // 2 -- a THREE-byte read: ACK, ACK, NACK.
           n_stop = 0;
           do_read(3);
           check_pattern(3, 2);
           if (n_stop != 1) begin $display("FAIL: expected one STOP after three bytes"); errors = errors + 1; end

           // 3 -- a FIVE-byte read, to show the pattern is not hard-coded to a length.
           n_stop = 0;
           do_read(5);
           check_pattern(5, 3);
           if (n_stop != 1) begin $display("FAIL: expected one STOP after five bytes"); errors = errors + 1; end

           // 4 -- a ZERO-byte read is a contradiction and must be refused outright.
           n_bytes = 8'd0;
           @(negedge clk);
           if (cfg_error !== 1'b1) begin $display("FAIL: a zero-byte read was not flagged"); errors = errors + 1; end
           n_stop = 0;
           start_read = 1'b1; @(negedge clk); start_read = 1'b0; repeat (3) @(negedge clk);
           if (read_active !== 1'b0) begin
               $display("FAIL: began a zero-byte read"); errors = errors + 1; end
           if (n_stop != 0) begin $display("FAIL: a refused read still requested a STOP"); errors = errors + 1; end

           // 5 -- no acknowledge decision leaks out when no read is active. A master
           //      that acknowledged outside a read would answer somebody else's byte.
           if (send_ack !== 1'b0) begin
               $display("FAIL: send_ack asserted while idle"); errors = errors + 1; end

           // 6 -- back-to-back reads must not inherit state from each other.
           n_stop = 0;
           do_read(2); check_pattern(2, 6);
           do_read(4); check_pattern(4, 6);
           if (n_stop != 2) begin
               $display("FAIL: expected two STOP requests over two reads, saw %0d", n_stop); errors = errors + 1; end

           if (errors == 0)
               $display("PASS: ACK every byte but the last, NACK the last, STOP after it; zero-length refused");
           else $display("FAIL: %0d error(s)", errors);
           $finish;
       end
   endmodule

   library ieee;
   use ieee.std_logic_1164.all;
   use ieee.numeric_std.all;

   -- A master-receiver's acknowledge policy. The specification makes it condition 5
   -- of the five NACK conditions: "A master-receiver must signal the end of the
   -- transfer to the slave transmitter." So the master acknowledges every byte it
   -- wants another after, and NACKs the last one -- the NACK is how it says "stop".
   entity i2c_master_rx_ack_sequencer is
       generic (
           CNT_W : positive := 8
       );
       port (
           clk           : in  std_logic;
           rst_n         : in  std_logic;
           start_read    : in  std_logic;                     -- pulse: begin a read
           n_bytes       : in  unsigned(CNT_W - 1 downto 0);  -- zero is illegal
           byte_received : in  std_logic;                     -- pulse: a byte arrived
           send_ack      : out std_logic;                     -- drive in the ninth slot
           read_active   : out std_logic;
           request_stop  : out std_logic;                     -- pulse: issue the STOP
           remaining     : out unsigned(CNT_W - 1 downto 0);
           cfg_error     : out std_logic                      -- zero-length read
       );
   end entity;

   architecture rtl of i2c_master_rx_ack_sequencer is
       constant ZERO : unsigned(CNT_W - 1 downto 0) := (others => '0');
       constant ONE  : unsigned(CNT_W - 1 downto 0) := to_unsigned(1, CNT_W);
       signal rem_i    : unsigned(CNT_W - 1 downto 0) := (others => '0');
       signal active_i : std_logic := '0';
   begin
       -- A zero-byte read is a contradiction, not a short read: the master would have
       -- to answer a byte it never asked for. Refuse rather than silently clamp.
       cfg_error <= '1' when n_bytes = ZERO else '0';

       remaining   <= rem_i;
       read_active <= active_i;

       -- ACK every byte except the last. rem_i still INCLUDES the byte currently on the
       -- bus, so the last byte is the one where it reads 1.
       send_ack <= '1' when (active_i = '1' and rem_i > ONE) else '0';

       process (clk)
       begin
           if rising_edge(clk) then
               if rst_n = '0' then
                   active_i     <= '0';
                   rem_i        <= (others => '0');
                   request_stop <= '0';
               else
                   request_stop <= '0';

                   if start_read = '1' and n_bytes /= ZERO then
                       active_i <= '1';
                       rem_i    <= n_bytes;
                   elsif active_i = '1' and byte_received = '1' then
                       if rem_i <= ONE then
                           -- That was the last byte. It was NACKed, and a NACK must be
                           -- followed by a STOP or a repeated START, never more clocks.
                           active_i     <= '0';
                           rem_i        <= (others => '0');
                           request_stop <= '1';
                       else
                           rem_i <= rem_i - 1;
                       end if;
                   end if;
               end if;
           end if;
       end process;
   end architecture;

   library ieee;
   use ieee.std_logic_1164.all;
   use ieee.numeric_std.all;

   entity i2c_master_rx_ack_sequencer_tb is
   end entity;

   architecture sim of i2c_master_rx_ack_sequencer_tb is
       constant CNT_W : positive := 8;

       signal clk           : std_logic := '0';
       signal rst_n         : std_logic := '0';
       signal start_read    : std_logic := '0';
       signal byte_received : std_logic := '0';
       signal n_bytes       : unsigned(CNT_W - 1 downto 0) := (others => '0');
       signal send_ack, read_active, request_stop, cfg_error : std_logic;
       signal remaining     : unsigned(CNT_W - 1 downto 0);

       signal n_stop    : natural := 0;
       signal test_done : std_logic := '0';
   begin
       dut : entity work.i2c_master_rx_ack_sequencer
           generic map (CNT_W => CNT_W)
           port map (clk => clk, rst_n => rst_n, start_read => start_read, n_bytes => n_bytes,
                     byte_received => byte_received, send_ack => send_ack,
                     read_active => read_active, request_stop => request_stop,
                     remaining => remaining, cfg_error => cfg_error);

       clk <= not clk after 5 ns;

       watchdog : process
       begin
           wait for 40 us;
           if test_done = '0' then
               report "watchdog expired -- the design never reached the expected state"
                   severity failure;
           end if;
           wait;
       end process;

       count : process (clk)
       begin
           if rising_edge(clk) then
               if rst_n = '1' and request_stop = '1' then n_stop <= n_stop + 1; end if;
           end if;
       end process;

       stim : process
           variable errs     : natural := 0;
           type log_t is array (0 to 15) of std_logic;
           variable ack_log  : log_t := (others => '0');
           variable n_logged : natural := 0;
           variable base     : natural := 0;

           procedure waitn (n : in positive) is
           begin
               for i in 1 to n loop wait until falling_edge(clk); end loop;
           end procedure;

           procedure do_read (count : in positive) is
           begin
               n_logged := 0;
               n_bytes <= to_unsigned(count, CNT_W);
               start_read <= '1'; waitn(1); start_read <= '0'; waitn(1);
               for b in 1 to count loop
                   -- Sample the decision at the moment the acknowledge slot would use
                   -- it, BEFORE the byte is declared received.
                   ack_log(n_logged) := send_ack; n_logged := n_logged + 1;
                   byte_received <= '1'; waitn(1); byte_received <= '0'; waitn(1);
               end loop;
           end procedure;

           procedure check_pattern (count : in positive; step : in natural) is
               variable expect_ack : std_logic;
           begin
               for i in 0 to count - 1 loop
                   if i < count - 1 then expect_ack := '1'; else expect_ack := '0'; end if;
                   if ack_log(i) /= expect_ack then
                       report "step " & integer'image(step) & ": byte " & integer'image(i + 1)
                            & " of " & integer'image(count) & " had the wrong acknowledge"
                           severity error;
                       errs := errs + 1;
                   end if;
               end loop;
               if n_logged /= count then
                   report "step " & integer'image(step) & ": wrong number of decisions logged"
                       severity error; errs := errs + 1;
               end if;
           end procedure;
       begin
           waitn(3);
           if read_active /= '0' then
               report "read_active out of reset" severity error; errs := errs + 1; end if;
           rst_n <= '1'; waitn(1);

           -- 1: a ONE-byte read -- the only byte is the last, so it is NACKed at once.
           base := n_stop;
           do_read(1); check_pattern(1, 1);
           if (n_stop - base) /= 1 then
               report "expected one STOP request" severity error; errs := errs + 1; end if;
           if read_active /= '0' then
               report "still active after a one-byte read" severity error; errs := errs + 1; end if;

           -- 2: a THREE-byte read: ACK, ACK, NACK.
           base := n_stop;
           do_read(3); check_pattern(3, 2);
           if (n_stop - base) /= 1 then
               report "expected one STOP after three bytes" severity error; errs := errs + 1; end if;

           -- 3: FIVE bytes, to show the pattern is not hard-coded to a length.
           base := n_stop;
           do_read(5); check_pattern(5, 3);
           if (n_stop - base) /= 1 then
               report "expected one STOP after five bytes" severity error; errs := errs + 1; end if;

           -- 4: a ZERO-byte read is a contradiction and must be refused outright.
           n_bytes <= (others => '0'); waitn(1);
           if cfg_error /= '1' then
               report "a zero-byte read was not flagged" severity error; errs := errs + 1; end if;
           base := n_stop;
           start_read <= '1'; waitn(1); start_read <= '0'; waitn(3);
           if read_active /= '0' then
               report "began a zero-byte read" severity error; errs := errs + 1; end if;
           if (n_stop - base) /= 0 then
               report "a refused read still requested a STOP" severity error; errs := errs + 1; end if;

           -- 5: no acknowledge decision leaks out while idle.
           if send_ack /= '0' then
               report "send_ack asserted while idle" severity error; errs := errs + 1; end if;

           -- 6: back-to-back reads must not inherit state from each other.
           base := n_stop;
           do_read(2); check_pattern(2, 6);
           do_read(4); check_pattern(4, 6);
           if (n_stop - base) /= 2 then
               report "expected two STOP requests over two reads" severity error;
               errs := errs + 1; end if;

           if errs = 0 then
               report "i2c_master_rx_ack_sequencer self-check complete: ACK every byte but the "
                    & "last, NACK the last, STOP after it; zero-length refused" severity note;
           else
               report "i2c_master_rx_ack_sequencer self-check FAILED" severity error;
           end if;
           test_done <= '1';
           wait;
       end process;
   end architecture;

   `remaining` still INCLUDES the byte currently on the bus. So during byte k of an
   n-byte read:

       remaining = n - k + 1

   and the LAST byte is the one where remaining = 1, not 0. Hence:

       send_ack = (remaining > 1)

   Check the boundaries:

       n = 1:  byte 1 -> remaining = 1 -> send_ack = 0   NACK immediately.   correct
       n = 3:  byte 1 -> remaining = 3 -> send_ack = 1   ACK
               byte 2 -> remaining = 2 -> send_ack = 1   ACK
               byte 3 -> remaining = 1 -> send_ack = 0   NACK               correct

   The two adjacent formulations are both wrong, and wrong in opposite directions:

       send_ack = (remaining > 0)   ->  ACKs the last byte too.  Section 4's hang.
       send_ack = (remaining > 2)   ->  NACKs one byte early.    Short read.

   Both are single-character edits, both compile, and both are caught by section 7 --
   but only because the testbench checks the WHOLE PATTERN rather than the final
   byte. A test that verified "the last byte is NACKed" passes the second fault.

   // A NACK is only an error if it was not the fifth condition. Deciding that needs
   // two pieces of context the acknowledge bit does not carry: was the master
   // RECEIVING, and was this the byte it intended to be last?
   typedef enum { NACK_EXPECTED_END, NACK_UNEXPECTED } nack_class_e;

   function nack_class_e i2c_scoreboard::classify_nack(i2c_frame f, int byte_index);
       if (f.is_read && byte_index == f.expected_length - 1)
           return NACK_EXPECTED_END;      // condition 5 -- correct, and required
       return NACK_UNEXPECTED;            // conditions 1 to 4 -- report it
   endfunction

   // The property worth asserting is the POSITIVE obligation, not the absence of
   // NACKs: a read MUST end with one, and it must be on the last byte.
   property read_ends_with_a_nack;
       @(posedge clk) disable iff (!rst_n)
       (read_frame_complete) |-> (last_byte_was_nacked);
   endproperty
   assert property (read_ends_with_a_nack)
       else $error("a read completed without the master NACKing its final byte");

   // And the mirror: no byte BEFORE the last may be NACKed by the master, because
   // that is a short read rather than a termination.
   property no_early_master_nack;
       @(posedge clk) disable iff (!rst_n)
       (master_nacked && read_active) |-> (remaining == 1);
   endproperty