SmartNICs

Chapter 23.4 built a NIC whose behaviour was fixed at tape-out. This chapter makes it programmable, and the three quantities that change are an instruction budget, an area, and the moment the device's behaviour is decided.

Row three is the figure to carry. A 64-core packet-processing array running at 1.5 GHz gives 645 instructions per packet — enough for a firewall, a tunnel encapsulation, a flow table lookup and a rewrite, and nowhere near enough for a full transport implementation.

Set against the host it is offloading.

So a 64-core array is worth about eleven host cores of packet-processing work — which is the entire commercial argument for the part, and it is an argument about the host's cost rather than the NIC's.

Then the area, in Chapter 23.3 §2's unit.

A programmable datapath costs 197 times the fixed-function blocks it replaces, and makes Chapter 23.4's NIC 44% larger.

And the third change is not a number at all.

Row four is Section 20's refused property, and Section 11 is the mechanism — a verifier in the load path — that turns an open quantification back into a closed one.

1. Scope — What "Programmable" Costs, in Instructions and in Area

Scope: what work moves onto a programmable NIC, what the per-packet instruction budget is, what the programmability costs in area, and what it does to verification.

Not in scope: the transport. Whether a SmartNIC terminates TCP, implements RDMA or runs a virtual switch is a product decision; this chapter prices the capacity to do such things and leaves the choice of which to somebody else.

Three questions, and the third is the one the track has not met before.

Question 3 is new to the track. Every earlier chapter verified a design — a MAC, a PHY, a switch pipeline, a NIC — whose behaviour was fully determined by the silicon. A SmartNIC's behaviour is determined by silicon plus a program, and the program is loaded by an operator, after the part shipped, from a set that did not exist when the part was verified.

And one framing that runs through the chapter.

A fixed-function block is a program that was compiled into silicon. The difference is not what it computes — it is when the computation was chosen, and therefore what could be proved about it.

Which makes the comparison in Section 17 a three-way one rather than a two-way one.

Rows four and five are the trade, and they are the same trade every programmable system makes. What this chapter adds is the price in Chapter 23.3 §2's unit and the per-packet budget, both of which are usually asserted rather than derived.

2. The Per-Packet Instruction Budget

One division sets the whole architecture.

instructions per packet = cores × frequency × IPC ÷ packets per second

At 148.81 Mpps.

And read the other way, which is how a design is actually sized.

Row five is where the approach stops being viable, and it is worth saying why in area terms rather than in principle: 198 cores at 30 kGE each is 1.70 × 10⁷ BCE of logic plus 5.19 × 10⁷ of instruction memory — 243 MAC receive datapaths — which is a large fraction of Chapter 23.4's entire NIC for one program's worth of work.

What fits in the budget, at 645 instructions.

Rows six and seven are where a SmartNIC stops being a general-purpose processor and starts being a processor with accelerators bolted to it, which is what every real one is. The programmable cores do the decisions and fixed-function engines do the bulk arithmetic — a checksum, a cipher, a hash — because the instruction budget can afford a decision and cannot afford a loop over the payload.

The budget is per packet, not per octet. Anything that touches every byte must be fixed function, and anything that touches a header can be a program.

One number makes that concrete. AES-GCM over a 1 500-octet payload at even two octets per instruction is 750 instructions — more than the entire 64-core budget for one packet — so a design that encrypts in software sustains at most 128 Mpps of otherwise-zero processing, and in practice far less. A fixed-function AES engine does it at one packet per cycle for a few hundred thousand BCE.

3. RTL 1 — The SmartNIC Package and the Instruction Budget

// ---------------------------------------------------------------------
// smartnic_pkg -- a programmable NIC, and the one division that sets
// its architecture.
//
// Chapter 23.3's package held an area model; Chapter 23.4's held a
// bandwidth model. This one holds a COMPUTE model, because the
// quantity a SmartNIC rations is instructions per packet -- and
// Section 10 shows the quantity it cannot ration at all is which
// instructions.
// ---------------------------------------------------------------------
package smartnic_pkg;

  // ---- the wire, unchanged from Chapter 23.4 -----------------------------
  localparam int RATE_GBPS    = 100;
  localparam int PPS_MILLION  = 148;

  // ---- the compute array ------------------------------------------------
  localparam int CORES        = 64;
  localparam int CORE_MHZ     = 1500;
  localparam int IPC          = 1;
  localparam int IMEM_KB      = 32;
  localparam int CORE_GE      = 30000;

  // ---- the area unit, from Chapter 23.3 Section 2 ------------------------
  localparam int BCE_PER_FLOP = 20;
  // 1 GE = 1 / 0.35 BCE, expressed as a scaled integer.
  localparam int BCE_PER_GE_X100 = 286;
  localparam int DATAPATH_BCE = 283320;

  // ---- the budget --------------------------------------------------------
  function automatic int instr_per_packet();
    return (CORES * CORE_MHZ * IPC * 1000) / PPS_MILLION;
  endfunction

  function automatic int cores_for(int instr);
    return (instr * PPS_MILLION) / (CORE_MHZ * 1000 * IPC);
  endfunction

  // A host core, for the comparison that justifies the part.
  localparam int HOST_MHZ = 3000;
  localparam int HOST_IPC = 3;
  function automatic int host_instr_per_packet();
    return (HOST_MHZ * HOST_IPC * 1000) / PPS_MILLION;
  endfunction

  // ---- area --------------------------------------------------------------
  function automatic int array_bce();
    return (CORES * CORE_GE * BCE_PER_GE_X100) / 100
         + (CORES * IMEM_KB * 1024 * 8);
  endfunction

  // Chapter 18.7 Section 18's fixed-function offload set, for the ratio.
  localparam int FIXED_OFFLOAD_FLOPS = 5650;
  localparam int FIXED_OFFLOAD_BCE   = FIXED_OFFLOAD_FLOPS * BCE_PER_FLOP;

  // ---- what a program is --------------------------------------------------
  // The device's behaviour is a function of THIS, and it arrives after
  // the silicon does.
  typedef struct packed {
    logic [31:0] program_id;
    logic [15:0] instruction_count;
    logic [15:0] worst_case_instructions;   // often unknown
    logic [31:0] signature;
    logic        bounded_loops;             // a verifier's verdict
    logic        verified;
  } program_t;

  // Section 12: what a load-time verifier can and cannot establish.
  typedef enum logic [2:0] {
    VER_NONE        = 3'd0,
    VER_SIGNATURE   = 3'd1,   // it came from somebody we trust
    VER_TERMINATION = 3'd2,   // it halts
    VER_BUDGET      = 3'd3,   // it halts within N instructions
    VER_MEMORY      = 3'd4,   // it touches only what it may
    VER_FULL        = 3'd5    // all of the above
  } verification_level_e;

endpackage

Classification: a compute model, and its last declaration is a list of things a load-time check can establish.

What it teaches: that program_t.worst_case_instructions is a field that is often unknown and is the one the design depends on. An array sized for 645 instructions per packet sustains line rate only if every packet's program path fits in 645; a program whose worst case is 1 200 sustains 80 Mpps on the traffic that triggers it — Section 13's arithmetic. The mean is irrelevant and the worst case is frequently not computed, because computing it is a static-analysis problem the program's author had no reason to solve.

And it teaches that verification_level_e is a ladder with a top rung that is reachable. A loaded program can be checked for a signature (cheap, and establishes provenance rather than behaviour), termination, an instruction budget, and memory safety — and the last three are decidable for the restricted languages real SmartNICs use. That is the mechanism that closes Section 20's open quantification, and it lives in the load path rather than in a property.

Deliberately simplified: IPC = 1 where real packet cores are often multi-issue or multi-threaded, and a multi-threaded core hides memory latency in a way this model cannot express. CORE_GE = 30000 is a plausible figure for a small RISC core with a packet-oriented instruction set and varies by a factor of three across real designs. instr_per_packet assumes every core is available to every packet, ignoring the scheduler and any per-core specialisation. And program_t has no notion of several programs loaded at once, which every real device supports and which multiplies the verification problem.

Production implication: the missing multi-program case is where the load-time verifier's job becomes genuinely hard, and it is the normal deployment. Two programs that are each individually within budget can exceed it together — 400 instructions plus 400 is 800 against 645 — and two programs that are each memory-safe can interfere if they share a table. So the verifier's verdict cannot be per program; it must be over the loaded set, re-evaluated on every load and unload, which makes it a global check at a moment when the device is running at line rate. The practical answer is to verify against a static budget allocation per program — each program declares its share and the verifier checks the sum — which is weaker than verifying the composition and is the only thing that is affordable.

// ---------------------------------------------------------------------
// instruction_budget -- the division of Section 2, as a block, with the
// worst case separated from the mean.
//
// The block exists because a SmartNIC's throughput is set by the WORST
// path through the loaded program and every measurement people take
// reports the mean.
// ---------------------------------------------------------------------
module instruction_budget
  import smartnic_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] pps_million,
  input  logic [15:0] cores,
  input  logic [15:0] core_mhz,
  input  logic [7:0]  ipc,
  input  logic [15:0] program_mean_instr,
  input  logic [15:0] program_worst_instr,

  output logic [31:0] budget_per_packet,
  output logic [15:0] sustained_mpps_mean,
  output logic [15:0] sustained_mpps_worst,
  output logic [15:0] worst_case_pct_of_line,
  output logic        fits_at_mean,
  output logic        fits_at_worst,
  output logic [15:0] cores_needed_worst,
  output logic [15:0] host_cores_equivalent
);
  logic [31:0] array_mips;

  always_comb begin
    array_mips = 32'(cores) * 32'(core_mhz) * 32'(ipc);   // millions/s

    budget_per_packet = (pps_million == 0) ? 32'hFFFF_FFFF
                      : (array_mips / 32'(pps_million));

    sustained_mpps_mean = (program_mean_instr == 0) ? 16'hFFFF
                        : 16'(array_mips / 32'(program_mean_instr));
    sustained_mpps_worst = (program_worst_instr == 0) ? 16'hFFFF
                         : 16'(array_mips / 32'(program_worst_instr));

    worst_case_pct_of_line = (pps_million == 0) ? 16'd0
                           : (sustained_mpps_worst * 16'd100) / pps_million;

    fits_at_mean  = (sustained_mpps_mean  >= pps_million);
    fits_at_worst = (sustained_mpps_worst >= pps_million);

    cores_needed_worst = 16'((32'(program_worst_instr) * 32'(pps_million))
                             / (32'(core_mhz) * 32'(ipc)));

    // The commercial argument: how many host cores this array replaces.
    host_cores_equivalent = 16'(array_mips
                                / (32'(HOST_MHZ) * 32'(HOST_IPC)));
  end
endmodule

Classification: a division, computed twice — once with the mean and once with the worst case.

What it teaches: that fits_at_mean and fits_at_worst can differ, and only the second matters. A program averaging 400 instructions on a 64-core array fits comfortably at the mean — 240 Mpps against a required 148.81 — and a worst case of 1 200 gives 80 Mpps, 53.8% of line rate. The part is at line rate on ordinary traffic and at half on traffic that takes the long path, and which traffic that is depends on packet contents.

And it teaches that host_cores_equivalent is the number that sells the part. A 64-core array at 1.5 GHz executes 96 000 million instructions per second; a 3 GHz host core at 3 IPC executes 9 000 — so the array is worth 10.7 host cores. That comparison is the commercial case and it is independent of the packet rate, which is why it survives every workload argument.

Deliberately simplified: the model assumes perfect load balancing across cores, which a real scheduler approximates; a run-to-completion model with packets pinned to cores has the same balls-in-bins problem Chapter 23.2 §10 derived for uplinks. program_worst_instr is an input that a static analyser must supply and frequently cannot. There is no memory-latency term, so a program that misses a table lookup stalls in a way the model does not represent. And host_cores_equivalent compares raw instruction throughput, ignoring that a host core's instructions are wider and its memory system faster.

Production implication: the perfect-load-balancing assumption is the one that turns an adequate array into an inadequate one, and the mechanism is familiar. A run-to-completion architecture assigns a packet to a core and keeps it there for the packet's whole program, so the cores are bins and the packets are balls — and Chapter 23.2 §10's arithmetic applies exactly. With 64 cores and packets arriving at 148.81 Mpps, a long-running packet occupies its core for the whole of its program, and a burst of long-path packets can leave most of the array idle while a few cores are saturated. The remedy is the same one that chapter found: more, smaller units of work — split the program into stages and pipeline them across cores rather than running each packet to completion — which trades per-packet locality for utilisation.

4. Six Hundred and Forty-Five Instructions, and What Fits In Them

Section 2 gave the budget. This section spends it, and the spending pattern explains the architecture of every real SmartNIC.

What a program does per packet, by category.

Rows one to four are all header work and they all fit. A realistic composition — parse, two lookups, a rewrite and a connection update — is 200 to 390 instructions, comfortably inside 645. Row five does not fit and never will, because its cost scales with the payload and the budget does not.

The arithmetic that makes row five hopeless.

And the consequence is the structure every SmartNIC has.

The programmable cores make decisions about headers; fixed-function engines transform payloads. The budget is per packet and a payload is per octet, so the two cannot be done by the same mechanism.

Which gives the part's real shape.

Row one costs more than every other row combined by two orders of magnitude, and it is the row that can be changed after shipping. That is the entire trade: 197× the area of the fixed-function set, for the ability to decide what the part does after it is in a rack.

One qualification about the instruction counts. The figures above are for a packet-oriented instruction set — one with fields addressed by name, table lookups as single instructions and no general-purpose addressing. A general-purpose ISA doing the same work needs two to four times as many instructions, which is why SmartNIC cores are not simply small ARM or RISC-V cores in most designs, and why the ones that are need correspondingly more of them.

5. RTL 2 — The Core Array

// ---------------------------------------------------------------------
// core_array -- 64 packet cores, a scheduler, and the balls-in-bins
// problem that Chapter 23.2 Section 10 derived for uplinks arriving
// here for cores.
//
// A run-to-completion array assigns a packet to a core and keeps it
// there for the whole program. Cores are bins, packets are balls, and
// a long-running packet holds its bin.
// ---------------------------------------------------------------------
module core_array
  import smartnic_pkg::*;
#(
  parameter int N = CORES              // 64
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        pkt_arrives,
  input  logic [15:0] pkt_instructions,      // this packet's path length
  input  logic        run_to_completion,

  output logic        accepted,
  output logic [6:0]  assigned_core,
  output logic [6:0]  cores_busy,
  output logic [15:0] core_remaining [N],
  output logic [15:0] utilisation_pct,
  output logic        array_saturated,
  output logic [31:0] c_accepted,
  output logic [31:0] c_rejected,
  output logic [15:0] longest_occupancy
);
  logic [6:0] free_core;
  logic       any_free;

  always_comb begin
    any_free  = 1'b0;
    free_core = 7'd0;
    cores_busy = 7'd0;
    longest_occupancy = 16'd0;
    for (int i = 0; i < N; i++) begin
      if (core_remaining[i] == 16'd0) begin
        if (!any_free) begin any_free = 1'b1; free_core = 7'(i); end
      end else begin
        cores_busy = cores_busy + 7'd1;
        if (core_remaining[i] > longest_occupancy)
          longest_occupancy = core_remaining[i];
      end
    end

    accepted      = pkt_arrives && any_free;
    assigned_core = free_core;
    array_saturated = pkt_arrives && !any_free;

    utilisation_pct = 16'((32'(cores_busy) * 100) / N);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_accepted <= '0; c_rejected <= '0;
      for (int i = 0; i < N; i++) core_remaining[i] <= '0;
    end else begin
      for (int i = 0; i < N; i++)
        if (core_remaining[i] != 16'd0)
          core_remaining[i] <= core_remaining[i] - 16'd1;

      if (accepted) begin
        // Run to completion: the core is held for the WHOLE program,
        // so a long path holds a core for a long time.
        core_remaining[assigned_core] <= run_to_completion
                                       ? pkt_instructions
                                       : 16'd1;    // pipelined: one stage
        c_accepted <= c_accepted + 32'd1;
      end else if (pkt_arrives) begin
        c_rejected <= c_rejected + 32'd1;
      end
    end
  end
endmodule

Classification: a run-to-completion scheduler, and its failure mode is Chapter 23.2 §10's in a new setting.

What it teaches: that run_to_completion chooses between two completely different utilisation behaviours. With it true, a packet holds a core for its whole program — so a burst of 1 200-instruction packets occupies 64 cores for 800 nanoseconds and rejects everything that arrives meanwhile. With it false, the array is a pipeline: each core does one stage, packets flow through, and a long packet occupies each stage for one cycle. The second utilises better and loses per-packet locality, which is why a program with a large working set prefers the first.

And it teaches that longest_occupancy is the quantity that predicts rejection. The array saturates not when it is busy on average but when every core is simultaneously held, and a run-to-completion array with variable path lengths has exactly Chapter 23.2 §10's balls-in-bins distribution — a few cores holding long packets while the rest idle, and arrivals rejected because the free ones happen to be the wrong ones.

Deliberately simplified: the free-core search is a linear scan over 64 entries, combinational, which at 148.81 Mpps is a 64-way priority encoder and is fine. core_remaining decrements once per clock for every core, modelling one instruction per cycle with no stalls — a table lookup that misses stalls for hundreds of cycles and the model has no way to say so. run_to_completion false models a pipeline as a single stage. And a rejected packet is simply counted, where a real design buffers it, punts it or drops it, and the choice matters.

Production implication: the missing memory-stall term is what makes a real array's utilisation far worse than this model's, and it is the reason packet cores are multi-threaded. A program that performs three table lookups, each missing a local cache and costing 200 cycles, spends 600 of its budget stalled — and a single-threaded core is idle for all of it. Four-way multi-threading lets three other packets use those cycles, which raises utilisation roughly fourfold for the same core count and is why real packet cores have several hardware threads and a small register file per thread. The model's IPC = 1 is best read as one instruction per thread-cycle, and a design that sizes an array from it without threading needs four times the cores.

6. What a Programmable Datapath Costs Against the Blocks It Replaces

Chapter 18.7 §18 priced a fixed-function offload set. This section prices the programmable array that would do the same work, in Chapter 23.3 §2's unit.

The fixed-function set.

The programmable array that replaces the first five rows.

The ratio is 197.

A programmable datapath costs 197 times the fixed-function blocks it replaces, and two thirds of that cost is instruction memory rather than cores.

Row two of the second table is the one people forget. The cores are 19.4 datapaths; the memory to hold their programs is 59.2 — three times more. A design that reduces the instruction memory from 32 kB to 8 kB per core saves 44.4 datapaths, 57% of the array, at the cost of program size.

And against Chapter 23.4's NIC.

A SmartNIC is about 44% larger than the fixed-function NIC it is built from, and every bit of that increase buys the same thing: the ability to decide what the part does after it ships.

One comparison that puts the ratio in perspective.

The array is ninety-four times the forwarding logic of a 6.4 Tb/s switch. That is not an argument against it — a switch's pipeline does one fixed thing very fast and the array does an arbitrary thing rather fast — but it is the number to have when somebody describes programmability as cheap.

7. RTL 3 — The Fixed-Versus-Programmable Comparator

// ---------------------------------------------------------------------
// offload_comparator -- the same function, two ways, priced in the
// same unit.
//
// The block exists so that "should this be fixed function or a
// program" is answered with two numbers rather than a preference.
// ---------------------------------------------------------------------
module offload_comparator
  import smartnic_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] fixed_flops,
  input  logic [15:0] program_instructions,
  input  logic [15:0] pps_million,
  input  logic        touches_every_octet,
  input  logic [15:0] expected_changes_per_year,

  output logic [31:0] fixed_bce,
  output logic [31:0] prog_bce,
  output logic [15:0] ratio,
  output logic [15:0] cores_required,
  output logic        must_be_fixed,
  output logic        should_be_programmable,
  output logic [31:0] bce_per_change
);
  always_comb begin
    fixed_bce = 32'(fixed_flops) * 32'(BCE_PER_FLOP);

    cores_required = 16'((32'(program_instructions) * 32'(pps_million))
                         / (32'(CORE_MHZ) * 1000 * 32'(IPC)));

    prog_bce = (32'(cores_required) * CORE_GE * BCE_PER_GE_X100) / 100
             + (32'(cores_required) * IMEM_KB * 1024 * 8);

    ratio = (fixed_bce == 0) ? 16'hFFFF
          : 16'(prog_bce / fixed_bce);

    // Section 4: anything whose cost scales with the payload cannot be
    // a program, whatever the area says.
    must_be_fixed = touches_every_octet;

    // The honest criterion: programmability is worth its area when the
    // function is expected to change.
    should_be_programmable = !touches_every_octet &&
                             (expected_changes_per_year > 16'd0);

    // The figure a product decision actually needs: area per change.
    bce_per_change = (expected_changes_per_year == 0) ? 32'hFFFF_FFFF
                   : ((prog_bce - fixed_bce)
                      / 32'(expected_changes_per_year));
  end
endmodule

Classification: a two-number comparison with one categorical override.

What it teaches: that must_be_fixed overrides everything and is a property of the function, not of the economics. A transformation that touches every octet costs instructions proportional to the payload, and the budget is per packet — so no core count makes it work. Section 4's table: a 1 500-octet AES pass is 750 instructions, more than the entire 64-core budget for one packet. The comparator refuses the question rather than answering it.

And it teaches that bce_per_change is the figure a product decision needs and nobody computes. Programmability costs 2.23 × 10⁷ BCE more than the fixed set; if the function changes twice a year over a five-year life that is 2.23 × 10⁶ BCE per change — and the comparison is then against what a re-spin costs, which is a different currency entirely. The block makes the trade explicit rather than settling it.

Deliberately simplified: cores_required sizes the array from the program's instruction count and one line rate, ignoring that a real array is sized once for all programs it will ever run. prog_bce scales instruction memory with the core count, which is right for a per-core memory and wrong for a shared one. ratio is integer division, so a ratio under 1 reads as 0. And expected_changes_per_year is an input that nobody can supply honestly — it is the whole uncertainty of the decision, reduced to a parameter.

Production implication: the shared-instruction-memory option is the one that changes the arithmetic most and it is under-used. Section 6 showed instruction memory is 59.2 of the array's 78.6 datapaths — three quarters of it — and per-core memories are replicated 64 times to hold the same program. A design with one shared instruction memory and per-core caches holds 32 kB once rather than 64 times: 2.62 × 10⁵ BCE instead of 1.68 × 10⁷, a factor of 64 — at the cost of an instruction-fetch bandwidth problem that is exactly Chapter 23.3 §7's banked-lookup problem in a new place. The trade is real, the saving is enormous, and the reason per-core memories persist is that fetch bandwidth at 64 cores × 1.5 GHz is 96 billion instructions per second.

8. What Actually Moves Off the Host

The commercial case is that a SmartNIC removes work from the host. This section says how much, in the host's own unit.

Section 2's comparison, restated.

And per packet, which is how a workload is actually sized.

Which functions are worth moving, by that measure.

Row five is the case that justifies the part, and it is worth reading carefully: a SmartNIC running all four functions frees between four and eight host cores per 100 Gb/s port. On a host with 64 cores that is 6 to 12 per cent of the machine, recovered for the workload the machine was bought to run.

And the honest counter-argument, which is arithmetic rather than opinion.

Whether that trade is worth making depends on numbers this chapter cannot supply — the relative cost of a NIC's die area against a server's CPU sockets, and how many ports share one host. What it can supply is the two quantities, and the decision is then arithmetic rather than a preference.

One asymmetry that decides it in practice. A host core freed on one machine is worth one core; a SmartNIC design is amortised across every machine that ships with it. So the trade favours the NIC when the fleet is large and the function is stable, and favours the host when the fleet is small or the function changes often — which is the opposite of the intuition that programmability suits change. Programmability suits change in the function; the decision to have a programmable part at all suits stability in the deployment.

9. RTL 4 — The Program Loader

// ---------------------------------------------------------------------
// program_loader -- the moment the device's behaviour is decided.
//
// Every earlier chapter in this track verified a design whose behaviour
// was fixed by the silicon. This block is where that stops being true,
// and Section 20's refused property is what happens to a proof that was
// written before this block ran.
// ---------------------------------------------------------------------
module program_loader
  import smartnic_pkg::*;
#(
  parameter int SLOTS = 8            // programs resident at once
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        load_req,
  input  logic [31:0] load_program_id,
  input  logic [15:0] load_instr_count,
  input  logic [15:0] load_worst_case,
  input  logic        load_signature_ok,
  input  logic        load_verifier_ok,
  input  verification_level_e load_level,
  input  logic        unload_req,
  input  logic [2:0]  unload_slot,

  output logic        load_accepted,
  output logic [2:0]  load_slot,
  output logic [15:0] total_worst_case,
  output logic        budget_exceeded,
  output logic        unverified_resident,
  output logic [2:0]  slots_used,
  output logic [31:0] c_loads,
  output logic [31:0] c_rejected_loads,
  output logic [31:0] c_loads_since_verification
);
  program_t slot [SLOTS];
  logic [SLOTS-1:0] occupied;

  logic [2:0] free_slot;
  logic       any_free;

  always_comb begin
    any_free = 1'b0; free_slot = 3'd0;
    slots_used = 3'd0;
    total_worst_case = 16'd0;
    unverified_resident = 1'b0;
    for (int i = 0; i < SLOTS; i++) begin
      if (!occupied[i]) begin
        if (!any_free) begin any_free = 1'b1; free_slot = 3'(i); end
      end else begin
        slots_used = slots_used + 3'd1;
        // Section 3's production note: programs COMPOSE, so the budget
        // is over the loaded SET and not over any one member.
        total_worst_case = total_worst_case + slot[i].worst_case_instructions;
        if (!slot[i].verified) unverified_resident = 1'b1;
      end
    end

    budget_exceeded = ((total_worst_case + load_worst_case) >
                       16'(instr_per_packet()));

    load_accepted = load_req && any_free && load_signature_ok
                  && load_verifier_ok && !budget_exceeded;
    load_slot = free_slot;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      occupied <= '0; c_loads <= '0; c_rejected_loads <= '0;
      c_loads_since_verification <= '0;
    end else begin
      if (load_accepted) begin
        slot[load_slot].program_id              <= load_program_id;
        slot[load_slot].instruction_count       <= load_instr_count;
        slot[load_slot].worst_case_instructions <= load_worst_case;
        slot[load_slot].bounded_loops           <= (load_level >= VER_BUDGET);
        slot[load_slot].verified                <= (load_level == VER_FULL);
        occupied[load_slot] <= 1'b1;
        c_loads <= c_loads + 32'd1;
        // The counter that names the chapter's problem: how many
        // behaviours this device has had since anybody proved anything
        // about it.
        c_loads_since_verification <= c_loads_since_verification + 32'd1;
      end else if (load_req) begin
        c_rejected_loads <= c_rejected_loads + 32'd1;
      end
      if (unload_req) occupied[unload_slot] <= 1'b0;
    end
  end
endmodule

Classification: an admission control for behaviour, and its most telling output is a count of how many behaviours the device has had.

What it teaches: that budget_exceeded is computed over the loaded set and not over the arriving program. Two programs that each fit in 645 instructions do not both fit — 400 plus 400 is 800 — so the loader must hold a running sum and refuse a load that breaks it. That is a global check performed at line rate, on a device whose whole point is that programs arrive while it runs.

And it teaches that c_loads_since_verification is the number a compliance argument needs and no device reports. Every load changes the device's behaviour; a proof written before the first load ranged over the programs that existed then. A device that has been loaded forty times since anything was proved about it is running a behaviour nobody has examined, and that fact is a counter rather than a philosophy.

Deliberately simplified: budget_exceeded sums worst cases, which is correct and conservative, and a real device would want the sum of worst cases along a single packet's path rather than across all resident programs — a packet usually runs one. load_verifier_ok is an input: the verifier itself is Section 11. There is no notion of a program being active rather than merely resident, and eight resident programs of which one runs is a very different budget from eight that all run. And an unload does not check whether a packet is mid-program in that slot.

Production implication: the mid-program unload is the hazard that turns a management operation into a corruption, and it is the same shape as Chapter 23.3 §7's table update. A program unloaded while a packet is executing it leaves that packet running instructions from a slot that is being overwritten — the packet's behaviour is then a mixture of two programs, which is neither and was never verified as either. The remedy is the same one that chapter found: a valid bit, cleared first, so no new packet enters the slot, and a drain before the memory is reused. The drain is bounded by the worst-case program length — 1 200 instructions is 800 nanoseconds at 1.5 GHz — so it costs under a microsecond and is the difference between an atomic operation and an undefined one.

10. The Device's Behaviour Is Decided After It Ships

Every chapter in Modules 19 to 23 has verified a design. This is the first whose behaviour is not fully determined by the thing that was verified.

The difference, stated precisely.

Row four is the chapter's verification problem in one line. A property of the form for every program P, invariant I holds is proved over the programs that existed when it was written, and the device's future programs are not in that set. The property was correctly scoped when written and becomes wrongly scoped the moment a new program is loaded.

And the scale of the gap is a counter, not a philosophy.

Three things this does not mean, because the argument is easy to overstate.

Row two is the important one and it rests on a restriction. A general-purpose program's termination is undecidable; a packet-processing program's is not, because the languages real SmartNICs accept forbid unbounded loops. Restricting the language converts an undecidable question into a decidable one, and that restriction is the load-time verifier's whole foundation.

The fix for an open quantification is not a stronger property. It is a mechanism in the load path that makes the quantification closed again.

Which is a different kind of answer from any earlier chapter's.

Rows one to three add a measurement. Row four adds a refusal — the verifier does not observe the program, it declines to load one that falls outside the domain — and that is the first mechanism in the track that works by prevention rather than by detection.

11. RTL 5 — The Program Verifier

// ---------------------------------------------------------------------
// program_verifier -- the gate that closes Section 10's open
// quantification.
//
// It does not prove the program correct. It proves the program is
// INSIDE THE DOMAIN the device's properties were written over: bounded
// loops, a bounded instruction count, and memory accesses confined to
// the program's own region.
// ---------------------------------------------------------------------
module program_verifier
  import smartnic_pkg::*;
#(
  parameter int MAX_INSTR   = 645,
  parameter int MAX_LOOPS   = 0        // unbounded loops forbidden
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        verify_req,
  input  logic [15:0] instr_count,
  input  logic [15:0] backward_branches,
  input  logic [15:0] unbounded_loops,
  input  logic [15:0] max_memory_offset,
  input  logic [15:0] program_region_size,
  input  logic        signature_valid,
  input  logic [15:0] worst_case_path,

  output logic        verdict_ok,
  output verification_level_e level,
  output logic        fails_termination,
  output logic        fails_budget,
  output logic        fails_memory,
  output logic        fails_signature,
  output logic [31:0] c_verified,
  output logic [31:0] c_rejected,
  output logic        domain_is_closed
);
  always_comb begin
    // 1. Termination: no unbounded loops. Decidable because the
    //    language forbids them, not because the general problem is.
    fails_termination = (unbounded_loops > 16'(MAX_LOOPS));

    // 2. Budget: the worst-case path fits the per-packet allowance.
    fails_budget = (worst_case_path > 16'(MAX_INSTR));

    // 3. Memory safety: every access is inside the program's region.
    fails_memory = (max_memory_offset >= program_region_size);

    // 4. Provenance.
    fails_signature = !signature_valid;

    verdict_ok = verify_req && !fails_termination && !fails_budget
               && !fails_memory && !fails_signature;

    if (!verify_req)           level = VER_NONE;
    else if (fails_signature)  level = VER_NONE;
    else if (fails_termination)level = VER_SIGNATURE;
    else if (fails_budget)     level = VER_TERMINATION;
    else if (fails_memory)     level = VER_BUDGET;
    else                       level = VER_FULL;

    // The claim the whole mechanism exists to support.
    domain_is_closed = (level == VER_FULL);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_verified <= '0; c_rejected <= '0;
    end else if (verify_req) begin
      if (verdict_ok) c_verified <= c_verified + 32'd1;
      else            c_rejected <= c_rejected + 32'd1;
    end
  end
endmodule

Classification: four checks, of which three are decidable only because the language was restricted.

What it teaches: that fails_termination is answerable at all only because MAX_LOOPS is zero. The halting problem is undecidable for a general language and trivially decidable for one with no backward branches — or with only counted loops whose bounds are literals. The verifier does not solve a hard problem; the language designer removed it, and that removal is the reason a SmartNIC's programming model looks restrictive.

And it teaches that level is a ladder whose rungs fail in a useful order. A program that fails the signature never gets examined; one that passes provenance and fails termination is a bug in a trusted program; one that terminates and exceeds the budget is a performance statement rather than a safety one. The ladder tells the operator which kind of problem they have, which a single Boolean does not.

Deliberately simplified: worst_case_path is an input the verifier consumes rather than computes — the actual analysis is a longest-path walk over the program's control-flow graph, which is where the work is. fails_memory compares one maximum offset against one region size, modelling a program with a single flat region; real programs touch packet data, per-flow state and shared tables, each with its own bounds. MAX_INSTR is a constant where the real budget is the loaded set's, from Section 9. And nothing here verifies interaction between programs, which Section 9's production note showed is the case that matters.

Production implication: the offline-versus-online split is the practical decision, and getting it wrong makes the verifier either useless or unaffordable. A longest-path analysis over a control-flow graph is polynomial and cheap on a host and expensive in a device that must also forward at 148.81 Mpps. The workable arrangement is to do the analysis offline, emit the verdict and the worst-case path length as signed metadata, and have the device check only the signature and the arithmetic — which is what program_verifier above actually does. That reduces the device's job to a signature check and three comparisons, and it moves the trust to whoever signs. The alternative — a full in-device verifier — has been built, and it costs more area than the array it protects.

12. What a Verifier Can and Cannot Establish

Section 11's four checks close the domain. This section says exactly which claims they support and which they do not, because the distinction is where trust is usually misplaced.

What the verifier establishes.

What it does not establish, and cannot.

Row five deserves stating plainly because the four checks are often described as making a device safe. A program that drops every packet from one tenant, or mirrors traffic to an address of its choosing, or rewrites a header to bypass a policy is terminating, in budget and memory-safe. The verifier admits it, correctly, because those are behaviours rather than violations — and distinguishing them requires knowing what the device is supposed to do, which the verifier does not.

The verifier establishes that the program is inside the domain the device's properties were written over. It establishes nothing about whether the program should be running.

Which makes the trust model explicit and is worth writing down.

Row three is the correct arrangement and it is frequently misunderstood. The device is not deciding whether the program is a good idea; it is enforcing that the program cannot break the device. The question of whether the program should run is answered by the signature, which means the whole trust argument reduces to key management — a completely different discipline from anything in this track, and the one that actually secures the arrangement.

And the load-time checks have a cost that is worth naming.

The device's share is a signature check and three comparisons, which is why Section 11's block is small. Everything expensive happens offline and arrives as signed metadata, and the device's job is to refuse anything whose metadata does not check out.

13. RTL 6 — Per-Packet Determinism, and Why It Is Gone

// ---------------------------------------------------------------------
// determinism_monitor -- a fixed-function pipeline has constant
// latency. A programmable one has latency that depends on the packet.
//
// Chapter 23.3 Section 17 established that a switch's pipeline is
// fixed-latency and its buffer is not. A SmartNIC's PIPELINE is not
// fixed-latency either, and the variability is a function of packet
// CONTENT rather than of load.
// ---------------------------------------------------------------------
module determinism_monitor
  import smartnic_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        pkt_done,
  input  logic [15:0] instructions_taken,
  input  logic [15:0] budget,
  input  logic [15:0] pps_million,

  output logic [15:0] min_instructions,
  output logic [15:0] max_instructions,
  output logic [31:0] mean_instructions_x100,
  output logic [15:0] spread_ratio_x10,
  output logic [15:0] sustained_at_max_mpps,
  output logic [15:0] sustained_at_max_pct,
  output logic        content_dependent,
  output logic        adversary_can_halve,
  output logic [31:0] c_packets,
  output logic [31:0] c_over_budget
);
  logic [31:0] total_instructions;

  always_comb begin
    spread_ratio_x10 = (min_instructions == 0) ? 16'hFFFF
                     : (max_instructions * 16'd10) / min_instructions;

    // The throughput the array sustains on the WORST path, which is the
    // only figure a deadline or an adversary cares about.
    sustained_at_max_mpps = (max_instructions == 0) ? 16'hFFFF
                          : 16'((32'(CORES) * CORE_MHZ * 32'(IPC))
                                / 32'(max_instructions));
    sustained_at_max_pct = (pps_million == 0) ? 16'd0
                         : (sustained_at_max_mpps * 16'd100) / pps_million;

    // Always true for a programmable datapath, and it is the point.
    content_dependent = 1'b1;

    // If the worst path is more than twice the budget, a sender who can
    // steer packets onto it halves the part's throughput.
    adversary_can_halve = (max_instructions > (budget * 16'd2));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      min_instructions <= 16'hFFFF; max_instructions <= '0;
      total_instructions <= '0; c_packets <= '0; c_over_budget <= '0;
      mean_instructions_x100 <= '0;
    end else if (pkt_done) begin
      if (instructions_taken < min_instructions)
        min_instructions <= instructions_taken;
      if (instructions_taken > max_instructions)
        max_instructions <= instructions_taken;
      total_instructions <= total_instructions + 32'(instructions_taken);
      c_packets <= c_packets + 32'd1;
      if (instructions_taken > budget)
        c_over_budget <= c_over_budget + 32'd1;
      if (c_packets != 0)
        mean_instructions_x100 <= (total_instructions * 100)
                                  / (c_packets + 32'd1);
    end
  end
endmodule

Classification: a distribution monitor whose most important output is the maximum, not the mean.

What it teaches: that sustained_at_max_pct is the only throughput figure a programmable datapath can honestly quote. A program with a mean of 400 instructions and a worst case of 1 200 sustains 240 Mpps at the mean and 80 at the worst — 53.8% of line rate — and the traffic that triggers the worst path is decided by packet content. Every benchmark measures the mean; every deadline and every adversary cares about the maximum.

And it teaches that adversary_can_halve is a security property expressed as arithmetic. If the worst path is more than twice the budget, a sender who can construct packets that take it halves the part's throughput — without malformed frames, without a protocol violation, and without anything a firewall would notice. That is a denial of service performed entirely with valid traffic, and its magnitude is budget ÷ worst_case.

Deliberately simplified: min_instructions and max_instructions are running extrema with no decay, so a single outlier fixes the maximum for the device's life — a real monitor needs a windowed or percentile-based measure. mean_instructions_x100 divides by c_packets + 1 to avoid a divide-by-zero, which biases it. There is no per-program breakdown, so a device running eight programs reports one distribution. And content_dependent is a literal, which is honest: it is a claim about the architecture rather than a measurement.

Production implication: the missing per-program breakdown is what makes the adversary case hard to attribute, and separating it is cheap. A device running eight programs and showing a 1 200-instruction maximum does not say which program produced it, so an operator cannot tell whether the long path is a rarely-taken branch in a well-behaved program or a hostile input to a badly-written one. Per-program extrema are eight sets of two 16-bit registers — 256 flops, 5 120 BCE, 0.02 of a MAC receive datapath — and they turn the device occasionally takes 1 200 instructions into program 5 has a 1 200-instruction path and it is being taken 0.3% of the time. The second is actionable and the first is not.

14. What a SmartNIC Must Never Do

Five prohibitions, each derived earlier.

One — never size the array from a program's mean instruction count.

The traffic that triggers the worst path is chosen by packet content, so the mean describes a benchmark and the maximum describes a deployment.

Two — never put a payload transformation in a program.

Section 4: the budget is per packet and a payload cost is per octet. AES-GCM over 1 500 octets at two octets per instruction is 750 instructions — more than the entire 64-core budget for one packet. Anything that touches every byte must be fixed function, whatever the area comparison says.

Three — never load a program without closing the domain.

Section 10: a proof written before a load ranges over the programs that existed then. The gate is Section 11's verifier — signature, termination, budget, memory bounds — and the device's share of it is one public-key operation and three comparisons. Everything expensive runs offline and arrives as signed metadata.

Four — never treat a verifier's pass as a statement about behaviour.

A program that drops one tenant's traffic is terminating, in budget and memory-safe. The whole behavioural trust reduces to key management, which is a different discipline and the one that actually secures the arrangement.

Five — never unload a program while a packet is executing it.

Section 9's production note. A packet mid-program in a slot being overwritten runs a mixture of two programs — neither of which was verified. The remedy is Chapter 23.3 §7's: clear a valid bit first so no new packet enters, then drain. The drain is bounded by the worst-case path — 1 200 instructions is 800 ns at 1.5 GHz — so it costs under a microsecond.

15. RTL 7 — SmartNIC Telemetry

// ---------------------------------------------------------------------
// smartnic_telemetry -- what a programmable part knows about itself,
// plus the one field no fixed-function part needs: how many times its
// behaviour has changed.
// ---------------------------------------------------------------------
module smartnic_telemetry
  import smartnic_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        snapshot,

  input  logic [31:0] i_packets,
  input  logic [31:0] i_rejected_by_array,
  input  logic [15:0] i_min_instructions,
  input  logic [15:0] i_max_instructions,
  input  logic [31:0] i_mean_instructions_x100,
  input  logic [31:0] i_over_budget,
  input  logic [15:0] i_utilisation_pct,
  input  logic [31:0] i_loads,
  input  logic [31:0] i_rejected_loads,
  input  logic [31:0] i_loads_since_verification,
  input  logic [2:0]  i_slots_used,
  input  logic        i_unverified_resident,
  input  logic [15:0] i_total_worst_case,

  output logic [31:0] o_packets,
  output logic [15:0] o_min_instructions,
  output logic [15:0] o_max_instructions,
  output logic [31:0] o_mean_instructions_x100,
  output logic [15:0] o_spread_ratio_x10,
  output logic [15:0] o_over_budget_ppm,
  output logic [15:0] o_rejected_ppm,
  output logic [15:0] o_utilisation_pct,
  output logic [31:0] o_loads_since_verification,
  output logic [15:0] o_budget_used_pct,
  output logic [2:0]  o_caveats,
  output logic        o_behaviour_is_verified
);
  localparam int C_UNVERIFIED  = 0;
  localparam int C_OVER_BUDGET = 1;
  localparam int C_SPREAD      = 2;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      o_packets <= '0; o_min_instructions <= 16'hFFFF;
      o_max_instructions <= '0; o_mean_instructions_x100 <= '0;
      o_spread_ratio_x10 <= 16'd10; o_over_budget_ppm <= '0;
      o_rejected_ppm <= '0; o_utilisation_pct <= '0;
      o_loads_since_verification <= '0; o_budget_used_pct <= '0;
      o_caveats <= '0;
    end else if (snapshot) begin
      o_packets                  <= i_packets;
      o_min_instructions         <= i_min_instructions;
      o_max_instructions         <= i_max_instructions;
      o_mean_instructions_x100   <= i_mean_instructions_x100;
      o_utilisation_pct          <= i_utilisation_pct;
      o_loads_since_verification <= i_loads_since_verification;

      if (i_min_instructions != 0)
        o_spread_ratio_x10 <= (i_max_instructions * 16'd10)
                              / i_min_instructions;
      if (i_packets != 0) begin
        o_over_budget_ppm <= 16'((i_over_budget * 1_000_000) / i_packets);
        o_rejected_ppm    <= 16'((i_rejected_by_array * 1_000_000)
                                 / i_packets);
      end

      o_budget_used_pct <= 16'((32'(i_total_worst_case) * 100)
                               / 32'(instr_per_packet()));

      o_caveats[C_UNVERIFIED]  <= i_unverified_resident;
      o_caveats[C_OVER_BUDGET] <= (i_over_budget != 32'd0);
      // A spread above 3x means the worst case is far from the mean,
      // which is Section 13's adversary case.
      o_caveats[C_SPREAD]      <= (o_spread_ratio_x10 > 16'd30);
    end
  end

  // The claim a compliance argument needs, and no fixed-function part
  // ever had to make.
  assign o_behaviour_is_verified = !o_caveats[C_UNVERIFIED];
endmodule

Classification: a snapshot bank with one field that exists only because the part is programmable.

What it teaches: that o_loads_since_verification has no analogue in any earlier chapter. A MAC, a PHY, a switch or a fixed-function NIC has one behaviour, verified once. A SmartNIC has had as many behaviours as it has had loads, and a device that reports forty since anything was proved about it is making a statement about the standing of its own verification. It is a counter, it costs 32 flops, and it is the only honest summary of the situation.

And it teaches that o_spread_ratio_x10 is the field that surfaces Section 13's adversary case. A spread of 3× or more between the minimum and maximum instruction counts means the worst path is far from the typical one, so a sender who can steer packets onto it has a lever. The ratio costs one division and turns an architectural property into an observation.

Deliberately simplified: no read-clear, and at 148.81 Mpps a 32-bit packet counter wraps in 28.9 seconds — Chapter 23.4 §15's problem, unchanged. o_min_instructions and o_max_instructions are lifetime extrema with the decay problem Section 13 named. o_budget_used_pct sums worst cases across all resident programs, which over-counts when only one runs per packet. And there is no per-program breakdown, which Section 13's production note argued for.

Production implication: o_loads_since_verification is the field to expose to a compliance process rather than to an operator, and the distinction matters. An operator wants to know whether the device is working; a compliance argument wants to know whether the thing that was certified is the thing that is running. For a part whose behaviour is a program, those are different questions, and the second is answered by a program-set hash rather than a load count — a digest over the identifiers of every resident program, which changes on every load and unload. Thirty-two bits, updated on two events, and it lets an auditor ask "is this the configuration that was approved" and get an answer.

16. RTL 8 — The SmartNIC Conformance Monitor

// ---------------------------------------------------------------------
// smartnic_conformance_monitor -- properties for a programmable NIC.
//
// Every property here is about the SILICON, because the silicon is the
// only part whose behaviour was fixed at tape-out. Properties 11 and 12
// are the two that constrain what the silicon does with a program, and
// they are the whole of what can be asserted about behaviour.
// ---------------------------------------------------------------------
module smartnic_conformance_monitor
  import smartnic_pkg::*;
(
  input logic        clk,
  input logic        rst_n,

  input logic [31:0] budget_per_packet,
  input logic [15:0] cores_busy,
  input logic        accepted,
  input logic        array_saturated,
  input logic        pkt_arrives,
  input logic [15:0] instructions_taken,
  input logic [15:0] program_worst_case,
  input logic        load_req,
  input logic        load_accepted,
  input logic        load_signature_ok,
  input logic        load_verifier_ok,
  input logic        budget_exceeded,
  input logic        verdict_ok,
  input logic        fails_termination,
  input logic        fails_budget,
  input logic        fails_memory,
  input logic        domain_is_closed,
  input logic        unverified_resident,
  input logic        behaviour_is_verified,
  input logic        claim_conformance
);
  // 1. A packet is accepted only if a core is free.
  p_sn_accept: assert property (@(posedge clk) disable iff (!rst_n)
    accepted |-> (cores_busy < 16'(CORES)));

  // 2. Saturation and acceptance are exclusive.
  p_sn_exclusive: assert property (@(posedge clk) disable iff (!rst_n)
    !(accepted && array_saturated));

  // 3. Every arrival is either accepted or counted as rejected.
  p_sn_accounted: assert property (@(posedge clk) disable iff (!rst_n)
    pkt_arrives |-> (accepted || array_saturated));

  // 4. A packet never executes more than its program's worst case.
  p_sn_worst_case: assert property (@(posedge clk) disable iff (!rst_n)
    instructions_taken <= program_worst_case);

  // 5. A load requires a valid signature.
  p_sn_load_sig: assert property (@(posedge clk) disable iff (!rst_n)
    load_accepted |-> load_signature_ok);

  // 6. And a verifier pass.
  p_sn_load_ver: assert property (@(posedge clk) disable iff (!rst_n)
    load_accepted |-> load_verifier_ok);

  // 7. And budget headroom over the loaded SET.
  p_sn_load_budget: assert property (@(posedge clk) disable iff (!rst_n)
    load_accepted |-> !budget_exceeded);

  // 8. The verifier's verdict is the conjunction of its four checks.
  p_sn_verdict: assert property (@(posedge clk) disable iff (!rst_n)
    verdict_ok == (!fails_termination && !fails_budget && !fails_memory));

  // 9. A closed domain requires a full verification level.
  p_sn_domain: assert property (@(posedge clk) disable iff (!rst_n)
    domain_is_closed |-> verdict_ok);

  // 10. An unverified resident program clears the verified flag.
  p_sn_unverified: assert property (@(posedge clk) disable iff (!rst_n)
    unverified_resident |-> !behaviour_is_verified);

  // 11. A CONFORMANCE CLAIM requires every resident program to be
  //     inside the domain. This is the property Section 20 is about.
  p_sn_claim_domain: assert property (@(posedge clk) disable iff (!rst_n)
    claim_conformance |-> behaviour_is_verified);

  // 12. And the silicon's own properties to hold, which they do
  //     regardless of the program.
  p_sn_silicon_holds: assert property (@(posedge clk) disable iff (!rst_n)
    claim_conformance |-> (accepted || array_saturated || !pkt_arrives));
endmodule

Classification: twelve properties about silicon, and two of them are the only statements about behaviour that exist.

What it teaches: that property 4 is the one that depends on something outside the silicon. instructions_taken <= program_worst_case is checkable at run time only because the worst case arrived as signed metadata — the silicon does not compute it. Every other property here is a statement about gates, and this one imports a number from a verifier that ran offline.

And it teaches that property 11 is the whole behavioural guarantee. It says a conformance claim requires every resident program to be inside the domain — not that they are correct, not that they are safe, but that they are the kind of program the device's other eleven properties were written over. That is a weaker claim than any earlier chapter's conformance monitor makes, and it is the strongest one available.

Deliberately simplified: property 4 compares against the program's worst case rather than the array's budget, so a program whose metadata lies is not caught. Property 8 omits the signature from the conjunction, matching Section 11's ladder where a signature failure short-circuits. Property 12 is nearly vacuous — it restates property 3 — and is kept to make explicit that the silicon's properties are unconditional. And no property here says anything about what a program computes, which is Section 12's point stated as an absence.

Production implication: property 4's dependence on signed metadata is the seam where the whole arrangement can be attacked, and it is worth hardening. If a program's declared worst case is smaller than its real one, the loader admits it, the budget arithmetic is wrong and the array saturates — and property 4 fires, which is the correct behaviour and happens after the damage. A run-time instruction counter per packet with a hard cap — kill the packet at the budget, count it, and raise a caveat — turns a lie in the metadata into a bounded, counted event rather than a throughput collapse. It costs a comparator and a counter per core: 64 × 32 bits = 2 048 flops, 40 960 BCE, 0.14 of a MAC receive datapath.

17. The Three Architectures, Compared

Fixed function, programmable datapath, host software — the same work, three places, and the comparison is now in one unit.

Row eight is the one that is usually left out. A fixed-function block's throughput does not depend on packet content; a programmable array's does, and a sender who can steer packets onto the long path halves it. Host software is worse still, because it adds scheduling and cache behaviour to the same effect.

And the decision rule that falls out.

Row two is the one that decides most cases and it is the one an enthusiasm for programmability tends to skip. A programmable array costs 197 times the fixed-function blocks it replaces; for a function that is not going to change, that is 197× of area purchased for an option nobody will exercise.

The three architectures' place in the track.

A SmartNIC is Chapter 23.4's NIC, 44% larger, with the option to change its mind. Everything in this chapter is the price and the conditions of that option.

18. What the SmartNIC Assumes

Seven premises, and three of them are about a program that does not exist yet.

Rows one to three are all about a program, and none of them can be checked by the silicon alone. Row one and row three are checked by signed metadata; row two is checked by a run-time counter with a hard cap, which Section 16's production note argued for at 0.14 datapaths.

Row five is the assumption that carries the most weight and receives the least attention in a hardware discussion. Section 12: the verifier establishes that a program is in the domain and nothing about whether it should run. A program that is terminating, in budget and memory-safe can still drop one tenant's traffic or mirror it somewhere — so the whole behavioural guarantee is that somebody trustworthy signed it, and the security of the arrangement is key management rather than anything in this chapter.

And one premise that is stated in every product brief and is false in an interesting way.

That programmability makes the part future-proof. It makes the part's function changeable; it does not change the instruction budget, which is fixed at tape-out by the core count and the clock. A part with 645 instructions per packet can be given a different program and cannot be given a bigger budget — so a future requirement that needs 1 500 instructions per packet is as unreachable on a SmartNIC as on a fixed-function part, and the flexibility that was bought does not extend in the direction the requirement grew.

19. The Cost, Accounted — in BCE

Chapter 23.3 §2's unit, applied to this chapter's blocks and to the array they manage.

The control logic that makes a programmable array safe is 0.15 of a MAC receive datapath — the loader, the verifier, the determinism monitor and the telemetry together — against an array of 78.6. The ratio is 535 : 1, and it is the same shape as every instrumentation argument in Modules 21 to 23: the mechanism that makes a structure trustworthy is a rounding error against the structure.

And the additions Sections 13 and 16 argued for.

Two tenths of one per cent of the array, and between them they supply which program takes the long path, a hard cap when the metadata lied, and a digest an auditor can compare against an approved configuration.

The chapter's totals, set against the rest of Module 23.

Row three against row two is the number to keep. A 64-core programmable array is ninety-four times the forwarding logic of a 6.4 Tb/s switch — not because the array is enormous, but because a switch's pipeline is remarkably small, which Chapter 23.3 §19 established and this table confirms from the other side.

20. Properties Worth Asserting, and One Worth Refusing

Six groups. Every property here is about the silicon, because the silicon is the only thing whose behaviour was fixed when the properties were written.

Group A — the budget.

// A1. The budget is the array's throughput over the packet rate.
p_bd_divide: assert property (@(posedge clk) disable iff (!rst_n)
  (pps_million != 0) |->
    (budget_per_packet == ((cores * core_mhz * ipc) / pps_million)));

// A2. Sustained throughput at the worst case is the array over it.
p_bd_worst: assert property (@(posedge clk) disable iff (!rst_n)
  (program_worst_instr != 0) |->
    (sustained_mpps_worst ==
      ((cores * core_mhz * ipc) / program_worst_instr)));

// A3. Fitting at the worst case implies fitting at the mean.
p_bd_implies: assert property (@(posedge clk) disable iff (!rst_n)
  fits_at_worst |-> fits_at_mean);

// A4. The host-core equivalence is array MIPS over host MIPS.
p_bd_host: assert property (@(posedge clk) disable iff (!rst_n)
  host_cores_equivalent ==
    ((cores * core_mhz * ipc) / (HOST_MHZ * HOST_IPC)));

// A5. Cores needed scales linearly with the worst case.
p_bd_linear: assert property (@(posedge clk) disable iff (!rst_n)
  cores_needed_worst ==
    ((program_worst_instr * pps_million) / (core_mhz * ipc)));

Group B — the array.

// B1. Acceptance requires a free core.
p_ar_free: assert property (@(posedge clk) disable iff (!rst_n)
  accepted |-> (cores_busy < 16'(CORES)));

// B2. Acceptance and saturation are exclusive.
p_ar_exclusive: assert property (@(posedge clk) disable iff (!rst_n)
  !(accepted && array_saturated));

// B3. Every arrival is accounted.
p_ar_accounted: assert property (@(posedge clk) disable iff (!rst_n)
  pkt_arrives |-> (accepted || array_saturated));

// B4. A run-to-completion assignment holds the core for the program.
p_ar_holds: assert property (@(posedge clk) disable iff (!rst_n)
  (accepted && run_to_completion) |=>
    (core_remaining[$past(assigned_core)] == $past(pkt_instructions) - 1));

// B5. Utilisation is busy cores over total.
p_ar_util: assert property (@(posedge clk) disable iff (!rst_n)
  utilisation_pct == ((cores_busy * 100) / CORES));

// B6. Core occupancy never exceeds the longest program.
p_ar_occupancy: assert property (@(posedge clk) disable iff (!rst_n)
  longest_occupancy <= program_worst_case);

Group C — the loader.

// C1. A load requires a signature.
p_ld_sig: assert property (@(posedge clk) disable iff (!rst_n)
  load_accepted |-> load_signature_ok);

// C2. And a verifier pass.
p_ld_ver: assert property (@(posedge clk) disable iff (!rst_n)
  load_accepted |-> load_verifier_ok);

// C3. And budget headroom over the loaded set.
p_ld_budget: assert property (@(posedge clk) disable iff (!rst_n)
  load_accepted |-> !budget_exceeded);

// C4. And a free slot.
p_ld_slot: assert property (@(posedge clk) disable iff (!rst_n)
  load_accepted |-> (slots_used < 3'(SLOTS)));

// C5. The load counter advances on every accepted load.
p_ld_count: assert property (@(posedge clk) disable iff (!rst_n)
  load_accepted |=> (c_loads_since_verification ==
                     $past(c_loads_since_verification) + 1));

// C6. An unload frees exactly one slot.
p_ld_unload: assert property (@(posedge clk) disable iff (!rst_n)
  unload_req |=> (slots_used == $past(slots_used) - 1));

Group D — the verifier.

// D1. The verdict is the conjunction of the three analyses.
p_vf_verdict: assert property (@(posedge clk) disable iff (!rst_n)
  verdict_ok == (!fails_termination && !fails_budget && !fails_memory
                 && !fails_signature));

// D2. An unbounded loop fails termination.
p_vf_loops: assert property (@(posedge clk) disable iff (!rst_n)
  (unbounded_loops > MAX_LOOPS) |-> fails_termination);

// D3. A worst-case path over the budget fails the budget check.
p_vf_budget: assert property (@(posedge clk) disable iff (!rst_n)
  (worst_case_path > MAX_INSTR) |-> fails_budget);

// D4. An out-of-region offset fails memory safety.
p_vf_memory: assert property (@(posedge clk) disable iff (!rst_n)
  (max_memory_offset >= program_region_size) |-> fails_memory);

// D5. A closed domain requires a full pass.
p_vf_closed: assert property (@(posedge clk) disable iff (!rst_n)
  domain_is_closed |-> verdict_ok);

// D6. Verified plus rejected equals verification requests.
p_vf_account: assert property (@(posedge clk) disable iff (!rst_n)
  verify_req |=> ((c_verified + c_rejected) ==
                  ($past(c_verified) + $past(c_rejected) + 1)));

Group E — determinism.

// E1. A packet never exceeds its program's declared worst case.
p_dt_worst: assert property (@(posedge clk) disable iff (!rst_n)
  pkt_done |-> (instructions_taken <= program_worst_case));

// E2. The maximum is monotone.
p_dt_max: assert property (@(posedge clk) disable iff (!rst_n)
  max_instructions >= $past(max_instructions));

// E3. The minimum never exceeds the maximum.
p_dt_order: assert property (@(posedge clk) disable iff (!rst_n)
  min_instructions <= max_instructions);

// E4. The part is content-dependent and says so.
p_dt_declares: assert property (@(posedge clk) disable iff (!rst_n)
  content_dependent);

// E5. Over-budget packets are counted, not silently truncated.
p_dt_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (pkt_done && (instructions_taken > budget)) |=>
    (c_over_budget == $past(c_over_budget) + 1));

// E6. The adversary flag is the arithmetic and nothing more.
p_dt_adversary: assert property (@(posedge clk) disable iff (!rst_n)
  adversary_can_halve == (max_instructions > (budget * 16'd2)));

Group F — the claim.

// F1. A conformance claim requires every resident program verified.
p_cf_domain: assert property (@(posedge clk) disable iff (!rst_n)
  claim_conformance |-> behaviour_is_verified);

// F2. An unverified resident clears the flag.
p_cf_unverified: assert property (@(posedge clk) disable iff (!rst_n)
  unverified_resident |-> !behaviour_is_verified);

// F3. A throughput claim names a worst case, not a mean.
p_cf_throughput: assert property (@(posedge clk) disable iff (!rst_n)
  claim_line_rate |-> fits_at_worst);

// F4. The load count since verification is exposed.
p_cf_exposed: assert property (@(posedge clk) disable iff (!rst_n)
  snapshot |=> (o_loads_since_verification ==
                $past(i_loads_since_verification)));

// F5. The silicon's properties hold regardless of the program.
p_cf_silicon: assert property (@(posedge clk) disable iff (!rst_n)
  pkt_arrives |-> (accepted || array_saturated));

Thirty-four properties. Every one is about the silicon, and the silicon is the same after a program load as before it.

21. Verification Scenarios

Fifty-eight scenarios. Group 4's cannot be run before the programs exist, which is the chapter's problem stated as a test plan.

Group 1 — the instruction budget (10).

Group 2 — what fits (8).

Group 3 — the array (10).