Protocols fail in long, rare sequences that directed tests miss: a pulse pair three cycles apart after a reset, data moved mid-handshake, a flag sampled one cycle early. Assertions watch every cycle, so they catch the rare case the testbench author never thought to write. Signoff expects one assertion per protocol rule, bound in the design, plus a runnable equivalent where the simulator cannot execute the assertion form.
The SVA form below states the toggle spacing rule directly. It needs a simulator with full assertion support, so it is marked accordingly, and the runnable checker after it implements the same rule in plain SystemVerilog:
// not-run: needs an SVA-capable simulator; kept as the binding specification.
// property p_toggle_spacing;
// @(posedge clk_s) $rose(toggle_s) |-> ##[8:$] ($rose(toggle_s) or $fell(toggle_s));
// endproperty
// a_toggle_spacing: assert property (p_toggle_spacing)
// else $error("toggle re-flipped inside the minimum gap");`timescale 1ns/1ps
// Runnable spacing checker: flags any two toggle flips closer than
// MIN_GAP source cycles. Plain SystemVerilog, runs under Icarus.
module spacing_checker #(parameter int MIN_GAP = 8) (
input logic clk_s, rst_s_n, input logic toggle_s, output int errors
);
logic prev;
int gap;
always @(posedge clk_s or negedge rst_s_n)
if (!rst_s_n) begin prev <= 1'b0; gap <= MIN_GAP; errors <= 0; end
else begin
if (toggle_s !== prev) begin
if (gap < MIN_GAP) errors <= errors + 1;
gap <= 0; prev <= toggle_s;
end else if (gap < MIN_GAP) gap <= gap + 1;
end
endmodule
module tb_spacing;
logic clk_s = 0, rst_s_n = 0, tog = 0;
int errors;
spacing_checker #(8) chk (.clk_s, .rst_s_n, .toggle_s(tog), .errors);
always #5 clk_s = ~clk_s;
initial begin
repeat (3) @(posedge clk_s); rst_s_n = 1;
repeat (20) @(posedge clk_s);
@(negedge clk_s); tog = ~tog; // legal flip after a long gap
repeat (3) @(posedge clk_s);
@(negedge clk_s); tog = ~tog; // illegal: only 3 cycles later
repeat (12) @(posedge clk_s);
if (errors == 1) $display("PASS: spacing checker flagged exactly the short gap");
else $display("FAIL: errors=%0d, want 1", errors);
$finish;
end
endmoduleThe handshake rule that breaks most often is data stability while req is high. The runnable checker below captures the bus at the req rise and flags any movement before req falls; stimulus moves the bus mid-transfer on purpose:
`timescale 1ns/1ps
// Runnable handshake checker: data must not move while req is high.
module hs_checker (
input logic clk_s, rst_s_n,
input logic req, input logic [7:0] data, output int errors
);
logic [7:0] held;
logic was_req;
always @(posedge clk_s or negedge rst_s_n)
if (!rst_s_n) begin held <= '0; was_req <= 1'b0; errors <= 0; end
else begin
if (req && !was_req) held <= data; // capture at the req rise
else if (req && data !== held) errors <= errors + 1;
was_req <= req;
end
endmodule
module tb_hs_check;
logic clk_s = 0, rst_s_n = 0, req = 0;
logic [7:0] data = 0;
int errors;
hs_checker chk (.clk_s, .rst_s_n, .req, .data, .errors);
always #5 clk_s = ~clk_s;
initial begin
repeat (2) @(posedge clk_s); rst_s_n = 1;
@(negedge clk_s); data = 8'hA5;
@(negedge clk_s); req = 1; // legal transfer starts
repeat (4) @(posedge clk_s);
@(negedge clk_s); data = 8'h3C; // illegal mid-transfer move
repeat (2) @(posedge clk_s);
@(negedge clk_s); req = 0;
repeat (2) @(posedge clk_s);
if (errors >= 1) $display("PASS: checker saw data move while req was high (%0d hits)", errors);
else $display("FAIL: checker missed the mid-transfer data change");
$finish;
end
endmoduleThe FIFO flag rule is directional: the write-side occupancy estimate must never fall below the true fill, because the synchronised read pointer only ever lags. The runnable check below models a two-cycle-stale read pointer (non-blocking flops, so the lag is real) against live writes and reads, and adds a deliberately leading estimate to prove the checker can fire:
`timescale 1ns/1ps
// Runnable check of the conservative-flag argument. A real two-flop lag in the
// read pointer must never make the write-side fill estimate undercut the true
// fill. A second, deliberately LEADING estimate proves the checker can fire.
module tb_flag_safe;
logic clk = 0;
always #5 clk = ~clk;
int wptr = 0, rptr = 0, rptr_q = 0, rptr_sync = 0;
int errors = 0, bad_errors = 0;
initial begin
repeat (200) begin
@(posedge clk);
if ($urandom_range(0, 9) < 6) wptr = wptr + 1;
if ($urandom_range(0, 9) < 5) rptr = rptr + 1;
rptr_q <= rptr; // synchroniser stage 1 (a real lag)
rptr_sync <= rptr_q; // synchroniser stage 2
#1; // let the non-blocking updates land
if (wptr - rptr_sync < wptr - rptr) errors++; // lagging estimate below truth? must never fire
if (wptr - (rptr + 1) < wptr - rptr) bad_errors++; // leading estimate: must fire
end
if (errors == 0 && bad_errors > 0)
$display("PASS: lagging estimate stayed conservative for 200 cycles; the leading estimate was caught %0d times", bad_errors);
else $display("FAIL: lagging errors=%0d, leading errors=%0d", errors, bad_errors);
$finish;
end
endmoduleUnknown: the test never challenges it. Shorten one gap deliberately (as the testbench above does) and confirm exactly one error before trusting the zero.