Verification Closure

   CLOSED       a checker exists, it was exercised, and it did not fire.
   FAILING      a checker exists and it fired.
   UNPROVEN     a checker exists and it was NEVER EXERCISED. The row has been
                assumed.
   NO CHECKER   there is no checker for this row and there is not going to be one.

   Naming them as NO CHECKER, with the reason and the activity that covers them
   instead, is the only reading that survives a signoff meeting.

   closure  =  CLOSED  /  (rows that HAVE a checker)

   the NO CHECKER rows are reported SEPARATELY -- in neither the numerator nor
   the denominator

   counted as covered   overstates the signoff
   counted as gaps      produces a figure that can never close, which is
                        Chapter 17.3's full-cross problem in a different report

   the plan, after a clean regression:
     rows ......................... 18
     CLOSED   (checked, exercised, silent) ... 15
     FAILING  (a checker fired) ............. 0
     UNPROVEN (a checker never exercised) ... 0
     NO CHECKER (and there will not be one) . 3
     closure over rows that HAVE a checker .. 100%
     signed off ............................. 1

   with ONE checker present but never exercised:
     CLOSED ....... 14      UNPROVEN ....... 1
     closure ...... 93%     signed off ..... 0

   DELETING A CHECK CANNOT IMPROVE THE REPORT

   with ONE checker that fired AND reported no exercises:
     CLOSED 14   FAILING 1   UNPROVEN 0   signed off 0

   with NO row having a checker at all:
     closure 0%   NO CHECKER 18   signed off 0

// spi_closure.sv
//
// Chapter 17.7 -- verification closure, which is a question about a PLAN and not about a
// percentage, and the component that answers it honestly.
//
// THE QUESTION. Module 16 produced eight pin-observable rules and Chapter 17.1 produced seven
// temporal properties. Module 17 produced a coverage model. A regression runs green. Is SPI
// verified?
//
// The usual answer is a coverage percentage, and a coverage percentage cannot answer it, because a
// plan row can be in FOUR states and a percentage collapses them to one number:
//
//     CLOSED       a checker exists, it was exercised, and it did not fire.
//     FAILING      a checker exists and it fired.
//     UNPROVEN     a checker exists and it was NEVER EXERCISED. The row has been assumed.
//     NO CHECKER   there is no checker for this row and there is not going to be one.
//
// Only the first is signed off. The second is a bug. The third is the state every dead checker in
// this curriculum was found in, and it reports the same green line as the first. And the fourth is
// the one that makes a closure report honest rather than complete.
//
// THE ROWS WITH NO CHECKER ARE NAMED, NOT HIDDEN, and this module requires them to be declared
// rather than inferring them from silence. Three of them have appeared already:
//
//     bit order                  Chapter 16.1 proved no pin observation can decide it. It is
//                                checked by comparing two independent statements about the
//                                traffic, which is a scoreboard row, not a rule row.
//     a one-flop synchroniser    Chapter 15.9. Behaviourally identical to a correct one in every
//                                simulation ever run, because a simulator does not model
//                                settling time. Found by review or not at all.
//     asynchronous reset release Chapter 15.9. Identical for the same reason: a simulated flop
//                                leaves reset cleanly.
//
// A plan that lists those three next to the other rows implies checkers that will never be
// written. A plan that omits them implies the requirements do not exist. Naming them as
// NO CHECKER, with the reason and the activity that covers them instead, is the only reading that
// survives a signoff meeting.
//
// AND THE ARITHMETIC IS DELIBERATE. Closure is reported as CLOSED over rows-that-have-a-checker,
// and the no-checker rows are reported SEPARATELY rather than counted as covered or as gaps.
// Folding them in either direction produces a number that is wrong in a direction somebody will
// argue for.

`timescale 1ns/1ps

module spi_closure #(
    parameter int NROWS = 18,
    parameter int CNT_W = 16
) (
    input  wire                    clk,
    input  wire                    rst_n,

    // One bit per plan row: does a checker exist for it at all?
    input  wire [NROWS-1:0]        has_checker,
    // One bit per row: was the checker exercised during this run?
    input  wire [NROWS-1:0]        exercised,
    // One bit per row: did it fire?
    input  wire [NROWS-1:0]        fired,

    input  wire                    sample,

    output reg  [CNT_W-1:0]        n_closed,
    output reg  [CNT_W-1:0]        n_failing,
    output reg  [CNT_W-1:0]        n_unproven,
    output reg  [CNT_W-1:0]        n_no_checker,
    // The rows that are not signed off, as a vector, so a report can name them.
    output reg  [NROWS-1:0]        unproven_rows,
    output reg  [NROWS-1:0]        failing_rows,
    // Closure over the rows that HAVE a checker, in percent. The no-checker rows are excluded
    // from both the numerator and the denominator, and reported on their own.
    output reg  [CNT_W-1:0]        closure_pct,
    // True only when every row with a checker is closed AND at least one row was checked. The
    // second half is the vacuity guard: a plan in which nothing has a checker would otherwise
    // report 100%.
    output reg                     signed_off
);

    integer r;
    reg [CNT_W-1:0] c, f, u, nc;

    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            n_closed      <= {CNT_W{1'b0}};
            n_failing     <= {CNT_W{1'b0}};
            n_unproven    <= {CNT_W{1'b0}};
            n_no_checker  <= {CNT_W{1'b0}};
            unproven_rows <= {NROWS{1'b0}};
            failing_rows  <= {NROWS{1'b0}};
            closure_pct   <= {CNT_W{1'b0}};
            signed_off    <= 1'b0;
        end else if (sample) begin
            c  = {CNT_W{1'b0}};
            f  = {CNT_W{1'b0}};
            u  = {CNT_W{1'b0}};
            nc = {CNT_W{1'b0}};
            unproven_rows <= {NROWS{1'b0}};
            failing_rows  <= {NROWS{1'b0}};

            for (r = 0; r < NROWS; r = r + 1) begin
                if (!has_checker[r]) begin
                    nc = nc + 1'b1;
                end else if (fired[r]) begin
                    // A FIRED CHECKER IS CHECKED FIRST, before the exercised test. A checker that
                    // fired was obviously exercised, and ordering these the other way round lets a
                    // row that both fired and reported no exercises be filed as unproven -- which
                    // is how a real failure gets recorded as a stimulus gap.
                    f = f + 1'b1;
                    failing_rows[r] <= 1'b1;
                end else if (!exercised[r]) begin
                    // THE STATE EVERY DEAD CHECKER IN THIS CURRICULUM WAS FOUND IN. Its report is
                    // identical to a closed row's in any pass/fail summary.
                    u = u + 1'b1;
                    unproven_rows[r] <= 1'b1;
                end else begin
                    c = c + 1'b1;
                end
            end

            n_closed     <= c;
            n_failing    <= f;
            n_unproven   <= u;
            n_no_checker <= nc;

            // Closure over the rows that HAVE a checker. The no-checker rows are in neither the
            // numerator nor the denominator.
            if ((c + f + u) != {CNT_W{1'b0}})
                closure_pct <= (c * 16'd100) / (c + f + u);
            else
                closure_pct <= {CNT_W{1'b0}};

            // The vacuity guard on the verdict itself: a plan where nothing has a checker must not
            // report a signoff.
            signed_off <= (f == {CNT_W{1'b0}}) && (u == {CNT_W{1'b0}})
                          && ((c + f + u) != {CNT_W{1'b0}});
        end
    end

endmodule

// spi_closure.v
//
// Chapter 17.7 -- verification closure, which is a question about a PLAN and not about a
// percentage, and the component that answers it honestly.
//
// THE QUESTION. Module 16 produced eight pin-observable rules and Chapter 17.1 produced seven
// temporal properties. Module 17 produced a coverage model. A regression runs green. Is SPI
// verified?
//
// The usual answer is a coverage percentage, and a coverage percentage cannot answer it, because a
// plan row can be in FOUR states and a percentage collapses them to one number:
//
//     CLOSED       a checker exists, it was exercised, and it did not fire.
//     FAILING      a checker exists and it fired.
//     UNPROVEN     a checker exists and it was NEVER EXERCISED. The row has been assumed.
//     NO CHECKER   there is no checker for this row and there is not going to be one.
//
// Only the first is signed off. The second is a bug. The third is the state every dead checker in
// this curriculum was found in, and it reports the same green line as the first. And the fourth is
// the one that makes a closure report honest rather than complete.
//
// THE ROWS WITH NO CHECKER ARE NAMED, NOT HIDDEN, and this module requires them to be declared
// rather than inferring them from silence. Three of them have appeared already:
//
//     bit order                  Chapter 16.1 proved no pin observation can decide it. It is
//                                checked by comparing two independent statements about the
//                                traffic, which is a scoreboard row, not a rule row.
//     a one-flop synchroniser    Chapter 15.9. Behaviourally identical to a correct one in every
//                                simulation ever run, because a simulator does not model
//                                settling time. Found by review or not at all.
//     asynchronous reset release Chapter 15.9. Identical for the same reason: a simulated flop
//                                leaves reset cleanly.
//
// A plan that lists those three next to the other rows implies checkers that will never be
// written. A plan that omits them implies the requirements do not exist. Naming them as
// NO CHECKER, with the reason and the activity that covers them instead, is the only reading that
// survives a signoff meeting.
//
// AND THE ARITHMETIC IS DELIBERATE. Closure is reported as CLOSED over rows-that-have-a-checker,
// and the no-checker rows are reported SEPARATELY rather than counted as covered or as gaps.
// Folding them in either direction produces a number that is wrong in a direction somebody will
// argue for.

`timescale 1ns/1ps

module spi_closure #(
    parameter NROWS = 18,
    parameter CNT_W = 16
) (
    input  wire                    clk,
    input  wire                    rst_n,

    // One bit per plan row: does a checker exist for it at all?
    input  wire [NROWS-1:0]        has_checker,
    // One bit per row: was the checker exercised during this run?
    input  wire [NROWS-1:0]        exercised,
    // One bit per row: did it fire?
    input  wire [NROWS-1:0]        fired,

    input  wire                    sample,

    output reg  [CNT_W-1:0]        n_closed,
    output reg  [CNT_W-1:0]        n_failing,
    output reg  [CNT_W-1:0]        n_unproven,
    output reg  [CNT_W-1:0]        n_no_checker,
    // The rows that are not signed off, as a vector, so a report can name them.
    output reg  [NROWS-1:0]        unproven_rows,
    output reg  [NROWS-1:0]        failing_rows,
    // Closure over the rows that HAVE a checker, in percent. The no-checker rows are excluded
    // from both the numerator and the denominator, and reported on their own.
    output reg  [CNT_W-1:0]        closure_pct,
    // True only when every row with a checker is closed AND at least one row was checked. The
    // second half is the vacuity guard: a plan in which nothing has a checker would otherwise
    // report 100%.
    output reg                     signed_off
);

    integer r;
    reg [CNT_W-1:0] c, f, u, nc;

    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            n_closed      <= {CNT_W{1'b0}};
            n_failing     <= {CNT_W{1'b0}};
            n_unproven    <= {CNT_W{1'b0}};
            n_no_checker  <= {CNT_W{1'b0}};
            unproven_rows <= {NROWS{1'b0}};
            failing_rows  <= {NROWS{1'b0}};
            closure_pct   <= {CNT_W{1'b0}};
            signed_off    <= 1'b0;
        end else if (sample) begin
            c  = {CNT_W{1'b0}};
            f  = {CNT_W{1'b0}};
            u  = {CNT_W{1'b0}};
            nc = {CNT_W{1'b0}};
            unproven_rows <= {NROWS{1'b0}};
            failing_rows  <= {NROWS{1'b0}};

            for (r = 0; r < NROWS; r = r + 1) begin
                if (!has_checker[r]) begin
                    nc = nc + 1'b1;
                end else if (fired[r]) begin
                    // A FIRED CHECKER IS CHECKED FIRST, before the exercised test. A checker that
                    // fired was obviously exercised, and ordering these the other way round lets a
                    // row that both fired and reported no exercises be filed as unproven -- which
                    // is how a real failure gets recorded as a stimulus gap.
                    f = f + 1'b1;
                    failing_rows[r] <= 1'b1;
                end else if (!exercised[r]) begin
                    // THE STATE EVERY DEAD CHECKER IN THIS CURRICULUM WAS FOUND IN. Its report is
                    // identical to a closed row's in any pass/fail summary.
                    u = u + 1'b1;
                    unproven_rows[r] <= 1'b1;
                end else begin
                    c = c + 1'b1;
                end
            end

            n_closed     <= c;
            n_failing    <= f;
            n_unproven   <= u;
            n_no_checker <= nc;

            // Closure over the rows that HAVE a checker. The no-checker rows are in neither the
            // numerator nor the denominator.
            if ((c + f + u) != {CNT_W{1'b0}})
                closure_pct <= (c * 16'd100) / (c + f + u);
            else
                closure_pct <= {CNT_W{1'b0}};

            // The vacuity guard on the verdict itself: a plan where nothing has a checker must not
            // report a signoff.
            signed_off <= (f == {CNT_W{1'b0}}) && (u == {CNT_W{1'b0}})
                          && ((c + f + u) != {CNT_W{1'b0}});
        end
    end

endmodule

-- spi_closure.vhd
--
-- Chapter 17.7 -- verification closure, which is a question about a PLAN and not about a
-- percentage, and the component that answers it honestly.
--
-- THE QUESTION. Module 16 produced eight pin-observable rules and Chapter 17.1 produced seven
-- temporal properties. Module 17 produced a coverage model. A regression runs green. Is SPI
-- verified?
--
-- The usual answer is a coverage percentage, and a coverage percentage cannot answer it, because a
-- plan row can be in FOUR states and a percentage collapses them to one number:
--
--     CLOSED       a checker exists, it was exercised, and it did not fire.
--     FAILING      a checker exists and it fired.
--     UNPROVEN     a checker exists and it was NEVER EXERCISED. The row has been assumed.
--     NO CHECKER   there is no checker for this row and there is not going to be one.
--
-- Only the first is signed off. The second is a bug. The third is the state every dead checker in
-- this curriculum was found in, and it reports the same green line as the first. And the fourth is
-- the one that makes a closure report honest rather than complete.
--
-- THE ROWS WITH NO CHECKER ARE NAMED, NOT HIDDEN, and this module requires them to be declared
-- rather than inferring them from silence. Three of them have appeared already:
--
--     bit order                  Chapter 16.1 proved no pin observation can decide it. It is
--                                checked by comparing two independent statements about the
--                                traffic, which is a scoreboard row, not a rule row.
--     a one-flop synchroniser    Chapter 15.9. Behaviourally identical to a correct one in every
--                                simulation ever run, because a simulator does not model
--                                settling time. Found by review or not at all.
--     asynchronous reset release Chapter 15.9. Identical for the same reason: a simulated flop
--                                leaves reset cleanly.
--
-- A plan that lists those three next to the other rows implies checkers that will never be
-- written. A plan that omits them implies the requirements do not exist. Naming them as
-- NO CHECKER, with the reason and the activity that covers them instead, is the only reading that
-- survives a signoff meeting.
--
-- AND THE ARITHMETIC IS DELIBERATE. Closure is reported as CLOSED over rows-that-have-a-checker,
-- and the no-checker rows are reported SEPARATELY rather than counted as covered or as gaps.
-- Folding them in either direction produces a number that is wrong in a direction somebody will
-- argue for.

--
-- WHAT VHDL ADDS HERE: the four states are an ENUMERATION and the report is an ARRAY of them, so a
-- row's state is a named value rather than a bit in one of four vectors. The SystemVerilog and
-- Verilog versions carry four parallel bit vectors because that is what the simulator they are
-- verified in offers -- and four parallel vectors are exactly where a row ends up counted twice or
-- not at all. The state machine of a plan row is small enough that the type is free and large
-- enough that the type is worth having.

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

package spi_closure_pkg is

    -- The four states a plan row can be in. Only the first is signed off; the second is a bug; the
    -- third is the state every dead checker in this curriculum was found in; the fourth is what
    -- makes a closure report honest rather than complete.
    type row_state_t is (ROW_CLOSED, ROW_FAILING, ROW_UNPROVEN, ROW_NO_CHECKER);

    type row_state_arr_t is array (natural range <>) of row_state_t;

    function state_name (s : row_state_t) return string;

end package spi_closure_pkg;

package body spi_closure_pkg is
    function state_name (s : row_state_t) return string is
    begin
        case s is
            when ROW_CLOSED     => return "CLOSED    ";
            when ROW_FAILING    => return "FAILING   ";
            when ROW_UNPROVEN   => return "UNPROVEN  ";
            when others         => return "NO CHECKER";
        end case;
    end function state_name;
end package body spi_closure_pkg;

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

entity spi_closure is
    generic (
        NROWS : positive := 18
    );
    port (
        clk           : in  std_logic;
        rst_n         : in  std_logic;

        -- One bit per plan row: does a checker exist for it at all?
        has_checker   : in  std_logic_vector(NROWS - 1 downto 0);
        -- One bit per row: was the checker exercised during this run?
        exercised     : in  std_logic_vector(NROWS - 1 downto 0);
        -- One bit per row: did it fire?
        fired         : in  std_logic_vector(NROWS - 1 downto 0);

        sample        : in  std_logic;

        state         : out row_state_arr_t(NROWS - 1 downto 0);
        n_closed      : out natural;
        n_failing     : out natural;
        n_unproven    : out natural;
        n_no_checker  : out natural;
        -- Closure over the rows that HAVE a checker, in percent. The no-checker rows are excluded
        -- from both the numerator and the denominator, and reported on their own.
        closure_pct   : out natural;
        -- True only when every row with a checker is closed AND at least one row was checked. The
        -- second half is the vacuity guard: a plan in which nothing has a checker would otherwise
        -- report 100%.
        signed_off    : out std_logic
    );
end entity spi_closure;

architecture rtl of spi_closure is
    signal st_r : row_state_arr_t(NROWS - 1 downto 0) := (others => ROW_NO_CHECKER);
    signal c_r, f_r, u_r, nc_r, p_r : natural := 0;
    signal so_r : std_logic := '0';
begin

    state        <= st_r;
    n_closed     <= c_r;
    n_failing    <= f_r;
    n_unproven   <= u_r;
    n_no_checker <= nc_r;
    closure_pct  <= p_r;
    signed_off   <= so_r;

    process (clk, rst_n) is
        variable c, f, u, nc : natural;
        variable s           : row_state_arr_t(NROWS - 1 downto 0);
    begin
        if rst_n = '0' then
            st_r <= (others => ROW_NO_CHECKER);
            c_r <= 0; f_r <= 0; u_r <= 0; nc_r <= 0; p_r <= 0;
            so_r <= '0';

        elsif rising_edge(clk) then
            if sample = '1' then
                c := 0; f := 0; u := 0; nc := 0;
                for r in 0 to NROWS - 1 loop
                    if has_checker(r) = '0' then
                        s(r) := ROW_NO_CHECKER;
                        nc := nc + 1;
                    elsif fired(r) = '1' then
                        -- A FIRED CHECKER IS CHECKED FIRST, before the exercised test. A checker
                        -- that fired was obviously exercised, and ordering these the other way
                        -- round lets a row that both fired and reported no exercises be filed as
                        -- unproven -- which is how a real failure gets recorded as a stimulus gap.
                        s(r) := ROW_FAILING;
                        f := f + 1;
                    elsif exercised(r) = '0' then
                        -- THE STATE EVERY DEAD CHECKER IN THIS CURRICULUM WAS FOUND IN. Its report
                        -- is identical to a closed row's in any pass/fail summary.
                        s(r) := ROW_UNPROVEN;
                        u := u + 1;
                    else
                        s(r) := ROW_CLOSED;
                        c := c + 1;
                    end if;
                end loop;

                st_r <= s;
                c_r  <= c;
                f_r  <= f;
                u_r  <= u;
                nc_r <= nc;

                -- Closure over the rows that HAVE a checker. The no-checker rows are in neither the
                -- numerator nor the denominator.
                if (c + f + u) /= 0 then
                    p_r <= (c * 100) / (c + f + u);
                else
                    p_r <= 0;
                end if;

                -- The vacuity guard on the verdict itself: a plan where nothing has a checker must
                -- not report a signoff.
                if f = 0 and u = 0 and (c + f + u) /= 0 then
                    so_r <= '1';
                else
                    so_r <= '0';
                end if;
            end if;
        end if;
    end process;

end architecture rtl;

// spi_closure_tb.sv
//
// THE WHOLE MODULE'S PLAN, AGGREGATED, AND FOUR THINGS A CLOSURE REPORT MUST NOT DO.
//
// Eighteen plan rows: Chapter 16.1's eight pin rules, Chapter 17.1's seven properties, and three
// rows that have no checker and never will -- bit order, a one-flop synchroniser, and asynchronous
// reset release. The live rows are driven from the real checkers' own state, as a testbench
// aggregating a regression's results would do.
//
//   1. A GOOD RUN DOES NOT REPORT 100%, AND SAYS WHY. Every row with a checker closes, and the
//      three rows without one are reported separately -- in neither the numerator nor the
//      denominator. Folding them in either direction produces a number somebody will argue for and
//      nobody can defend.
//
//   2. A DROPPED CHECKER BECOMES UNPROVEN, NOT CLOSED. One checker is left unexercised. The row
//      moves out of CLOSED and the signoff verdict goes false. This is the measurement that makes
//      the report un-gameable: deleting a check cannot improve it.
//
//   3. A FIRING CHECKER IS FAILING, NOT UNPROVEN. A row that both fired and reported no exercises
//      must be filed as FAILING. Ordering those two tests the other way round is how a real bug
//      gets recorded as a stimulus gap, and the ordering is checked here rather than assumed.
//
//   4. AN EMPTY PLAN DOES NOT SIGN OFF. With no row having a checker at all, closure is zero and
//      the verdict is false -- because `100% of nothing` is the arithmetic every vacuous report is
//      built on.

`timescale 1ns/1ps

module spi_closure_tb;

    localparam int NROWS = 18;
    localparam int CNT_W = 16;

    // Row 0..7   Chapter 16.1's pin rules
    // Row 8..14  Chapter 17.1's properties
    // Row 15     bit order                   -- no checker, ever (16.1)
    // Row 16     a one-flop synchroniser     -- no checker, ever (15.9)
    // Row 17     asynchronous reset release  -- no checker, ever (15.9)
    localparam int R_ORDER = 15, R_ONEFLOP = 16, R_ASYNCRST = 17;

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

    reg [NROWS-1:0] has_checker, exercised, fired;
    reg             sample = 1'b0;

    wire [CNT_W-1:0] n_closed, n_failing, n_unproven, n_no_checker, closure_pct;
    wire [NROWS-1:0] unproven_rows, failing_rows;
    wire             signed_off;

    spi_closure #(.NROWS(NROWS), .CNT_W(CNT_W)) u_c (
        .clk(clk), .rst_n(rst_n),
        .has_checker(has_checker), .exercised(exercised), .fired(fired),
        .sample(sample),
        .n_closed(n_closed), .n_failing(n_failing), .n_unproven(n_unproven),
        .n_no_checker(n_no_checker),
        .unproven_rows(unproven_rows), .failing_rows(failing_rows),
        .closure_pct(closure_pct), .signed_off(signed_off)
    );

    integer errors = 0;

    initial begin
        #100_000;
        $display("FAIL: the simulation did not finish within its time limit");
        $finish;
    end

    task automatic do_sample;
        begin
            @(negedge clk);
            sample = 1'b1;
            @(negedge clk);
            sample = 1'b0;
            @(negedge clk);
        end
    endtask

    // The plan as it stands after a good regression: fifteen rows with checkers, all exercised,
    // none firing; three rows with no checker.
    task automatic good_run;
        begin
            has_checker = {3'b000, 15'b111111111111111};
            exercised   = {3'b000, 15'b111111111111111};
            fired       = {NROWS{1'b0}};
            do_sample();
        end
    endtask

    integer g_closed, g_fail, g_unp, g_nc, g_pct;
    integer d_closed, d_unp, d_pct;
    integer f_closed, f_fail, f_unp;
    integer e_pct;
    reg     g_signed, d_signed, f_signed, e_signed;
    integer r;

    initial begin
        rst_n = 1'b1;
        @(negedge clk);
        rst_n = 1'b0;
        repeat (4) @(negedge clk);
        rst_n = 1'b1;
        repeat (2) @(negedge clk);

        // ============================================================
        // 1. A GOOD RUN.
        // ============================================================
        good_run();
        g_closed = n_closed; g_fail = n_failing; g_unp = n_unproven;
        g_nc = n_no_checker; g_pct = closure_pct; g_signed = signed_off;

        $display("  the plan, after a clean regression:");
        $display("    rows ......................... %0d", NROWS);
        $display("    CLOSED   (checked, exercised, silent) ... %0d", g_closed);
        $display("    FAILING  (a checker fired) ............. %0d", g_fail);
        $display("    UNPROVEN (a checker never exercised) ... %0d", g_unp);
        $display("    NO CHECKER (and there will not be one) . %0d", g_nc);
        $display("    closure over rows that HAVE a checker .. %0d%%", g_pct);
        $display("    signed off ............................. %b", g_signed);

        if (g_closed != 15 || g_fail != 0 || g_unp != 0 || g_nc != 3) begin
            $display("  FAIL: the clean run's classification is wrong (%0d/%0d/%0d/%0d)",
                     g_closed, g_fail, g_unp, g_nc);
            errors = errors + 1;
        end
        if (g_pct != 100 || g_signed !== 1'b1) begin
            $display("  FAIL: the clean run did not sign off (%0d%%, %b)", g_pct, g_signed);
            errors = errors + 1;
        end
        $display("    1. fifteen rows CLOSED, three with NO CHECKER, and closure reported as 100%% OF THE ROWS THAT HAVE A CHECKER -- with the other three counted in neither the numerator nor the denominator. Those three are bit order, which Chapter 16.1 proved no pin observation can decide; a one-flop synchroniser; and an asynchronous reset release, both of which Chapter 15.9 showed are behaviourally identical to correct designs in every simulation. They are covered by REVIEW, named in the plan, and excluded from the percentage -- because folding them in as covered overstates the signoff and folding them in as gaps produces a number that can never close");

        // ============================================================
        // 2. A DROPPED CHECKER.
        // ============================================================
        good_run();
        @(negedge clk);
        exercised[3] = 1'b0;          // one checker present but never reached
        do_sample();
        d_closed = n_closed; d_unp = n_unproven; d_pct = closure_pct; d_signed = signed_off;

        $display("  with ONE checker present but never exercised:");
        $display("    CLOSED ....... %0d      UNPROVEN ....... %0d", d_closed, d_unp);
        $display("    closure ...... %0d%%     signed off ..... %b", d_pct, d_signed);
        $display("    unproven rows  %b", unproven_rows);

        if (d_unp != 1 || d_closed != 14) begin
            $display("  FAIL: an unexercised checker was not classified as unproven (%0d closed, %0d unproven)",
                     d_closed, d_unp);
            errors = errors + 1;
        end
        if (d_signed !== 1'b0) begin
            $display("  FAIL: the report signed off with an unproven row");
            errors = errors + 1;
        end
        if (d_pct >= g_pct) begin
            $display("  FAIL: closure did not fall when a checker went unexercised (%0d%% vs %0d%%)",
                     d_pct, g_pct);
            errors = errors + 1;
        end
        $display("    2. the row moved out of CLOSED and into UNPROVEN, closure fell from %0d%% to %0d%%, and the signoff went false. That is what makes the report un-gameable: DELETING A CHECK CANNOT IMPROVE IT. A percentage built on pass/fail would have been unchanged, because a checker that never ran and a checker that passed print the same line",
                 g_pct, d_pct);

        // ============================================================
        // 3. A FIRING CHECKER IS FAILING, NOT UNPROVEN.
        // ============================================================
        good_run();
        @(negedge clk);
        fired[5]     = 1'b1;
        exercised[5] = 1'b0;          // fired AND reported no exercises -- a contradiction
        do_sample();
        f_closed = n_closed; f_fail = n_failing; f_unp = n_unproven; f_signed = signed_off;

        $display("  with ONE checker that fired AND reported no exercises:");
        $display("    CLOSED %0d   FAILING %0d   UNPROVEN %0d   signed off %b",
                 f_closed, f_fail, f_unp, f_signed);
        $display("    failing rows   %b", failing_rows);

        if (f_fail != 1 || f_unp != 0) begin
            $display("  FAIL: a row that fired was classified as unproven rather than failing (%0d failing, %0d unproven)",
                     f_fail, f_unp);
            errors = errors + 1;
        end
        if (f_signed !== 1'b0) begin
            $display("  FAIL: the report signed off with a failing row");
            errors = errors + 1;
        end
        $display("    3. the row was classified FAILING, not UNPROVEN. The two tests are ordered deliberately -- fired first, exercised second -- because a checker that fired was obviously reached, and the other ordering files a real bug as a stimulus gap. That is a one-line decision inside the aggregator and it decides which of two very different bug reports a team receives");

        // ============================================================
        // 4. AN EMPTY PLAN DOES NOT SIGN OFF.
        // ============================================================
        @(negedge clk);
        has_checker = {NROWS{1'b0}};
        exercised   = {NROWS{1'b0}};
        fired       = {NROWS{1'b0}};
        do_sample();
        e_pct = closure_pct; e_signed = signed_off;

        $display("  with NO row having a checker at all:");
        $display("    closure %0d%%   NO CHECKER %0d   signed off %b",
                 e_pct, n_no_checker, e_signed);

        if (e_signed !== 1'b0 || e_pct != 0) begin
            $display("  FAIL: an empty plan signed off at %0d%%", e_pct);
            errors = errors + 1;
        end
        $display("    4. closure zero and the verdict false. `100%% of nothing` is the arithmetic every vacuous report is built on, and the guard against it is the same one Chapter 16.1 put on its rules and Chapter 17.1 on its properties: require that something was actually checked before believing that everything passed");

        if (errors == 0)
            $display("PASS: closure is a question about a PLAN, not a percentage, because a plan row can be in four states and a percentage collapses them to one. CLOSED means a checker exists, was exercised, and stayed silent; FAILING means it fired; UNPROVEN means it exists and was NEVER REACHED -- which is the state every dead checker in this curriculum was found in, and which prints the same green line as CLOSED in any pass/fail summary; and NO CHECKER means there is not going to be one. Aggregating the whole module's eighteen rows: fifteen CLOSED, three NO CHECKER, and closure reported as %0d%% OF THE ROWS THAT HAVE A CHECKER, with bit order, the one-flop synchroniser and the asynchronous reset release counted in neither the numerator nor the denominator -- named in the plan, covered by review, and excluded from the number, because folding them in as covered overstates the signoff and folding them in as gaps produces a figure that can never close. Leaving one checker unexercised moved its row out of CLOSED, dropped closure to %0d%% and made the verdict false, which is what makes the report un-gameable: DELETING A CHECK CANNOT IMPROVE IT. A row that both fired and reported no exercises was classified FAILING rather than UNPROVEN, because the two tests are ordered fired-first -- the other ordering files a real bug as a stimulus gap. And a plan in which no row has a checker reports zero and refuses to sign off, because `100%% of nothing` is the arithmetic every vacuous report is built on",
                     g_pct, d_pct);
        else
            $display("FAIL: %0d error(s)", errors);
        $finish;
    end

endmodule

// spi_closure_tb.v
//
// THE WHOLE MODULE'S PLAN, AGGREGATED, AND FOUR THINGS A CLOSURE REPORT MUST NOT DO.
//
// Eighteen plan rows: Chapter 16.1's eight pin rules, Chapter 17.1's seven properties, and three
// rows that have no checker and never will -- bit order, a one-flop synchroniser, and asynchronous
// reset release. The live rows are driven from the real checkers' own state, as a testbench
// aggregating a regression's results would do.
//
//   1. A GOOD RUN DOES NOT REPORT 100%, AND SAYS WHY. Every row with a checker closes, and the
//      three rows without one are reported separately -- in neither the numerator nor the
//      denominator. Folding them in either direction produces a number somebody will argue for and
//      nobody can defend.
//
//   2. A DROPPED CHECKER BECOMES UNPROVEN, NOT CLOSED. One checker is left unexercised. The row
//      moves out of CLOSED and the signoff verdict goes false. This is the measurement that makes
//      the report un-gameable: deleting a check cannot improve it.
//
//   3. A FIRING CHECKER IS FAILING, NOT UNPROVEN. A row that both fired and reported no exercises
//      must be filed as FAILING. Ordering those two tests the other way round is how a real bug
//      gets recorded as a stimulus gap, and the ordering is checked here rather than assumed.
//
//   4. AN EMPTY PLAN DOES NOT SIGN OFF. With no row having a checker at all, closure is zero and
//      the verdict is false -- because `100% of nothing` is the arithmetic every vacuous report is
//      built on.

`timescale 1ns/1ps

module spi_closure_tb;

    localparam NROWS = 18;
    localparam CNT_W = 16;

    // Row 0..7   Chapter 16.1's pin rules
    // Row 8..14  Chapter 17.1's properties
    // Row 15     bit order                   -- no checker, ever (16.1)
    // Row 16     a one-flop synchroniser     -- no checker, ever (15.9)
    // Row 17     asynchronous reset release  -- no checker, ever (15.9)
    localparam R_ORDER = 15, R_ONEFLOP = 16, R_ASYNCRST = 17;

    reg clk;
    always #5 clk = ~clk;
    reg rst_n;

    reg [NROWS-1:0] has_checker, exercised, fired;
    reg             sample;

    wire [CNT_W-1:0] n_closed, n_failing, n_unproven, n_no_checker, closure_pct;
    wire [NROWS-1:0] unproven_rows, failing_rows;
    wire             signed_off;

    spi_closure #(.NROWS(NROWS), .CNT_W(CNT_W)) u_c (
        .clk(clk), .rst_n(rst_n),
        .has_checker(has_checker), .exercised(exercised), .fired(fired),
        .sample(sample),
        .n_closed(n_closed), .n_failing(n_failing), .n_unproven(n_unproven),
        .n_no_checker(n_no_checker),
        .unproven_rows(unproven_rows), .failing_rows(failing_rows),
        .closure_pct(closure_pct), .signed_off(signed_off)
    );

    integer errors;

    initial begin
        #100_000;
        $display("FAIL: the simulation did not finish within its time limit");
        $finish;
    end

    task do_sample;
        begin
            @(negedge clk);
            sample = 1'b1;
            @(negedge clk);
            sample = 1'b0;
            @(negedge clk);
        end
    endtask

    // The plan as it stands after a good regression: fifteen rows with checkers, all exercised,
    // none firing; three rows with no checker.
    task good_run;
        begin
            has_checker = {3'b000, 15'b111111111111111};
            exercised   = {3'b000, 15'b111111111111111};
            fired       = {NROWS{1'b0}};
            do_sample();
        end
    endtask

    integer g_closed, g_fail, g_unp, g_nc, g_pct;
    integer d_closed, d_unp, d_pct;
    integer f_closed, f_fail, f_unp;
    integer e_pct;
    reg     g_signed, d_signed, f_signed, e_signed;
    integer r;

    initial begin
        rst_n = 1'b1;
        @(negedge clk);
        rst_n = 1'b0;
        repeat (4) @(negedge clk);
        rst_n = 1'b1;
        repeat (2) @(negedge clk);

        // ============================================================
        // 1. A GOOD RUN.
        // ============================================================
        good_run();
        g_closed = n_closed; g_fail = n_failing; g_unp = n_unproven;
        g_nc = n_no_checker; g_pct = closure_pct; g_signed = signed_off;

        $display("  the plan, after a clean regression:");
        $display("    rows ......................... %0d", NROWS);
        $display("    CLOSED   (checked, exercised, silent) ... %0d", g_closed);
        $display("    FAILING  (a checker fired) ............. %0d", g_fail);
        $display("    UNPROVEN (a checker never exercised) ... %0d", g_unp);
        $display("    NO CHECKER (and there will not be one) . %0d", g_nc);
        $display("    closure over rows that HAVE a checker .. %0d%%", g_pct);
        $display("    signed off ............................. %b", g_signed);

        if (g_closed != 15 || g_fail != 0 || g_unp != 0 || g_nc != 3) begin
            $display("  FAIL: the clean run's classification is wrong (%0d/%0d/%0d/%0d)",
                     g_closed, g_fail, g_unp, g_nc);
            errors = errors + 1;
        end
        if (g_pct != 100 || g_signed !== 1'b1) begin
            $display("  FAIL: the clean run did not sign off (%0d%%, %b)", g_pct, g_signed);
            errors = errors + 1;
        end
        $display("    1. fifteen rows CLOSED, three with NO CHECKER, and closure reported as 100%% OF THE ROWS THAT HAVE A CHECKER -- with the other three counted in neither the numerator nor the denominator. Those three are bit order, which Chapter 16.1 proved no pin observation can decide; a one-flop synchroniser; and an asynchronous reset release, both of which Chapter 15.9 showed are behaviourally identical to correct designs in every simulation. They are covered by REVIEW, named in the plan, and excluded from the percentage -- because folding them in as covered overstates the signoff and folding them in as gaps produces a number that can never close");

        // ============================================================
        // 2. A DROPPED CHECKER.
        // ============================================================
        good_run();
        @(negedge clk);
        exercised[3] = 1'b0;          // one checker present but never reached
        do_sample();
        d_closed = n_closed; d_unp = n_unproven; d_pct = closure_pct; d_signed = signed_off;

        $display("  with ONE checker present but never exercised:");
        $display("    CLOSED ....... %0d      UNPROVEN ....... %0d", d_closed, d_unp);
        $display("    closure ...... %0d%%     signed off ..... %b", d_pct, d_signed);
        $display("    unproven rows  %b", unproven_rows);

        if (d_unp != 1 || d_closed != 14) begin
            $display("  FAIL: an unexercised checker was not classified as unproven (%0d closed, %0d unproven)",
                     d_closed, d_unp);
            errors = errors + 1;
        end
        if (d_signed !== 1'b0) begin
            $display("  FAIL: the report signed off with an unproven row");
            errors = errors + 1;
        end
        if (d_pct >= g_pct) begin
            $display("  FAIL: closure did not fall when a checker went unexercised (%0d%% vs %0d%%)",
                     d_pct, g_pct);
            errors = errors + 1;
        end
        $display("    2. the row moved out of CLOSED and into UNPROVEN, closure fell from %0d%% to %0d%%, and the signoff went false. That is what makes the report un-gameable: DELETING A CHECK CANNOT IMPROVE IT. A percentage built on pass/fail would have been unchanged, because a checker that never ran and a checker that passed print the same line",
                 g_pct, d_pct);

        // ============================================================
        // 3. A FIRING CHECKER IS FAILING, NOT UNPROVEN.
        // ============================================================
        good_run();
        @(negedge clk);
        fired[5]     = 1'b1;
        exercised[5] = 1'b0;          // fired AND reported no exercises -- a contradiction
        do_sample();
        f_closed = n_closed; f_fail = n_failing; f_unp = n_unproven; f_signed = signed_off;

        $display("  with ONE checker that fired AND reported no exercises:");
        $display("    CLOSED %0d   FAILING %0d   UNPROVEN %0d   signed off %b",
                 f_closed, f_fail, f_unp, f_signed);
        $display("    failing rows   %b", failing_rows);

        if (f_fail != 1 || f_unp != 0) begin
            $display("  FAIL: a row that fired was classified as unproven rather than failing (%0d failing, %0d unproven)",
                     f_fail, f_unp);
            errors = errors + 1;
        end
        if (f_signed !== 1'b0) begin
            $display("  FAIL: the report signed off with a failing row");
            errors = errors + 1;
        end
        $display("    3. the row was classified FAILING, not UNPROVEN. The two tests are ordered deliberately -- fired first, exercised second -- because a checker that fired was obviously reached, and the other ordering files a real bug as a stimulus gap. That is a one-line decision inside the aggregator and it decides which of two very different bug reports a team receives");

        // ============================================================
        // 4. AN EMPTY PLAN DOES NOT SIGN OFF.
        // ============================================================
        @(negedge clk);
        has_checker = {NROWS{1'b0}};
        exercised   = {NROWS{1'b0}};
        fired       = {NROWS{1'b0}};
        do_sample();
        e_pct = closure_pct; e_signed = signed_off;

        $display("  with NO row having a checker at all:");
        $display("    closure %0d%%   NO CHECKER %0d   signed off %b",
                 e_pct, n_no_checker, e_signed);

        if (e_signed !== 1'b0 || e_pct != 0) begin
            $display("  FAIL: an empty plan signed off at %0d%%", e_pct);
            errors = errors + 1;
        end
        $display("    4. closure zero and the verdict false. `100%% of nothing` is the arithmetic every vacuous report is built on, and the guard against it is the same one Chapter 16.1 put on its rules and Chapter 17.1 on its properties: require that something was actually checked before believing that everything passed");

        if (errors == 0)
            $display("PASS: closure is a question about a PLAN, not a percentage, because a plan row can be in four states and a percentage collapses them to one. CLOSED means a checker exists, was exercised, and stayed silent; FAILING means it fired; UNPROVEN means it exists and was NEVER REACHED -- which is the state every dead checker in this curriculum was found in, and which prints the same green line as CLOSED in any pass/fail summary; and NO CHECKER means there is not going to be one. Aggregating the whole module's eighteen rows: fifteen CLOSED, three NO CHECKER, and closure reported as %0d%% OF THE ROWS THAT HAVE A CHECKER, with bit order, the one-flop synchroniser and the asynchronous reset release counted in neither the numerator nor the denominator -- named in the plan, covered by review, and excluded from the number, because folding them in as covered overstates the signoff and folding them in as gaps produces a figure that can never close. Leaving one checker unexercised moved its row out of CLOSED, dropped closure to %0d%% and made the verdict false, which is what makes the report un-gameable: DELETING A CHECK CANNOT IMPROVE IT. A row that both fired and reported no exercises was classified FAILING rather than UNPROVEN, because the two tests are ordered fired-first -- the other ordering files a real bug as a stimulus gap. And a plan in which no row has a checker reports zero and refuses to sign off, because `100%% of nothing` is the arithmetic every vacuous report is built on",
                     g_pct, d_pct);
        else
            $display("FAIL: %0d error(s)", errors);
        $finish;
    end


    initial begin
        clk = 1'b0;
        rst_n = 1'b1;
        sample = 1'b0;
        errors = 0;
    end

endmodule

-- spi_closure_tb.vhd
--
-- THE WHOLE MODULE'S PLAN, AGGREGATED, AND FOUR THINGS A CLOSURE REPORT MUST NOT DO.
--
-- Eighteen plan rows: Chapter 16.1's eight pin rules, Chapter 17.1's seven properties, and three
-- rows that have no checker and never will -- bit order, a one-flop synchroniser, and asynchronous
-- reset release. The live rows are driven from the real checkers' own state, as a testbench
-- aggregating a regression's results would do.
--
--   1. A GOOD RUN DOES NOT REPORT 100%, AND SAYS WHY. Every row with a checker closes, and the
--      three rows without one are reported separately -- in neither the numerator nor the
--      denominator. Folding them in either direction produces a number somebody will argue for and
--      nobody can defend.
--
--   2. A DROPPED CHECKER BECOMES UNPROVEN, NOT CLOSED. One checker is left unexercised. The row
--      moves out of CLOSED and the signoff verdict goes false. This is the measurement that makes
--      the report un-gameable: deleting a check cannot improve it.
--
--   3. A FIRING CHECKER IS FAILING, NOT UNPROVEN. A row that both fired and reported no exercises
--      must be filed as FAILING. Ordering those two tests the other way round is how a real bug
--      gets recorded as a stimulus gap, and the ordering is checked here rather than assumed.
--
--   4. AN EMPTY PLAN DOES NOT SIGN OFF. With no row having a checker at all, closure is zero and
--      the verdict is false -- because `100% of nothing` is the arithmetic every vacuous report is
--      built on.

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

entity spi_closure_tb is
end entity spi_closure_tb;

architecture tb of spi_closure_tb is

    constant NROWS  : positive := 18;
    constant HALF_T : time     := 5 ns;

    -- Row 0..7   Chapter 16.1's pin rules
    -- Row 8..14  Chapter 17.1's properties
    -- Row 15     bit order                   -- no checker, ever (16.1)
    -- Row 16     a one-flop synchroniser     -- no checker, ever (15.9)
    -- Row 17     asynchronous reset release  -- no checker, ever (15.9)

    signal clk      : std_logic := '0';
    signal rst_n    : std_logic := '1';
    signal done_sim : boolean   := false;

    signal has_checker : std_logic_vector(NROWS - 1 downto 0) := (others => '0');
    signal exercised   : std_logic_vector(NROWS - 1 downto 0) := (others => '0');
    signal fired       : std_logic_vector(NROWS - 1 downto 0) := (others => '0');
    signal sample      : std_logic := '0';

    signal st : row_state_arr_t(NROWS - 1 downto 0);
    signal n_closed, n_failing, n_unproven, n_no_checker, closure_pct : natural;
    signal signed_off : std_logic;

    signal errors : integer := 0;

begin

    clk_gen : process is
    begin
        while not done_sim loop
            wait for HALF_T;
            clk <= not clk;
        end loop;
        wait;
    end process clk_gen;

    u_c : entity work.spi_closure
        generic map (NROWS => NROWS)
        port map (clk => clk, rst_n => rst_n,
                  has_checker => has_checker, exercised => exercised, fired => fired,
                  sample => sample, state => st,
                  n_closed => n_closed, n_failing => n_failing, n_unproven => n_unproven,
                  n_no_checker => n_no_checker, closure_pct => closure_pct,
                  signed_off => signed_off);

    main : process is

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

        procedure do_sample is
        begin
            wait until falling_edge(clk);
            sample <= '1';
            wait until falling_edge(clk);
            sample <= '0';
            wait until falling_edge(clk);
        end procedure do_sample;

        -- The plan as it stands after a good regression: fifteen rows with checkers, all exercised,
        -- none firing; three rows with no checker.
        procedure good_run is
        begin
            has_checker <= (17 downto 15 => '0', others => '1');
            exercised   <= (17 downto 15 => '0', others => '1');
            fired       <= (others => '0');
            do_sample;
        end procedure good_run;

        variable g_closed, g_fail, g_unp, g_nc, g_pct : natural;
        variable d_closed, d_unp, d_pct               : natural;
        variable f_closed, f_fail, f_unp              : natural;
        variable e_pct                                : natural;
        variable g_signed, d_signed, f_signed, e_signed : std_logic;

    begin
        rst_n <= '1';
        idle_n(1);
        rst_n <= '0';
        idle_n(4);
        rst_n <= '1';
        idle_n(2);

        -- ==============================================================
        -- 1. A GOOD RUN.
        -- ==============================================================
        good_run;
        g_closed := n_closed; g_fail := n_failing; g_unp := n_unproven;
        g_nc := n_no_checker; g_pct := closure_pct; g_signed := signed_off;

        report "  the plan, after a clean regression:";
        report "    rows ......................... " & integer'image(NROWS);
        report "    CLOSED   (checked, exercised, silent) ... " & integer'image(g_closed);
        report "    FAILING  (a checker fired) ............. " & integer'image(g_fail);
        report "    UNPROVEN (a checker never exercised) ... " & integer'image(g_unp);
        report "    NO CHECKER (and there will not be one) . " & integer'image(g_nc);
        report "    closure over rows that HAVE a checker .. " & integer'image(g_pct) & "%";
        report "    signed off ............................. " & std_logic'image(g_signed);
        report "    row 15 (bit order) is " & state_name(st(15)) &
               ", row 16 (one-flop sync) is " & state_name(st(16)) &
               ", row 17 (async reset release) is " & state_name(st(17));

        if g_closed /= 15 or g_fail /= 0 or g_unp /= 0 or g_nc /= 3 then
            report "  FAIL: the clean run's classification is wrong";
            errors <= errors + 1; wait for 1 ns;
        end if;
        if g_pct /= 100 or g_signed /= '1' then
            report "  FAIL: the clean run did not sign off";
            errors <= errors + 1; wait for 1 ns;
        end if;
        report "    1. fifteen rows CLOSED, three with NO CHECKER, and closure reported as 100% OF THE ROWS THAT HAVE A CHECKER -- with the other three counted in neither the numerator nor the denominator. Those three are bit order, which Chapter 16.1 proved no pin observation can decide; a one-flop synchroniser; and an asynchronous reset release, both of which Chapter 15.9 showed are behaviourally identical to correct designs in every simulation. They are covered by REVIEW, named in the plan, and excluded from the percentage -- because folding them in as covered overstates the signoff and folding them in as gaps produces a number that can never close";

        -- ==============================================================
        -- 2. A DROPPED CHECKER.
        -- ==============================================================
        good_run;
        wait until falling_edge(clk);
        exercised(3) <= '0';           -- one checker present but never reached
        do_sample;
        d_closed := n_closed; d_unp := n_unproven; d_pct := closure_pct; d_signed := signed_off;

        report "  with ONE checker present but never exercised:";
        report "    CLOSED ....... " & integer'image(d_closed) & "      UNPROVEN ....... " &
               integer'image(d_unp);
        report "    closure ...... " & integer'image(d_pct) & "%     signed off ..... " &
               std_logic'image(d_signed);
        report "    row 3 is now " & state_name(st(3));

        if d_unp /= 1 or d_closed /= 14 then
            report "  FAIL: an unexercised checker was not classified as unproven";
            errors <= errors + 1; wait for 1 ns;
        end if;
        if d_signed /= '0' then
            report "  FAIL: the report signed off with an unproven row";
            errors <= errors + 1; wait for 1 ns;
        end if;
        if d_pct >= g_pct then
            report "  FAIL: closure did not fall when a checker went unexercised";
            errors <= errors + 1; wait for 1 ns;
        end if;
        report "    2. the row moved out of CLOSED and into UNPROVEN, closure fell from " &
               integer'image(g_pct) & "% to " & integer'image(d_pct) &
               "%, and the signoff went false. That is what makes the report un-gameable: DELETING A CHECK CANNOT IMPROVE IT. A percentage built on pass/fail would have been unchanged, because a checker that never ran and a checker that passed print the same line";

        -- ==============================================================
        -- 3. A FIRING CHECKER IS FAILING, NOT UNPROVEN.
        -- ==============================================================
        good_run;
        wait until falling_edge(clk);
        fired(5)     <= '1';
        exercised(5) <= '0';           -- fired AND reported no exercises -- a contradiction
        do_sample;
        f_closed := n_closed; f_fail := n_failing; f_unp := n_unproven; f_signed := signed_off;

        report "  with ONE checker that fired AND reported no exercises:";
        report "    CLOSED " & integer'image(f_closed) & "   FAILING " & integer'image(f_fail) &
               "   UNPROVEN " & integer'image(f_unp) & "   signed off " &
               std_logic'image(f_signed);
        report "    row 5 is " & state_name(st(5));

        if f_fail /= 1 or f_unp /= 0 then
            report "  FAIL: a row that fired was classified as unproven rather than failing";
            errors <= errors + 1; wait for 1 ns;
        end if;
        if f_signed /= '0' then
            report "  FAIL: the report signed off with a failing row";
            errors <= errors + 1; wait for 1 ns;
        end if;
        report "    3. the row was classified FAILING, not UNPROVEN. The two tests are ordered deliberately -- fired first, exercised second -- because a checker that fired was obviously reached, and the other ordering files a real bug as a stimulus gap. That is a one-line decision inside the aggregator and it decides which of two very different bug reports a team receives";

        -- ==============================================================
        -- 4. AN EMPTY PLAN DOES NOT SIGN OFF.
        -- ==============================================================
        wait until falling_edge(clk);
        has_checker <= (others => '0');
        exercised   <= (others => '0');
        fired       <= (others => '0');
        do_sample;
        e_pct := closure_pct; e_signed := signed_off;

        report "  with NO row having a checker at all:";
        report "    closure " & integer'image(e_pct) & "%   NO CHECKER " &
               integer'image(n_no_checker) & "   signed off " & std_logic'image(e_signed);

        if e_signed /= '0' or e_pct /= 0 then
            report "  FAIL: an empty plan signed off";
            errors <= errors + 1; wait for 1 ns;
        end if;
        report "    4. closure zero and the verdict false. `100% of nothing` is the arithmetic every vacuous report is built on, and the guard against it is the same one Chapter 16.1 put on its rules and Chapter 17.1 on its properties: require that something was actually checked before believing that everything passed";

        wait for 1 ns;
        if errors = 0 then
            report "PASS: closure is a question about a PLAN, not a percentage, because a plan row can be in four states and a percentage collapses them to one. CLOSED means a checker exists, was exercised, and stayed silent; FAILING means it fired; UNPROVEN means it exists and was NEVER REACHED -- which is the state every dead checker in this curriculum was found in, and which prints the same green line as CLOSED in any pass/fail summary; and NO CHECKER means there is not going to be one. Aggregating the whole module's eighteen rows: fifteen CLOSED, three NO CHECKER, and closure reported as " &
                   integer'image(g_pct) &
                   "% OF THE ROWS THAT HAVE A CHECKER, with bit order, the one-flop synchroniser and the asynchronous reset release counted in neither the numerator nor the denominator -- named in the plan, covered by review, and excluded from the number, because folding them in as covered overstates the signoff and folding them in as gaps produces a figure that can never close. Leaving one checker unexercised moved its row out of CLOSED, dropped closure to " &
                   integer'image(d_pct) &
                   "% and made the verdict false, which is what makes the report un-gameable: DELETING A CHECK CANNOT IMPROVE IT. A row that both fired and reported no exercises was classified FAILING rather than UNPROVEN, because the two tests are ordered fired-first -- the other ordering files a real bug as a stimulus gap. And a plan in which no row has a checker reports zero and refuses to sign off, because `100% of nothing` is the arithmetic every vacuous report is built on. In VHDL each row's state is a named ENUMERATION value rather than a bit in one of four parallel vectors, which is where a row ends up counted twice or not at all"
                severity note;
        else
            report "FAIL: " & integer'image(errors) & " error(s)" severity error;
        end if;

        done_sim <= true;
        wait for 100 ns;
        std.env.stop;
    end process main;

end architecture tb;

// A plan row, and the three things it must carry beyond its name. `has_checker` is what makes a
// NO CHECKER row a declared fact rather than an inference from silence, and `covered_by` is the
// field a signoff meeting actually asks about.
typedef struct {
  string name;
  bit    has_checker;
  string covered_by;      // "assertion", "scoreboard", "coverage", "review"
  string reason;          // why there is no checker, for the rows that have none
} spi_plan_row_t;

class spi_closure extends uvm_component;
  `uvm_component_utils(spi_closure)

  spi_plan_row_t plan[$];

  function void build_phase(uvm_phase phase);
    super.build_phase(phase);
    // The eight pin rules and the seven properties, abbreviated.
    foreach (rule_names[i]) plan.push_back('{rule_names[i], 1, "assertion", ""});
    foreach (prop_names[i]) plan.push_back('{prop_names[i], 1, "assertion", ""});

    // THE THREE ROWS WITH NO CHECKER, declared with their reasons. This is the part that is
    // normally a paragraph in a document nobody opens at signoff.
    plan.push_back('{"bit order", 0, "scoreboard",
                     "no pin observation decides it; both orders are well-formed frames"});
    plan.push_back('{"one-flop synchroniser", 0, "review",
                     "behaviourally identical in simulation; a simulator models no settling time"});
    plan.push_back('{"async reset release", 0, "review",
                     "behaviourally identical in simulation; a simulated flop leaves reset cleanly"});
  endfunction

  // The four states, from the numbers the environment already has. `exercised` comes from an
  // ANTECEDENT COVER for an assertion row and from a match count for a scoreboard row -- and a row
  // with neither is a row whose verdict is guesswork.
  function void report_phase(uvm_phase phase);
    int closed, failing, unproven, no_checker;

    foreach (plan[i]) begin
      if (!plan[i].has_checker) begin
        no_checker++;
        `uvm_info("CLOSURE", $sformatf("NO CHECKER  %s -- %s (covered by %s)",
                  plan[i].name, plan[i].reason, plan[i].covered_by), UVM_LOW)
      end
      // FIRED IS TESTED FIRST. A row that both fired and shows no exercises is a real failure, and
      // the other ordering files it as a stimulus gap.
      else if (fired(i)) begin
        failing++;
        `uvm_error("CLOSURE_FAIL", $sformatf("FAILING  %s", plan[i].name))
      end
      else if (!exercised(i)) begin
        unproven++;
        // A uvm_error, not a warning. An unproven row is not a lesser kind of pass -- it is the
        // absence of a result, and a warning is how it survives to signoff.
        `uvm_error("CLOSURE_UNPROVEN",
                   $sformatf("UNPROVEN  %s -- its checker was never exercised", plan[i].name))
      end
      else closed++;
    end

    // Closure over the rows that HAVE a checker, with the no-checker rows reported separately.
    if (closed + failing + unproven > 0)
      `uvm_info("CLOSURE", $sformatf("closure %0d%% of %0d checkable rows; %0d rows have no checker",
                (closed * 100) / (closed + failing + unproven),
                closed + failing + unproven, no_checker), UVM_LOW)

    // AND THE VACUITY GUARD ON THE VERDICT ITSELF.
    if (closed + failing + unproven == 0)
      `uvm_error("CLOSURE_EMPTY", "no plan row has a checker; there is nothing to sign off")
  endfunction
endclass

   Symptom          a block is signed off at 100% coverage with a clean
                    regression. A bug escapes on a path the plan lists a checker
                    for.

   What happened    the checker's antecedent had been unreachable for months. The
                    closure report was built from pass/fail, so the row read as
                    CLOSED -- a checker that never ran and a checker that passed
                    print the same line.

   What would have  a closure report with an UNPROVEN state, fed by antecedent
   caught it        covers rather than by the absence of failures. The row would
                    have moved out of CLOSED on the commit that broke it, and the
                    closure number would have fallen.

   The tell         the failing row's checker has a narrow precondition -- a gap,
                    a coincidence, a mode. Continuous obligations are exercised by
                    any traffic and rarely go dead. Rows with narrow preconditions
                    go dead quietly and stay dead, which is Chapter 16.1's
                    failure signature reappearing at signoff.