SPI · Module 17
Mode-Aware Checking and Assertion Pitfalls
One obligation written five ways. On legal traffic all five report zero, which is why four of them survive review. A checker clocked on SCLK is unfalsifiable rather than merely under-exercised, and a disable-iff that overlaps its antecedent reports nothing on any stimulus.
Chapter 17.1 wrote seven properties and measured them. This chapter takes one of them — the simplest one in the set — and writes it five ways.
While the slave is deselected, SCLK must sit at CPOL. Three lines of any assertion language, impossible to misunderstand, and at least four ways to write it that do not work.
1. The Five Writings
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
T1 CORRECT sampled on the OBSERVER's clock, guarded by reset,
reported once per offending cycle.
T2 CLOCKED ON SCLK "check the SPI protocol on the SPI clock". Blind for
two independent reasons, and the second one cannot be
fixed by adding stimulus.
T3 NO RESET GUARD the same check without `disable iff (!rst_n)`.
Correct once the design is running; noisy during reset.
T4 DISABLE OVERLAPS `disable iff (cs_n)` -- added by somebody silencing
T3's noise. The disable condition IS the antecedent.
T5 EDGE-REPORTED identical to T1 except that it reports once per
OFFENCE rather than once per offending cycle.CPOL is 1 throughout the measurements, so the offending SCLK level is 0. That detail decides everything about T2.
2. Why A Checker Clocked On SCLK Cannot Fail
Where each checker is evaluated
16 cyclesT2 is blind for two independent reasons, and the second is the one that cannot be fixed by running longer.
First, SCLK stops between transactions, so there is no clock edge during most of the interval this obligation is about.
Second — and this is the part that makes the property unfalsifiable — a block clocked on posedge sclk samples SCLK only at the instants SCLK IS 1. With CPOL = 1 the obligation is SCLK must be 1, so every evaluation point is a compliant one by construction. The property is not under-exercised. It cannot fail.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
a checker clocked on the signal it checks can only ever observe that signal
in one state3. The Measurement
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
variant S1 legal S2 fault, SCLK moving S3 fault, SCLK still
T1 correct 0 4 6
T2 clocked on SCLK 0 0 0
T3 no reset guard 0 4 6
T4 disable iff overlaps 0 0 0
T5 edge-reported 0 2 1
during reset, when the pins mean nothing:
T1 correct (reset-guarded) ..... 0
T3 no reset guard .............. 6
and the EVALUATION counts over S3: T1 evaluated 12 times, T2 evaluated 1Read the first column first. On legal traffic all five report zero. That is not a footnote; it is the reason four defective writings of a three-line obligation survive review indefinitely.
S2 gives T2 clock edges and it still reports nothing. SCLK is parked at the wrong level and toggled inside the window, so the SCLK-clocked checker does get evaluated — and every evaluation lands at a rising edge, where SCLK is 1, where the obligation holds. More clock does not help it.
S3 is the arithmetic of the first blindness. With SCLK still, T2 is evaluated once against T1's twelve — at the compliant edge out of the window.
T4 reports zero on all three stimuli, including both faults. Its disable condition is its antecedent, so there is nothing it could ever report, and in a suite's output it is indistinguishable from T1.
4. T1 Against T5 Is Not A Correctness Question
T1 reports 4 offending cycles where T5 reports 2 offences; with SCLK still, 6 against 1. Both are correct and they answer different questions — how long was the bus wrong and how many times did it go wrong.
It is worth noticing which of the five differences people argue about. This one, usually, while T4 sits in the same file reporting nothing.
5. Building It — Three HDLs
Azvya Education Pvt. Ltd.VLSI Mentor
spi_assert_traps.sv — one obligation written five ways, with an evaluation count per variant
// spi_assert_traps.sv
//
// Chapter 17.2 -- ONE obligation, written FIVE ways, and the same faults shown to all five.
//
// THE OBLIGATION.
//
// while the slave is deselected, SCLK must sit at CPOL
//
// That is Chapter 16.1's rule R1 and Chapter 17.1's property P5. It is about three lines of
// anybody's assertion language, it is impossible to misunderstand, and there are at least four
// ways to write it that do not work. This module implements all five and counts what each one
// reports, because the differences between them are invisible in a review and obvious in a
// measurement.
//
// T1 CORRECT sampled on the OBSERVER's clock, guarded by reset, reported once
// per offending cycle.
//
// T2 CLOCKED ON SCLK the trap that looks like good practice: "check the SPI protocol on
// the SPI clock". It is blind for TWO independent reasons, and the
// second one is worse than the first.
//
// First, SCLK STOPS between transactions, so there is no clock edge
// during most of the interval this obligation is about.
//
// Second -- and this is the one that cannot be fixed by adding
// stimulus -- a block clocked on `posedge sclk` samples SCLK only at
// the instants SCLK IS 1. With CPOL = 1 the obligation is "SCLK must
// be 1", so every evaluation point is a compliant one BY
// CONSTRUCTION. The property is not merely under-exercised; it is
// unfalsifiable. A checker clocked on the signal it checks can only
// ever observe that signal in one state.
//
// T3 NO RESET GUARD the same check without `disable iff (!rst_n)`. Correct once the
// design is running, and it fires throughout reset, when the pins
// mean nothing. Noisy rather than dangerous -- and the usual fix
// for the noise is T4.
//
// T4 DISABLE OVERLAPS `disable iff (cs_n)` -- added by somebody silencing T3's noise, or
// by somebody who reasoned that a deselected bus is not interesting.
// The disable condition is EXACTLY the antecedent, so the property is
// switched off precisely when it applies. It reports zero on every
// stimulus, including the ones designed to break it. This is the
// dangerous one.
//
// T5 EDGE-REPORTED identical to T1 except that it reports once per OFFENCE rather than
// once per offending cycle. Not a correctness difference; a reporting
// difference, and the one people argue about while T4 sits in the same
// file reporting nothing.
//
// THE MEASUREMENT NEEDS THREE STIMULI, and the third is the one that separates T2.
//
// S1 legal traffic
// S2 SCLK parked off CPOL while deselected, WITH SCLK edges in the window
// S3 SCLK parked off CPOL while deselected, with NO SCLK edges in the window
//
// S3 is not a contrived stimulus. It is what a master does after its mode register is
// reprogrammed and before its next transfer: the clock sits at the wrong level and does not
// move. Chapter 16.4 found exactly that fault in its own driver.
`timescale 1ns/1ps
module spi_assert_traps #(
parameter int CNT_W = 16
) (
input wire clk, // the OBSERVER's clock
input wire rst_n,
input wire sclk,
input wire cs_n,
input wire cpol,
input wire clr,
output reg [CNT_W-1:0] t1_correct,
output reg [CNT_W-1:0] t2_sclk_clocked,
output reg [CNT_W-1:0] t3_no_reset_guard,
output reg [CNT_W-1:0] t4_disable_overlaps,
output reg [CNT_W-1:0] t5_edge_reported,
// How many times the obligation's antecedent was EVALUATED by each variant. T2's is the
// number that explains its silence, and it is the number a pass/fail report never shows.
output reg [CNT_W-1:0] t1_evals,
output reg [CNT_W-1:0] t2_evals
);
wire bad = (sclk !== cpol);
// ------------------------------------------------------------------
// T1, T3, T4, T5 -- all sampled on the observer's clock.
// ------------------------------------------------------------------
reg prev_bad_sel; // for T5: was the bus already offending on the previous cycle?
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
t1_correct <= {CNT_W{1'b0}};
t4_disable_overlaps <= {CNT_W{1'b0}};
t5_edge_reported <= {CNT_W{1'b0}};
t1_evals <= {CNT_W{1'b0}};
prev_bad_sel <= 1'b0;
end else begin
if (clr) begin
t1_correct <= {CNT_W{1'b0}};
t4_disable_overlaps <= {CNT_W{1'b0}};
t5_edge_reported <= {CNT_W{1'b0}};
t1_evals <= {CNT_W{1'b0}};
end
// T1 -- the obligation, guarded by reset because this block is not reached
// during reset at all, and reported once per offending cycle.
if (cs_n) begin
t1_evals <= t1_evals + 1'b1;
if (bad) t1_correct <= t1_correct + 1'b1;
end
// T4 -- `disable iff (cs_n)`. The disable condition IS the antecedent, so the
// consequent is never evaluated. Written out procedurally the defect is obvious;
// written as one line of SVA between two correct-looking properties it is not.
if (cs_n && !cs_n) begin
t4_disable_overlaps <= t4_disable_overlaps + 1'b1;
end
// T5 -- the same obligation, reported on the TRANSITION into the offence.
if (cs_n && bad && !prev_bad_sel)
t5_edge_reported <= t5_edge_reported + 1'b1;
prev_bad_sel <= cs_n && bad;
end
end
// T3 -- no reset guard. Deliberately NOT in the reset-sensitive block above, because that
// is the whole point: the check runs while reset is asserted, and the pins mean nothing
// then. The counter still needs an initial value, or the variant is unmeasurable rather
// than merely wrong.
initial t3_no_reset_guard = {CNT_W{1'b0}};
always @(posedge clk) begin
if (clr) t3_no_reset_guard <= {CNT_W{1'b0}};
else if (cs_n && bad) t3_no_reset_guard <= t3_no_reset_guard + 1'b1;
end
// ------------------------------------------------------------------
// T2 -- clocked on SCLK.
//
// This is the whole trap in two lines. The block is correct. Its condition is correct.
// It is sampled on a clock that does not run during the interval the condition is about,
// so it is evaluated a handful of times per transaction and never once while the bus is
// idle -- which is when the obligation applies.
// ------------------------------------------------------------------
always @(posedge sclk or negedge rst_n) begin
if (!rst_n) begin
t2_sclk_clocked <= {CNT_W{1'b0}};
t2_evals <= {CNT_W{1'b0}};
end else begin
// AND NOTE WHERE THIS CLEAR LIVES. `clr` is only acted on inside a block clocked
// on SCLK, so a variant clocked on the protocol's clock cannot even be RESET
// between test phases while that clock is idle. The testbench discovered this by
// measuring a counter that refused to go to zero, and it works in deltas
// afterwards. A checker whose clock the design controls is a checker the bench
// does not fully control either.
if (clr) begin
t2_sclk_clocked <= {CNT_W{1'b0}};
t2_evals <= {CNT_W{1'b0}};
end
if (cs_n) begin
t2_evals <= t2_evals + 1'b1;
if (bad) t2_sclk_clocked <= t2_sclk_clocked + 1'b1;
end
end
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_assert_traps.v — the same design in Verilog-2001
// spi_assert_traps.v
//
// Chapter 17.2 -- ONE obligation, written FIVE ways, and the same faults shown to all five.
//
// THE OBLIGATION.
//
// while the slave is deselected, SCLK must sit at CPOL
//
// That is Chapter 16.1's rule R1 and Chapter 17.1's property P5. It is about three lines of
// anybody's assertion language, it is impossible to misunderstand, and there are at least four
// ways to write it that do not work. This module implements all five and counts what each one
// reports, because the differences between them are invisible in a review and obvious in a
// measurement.
//
// T1 CORRECT sampled on the OBSERVER's clock, guarded by reset, reported once
// per offending cycle.
//
// T2 CLOCKED ON SCLK the trap that looks like good practice: "check the SPI protocol on
// the SPI clock". It is blind for TWO independent reasons, and the
// second one is worse than the first.
//
// First, SCLK STOPS between transactions, so there is no clock edge
// during most of the interval this obligation is about.
//
// Second -- and this is the one that cannot be fixed by adding
// stimulus -- a block clocked on `posedge sclk` samples SCLK only at
// the instants SCLK IS 1. With CPOL = 1 the obligation is "SCLK must
// be 1", so every evaluation point is a compliant one BY
// CONSTRUCTION. The property is not merely under-exercised; it is
// unfalsifiable. A checker clocked on the signal it checks can only
// ever observe that signal in one state.
//
// T3 NO RESET GUARD the same check without `disable iff (!rst_n)`. Correct once the
// design is running, and it fires throughout reset, when the pins
// mean nothing. Noisy rather than dangerous -- and the usual fix
// for the noise is T4.
//
// T4 DISABLE OVERLAPS `disable iff (cs_n)` -- added by somebody silencing T3's noise, or
// by somebody who reasoned that a deselected bus is not interesting.
// The disable condition is EXACTLY the antecedent, so the property is
// switched off precisely when it applies. It reports zero on every
// stimulus, including the ones designed to break it. This is the
// dangerous one.
//
// T5 EDGE-REPORTED identical to T1 except that it reports once per OFFENCE rather than
// once per offending cycle. Not a correctness difference; a reporting
// difference, and the one people argue about while T4 sits in the same
// file reporting nothing.
//
// THE MEASUREMENT NEEDS THREE STIMULI, and the third is the one that separates T2.
//
// S1 legal traffic
// S2 SCLK parked off CPOL while deselected, WITH SCLK edges in the window
// S3 SCLK parked off CPOL while deselected, with NO SCLK edges in the window
//
// S3 is not a contrived stimulus. It is what a master does after its mode register is
// reprogrammed and before its next transfer: the clock sits at the wrong level and does not
// move. Chapter 16.4 found exactly that fault in its own driver.
`timescale 1ns/1ps
module spi_assert_traps #(
parameter CNT_W = 16
) (
input wire clk, // the OBSERVER's clock
input wire rst_n,
input wire sclk,
input wire cs_n,
input wire cpol,
input wire clr,
output reg [CNT_W-1:0] t1_correct,
output reg [CNT_W-1:0] t2_sclk_clocked,
output reg [CNT_W-1:0] t3_no_reset_guard,
output reg [CNT_W-1:0] t4_disable_overlaps,
output reg [CNT_W-1:0] t5_edge_reported,
// How many times the obligation's antecedent was EVALUATED by each variant. T2's is the
// number that explains its silence, and it is the number a pass/fail report never shows.
output reg [CNT_W-1:0] t1_evals,
output reg [CNT_W-1:0] t2_evals
);
wire bad = (sclk !== cpol);
// ------------------------------------------------------------------
// T1, T3, T4, T5 -- all sampled on the observer's clock.
// ------------------------------------------------------------------
reg prev_bad_sel; // for T5: was the bus already offending on the previous cycle?
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
t1_correct <= {CNT_W{1'b0}};
t4_disable_overlaps <= {CNT_W{1'b0}};
t5_edge_reported <= {CNT_W{1'b0}};
t1_evals <= {CNT_W{1'b0}};
prev_bad_sel <= 1'b0;
end else begin
if (clr) begin
t1_correct <= {CNT_W{1'b0}};
t4_disable_overlaps <= {CNT_W{1'b0}};
t5_edge_reported <= {CNT_W{1'b0}};
t1_evals <= {CNT_W{1'b0}};
end
// T1 -- the obligation, guarded by reset because this block is not reached
// during reset at all, and reported once per offending cycle.
if (cs_n) begin
t1_evals <= t1_evals + 1'b1;
if (bad) t1_correct <= t1_correct + 1'b1;
end
// T4 -- `disable iff (cs_n)`. The disable condition IS the antecedent, so the
// consequent is never evaluated. Written out procedurally the defect is obvious;
// written as one line of SVA between two correct-looking properties it is not.
if (cs_n && !cs_n) begin
t4_disable_overlaps <= t4_disable_overlaps + 1'b1;
end
// T5 -- the same obligation, reported on the TRANSITION into the offence.
if (cs_n && bad && !prev_bad_sel)
t5_edge_reported <= t5_edge_reported + 1'b1;
prev_bad_sel <= cs_n && bad;
end
end
// T3 -- no reset guard. Deliberately NOT in the reset-sensitive block above, because that
// is the whole point: the check runs while reset is asserted, and the pins mean nothing
// then. The counter still needs an initial value, or the variant is unmeasurable rather
// than merely wrong.
initial t3_no_reset_guard = {CNT_W{1'b0}};
always @(posedge clk) begin
if (clr) t3_no_reset_guard <= {CNT_W{1'b0}};
else if (cs_n && bad) t3_no_reset_guard <= t3_no_reset_guard + 1'b1;
end
// ------------------------------------------------------------------
// T2 -- clocked on SCLK.
//
// This is the whole trap in two lines. The block is correct. Its condition is correct.
// It is sampled on a clock that does not run during the interval the condition is about,
// so it is evaluated a handful of times per transaction and never once while the bus is
// idle -- which is when the obligation applies.
// ------------------------------------------------------------------
always @(posedge sclk or negedge rst_n) begin
if (!rst_n) begin
t2_sclk_clocked <= {CNT_W{1'b0}};
t2_evals <= {CNT_W{1'b0}};
end else begin
// AND NOTE WHERE THIS CLEAR LIVES. `clr` is only acted on inside a block clocked
// on SCLK, so a variant clocked on the protocol's clock cannot even be RESET
// between test phases while that clock is idle. The testbench discovered this by
// measuring a counter that refused to go to zero, and it works in deltas
// afterwards. A checker whose clock the design controls is a checker the bench
// does not fully control either.
if (clr) begin
t2_sclk_clocked <= {CNT_W{1'b0}};
t2_evals <= {CNT_W{1'b0}};
end
if (cs_n) begin
t2_evals <= t2_evals + 1'b1;
if (bad) t2_sclk_clocked <= t2_sclk_clocked + 1'b1;
end
end
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_assert_traps.vhd — the same design in VHDL
-- spi_assert_traps.vhd
--
-- Chapter 17.2 -- ONE obligation, written FIVE ways, and the same faults shown to all five.
--
-- THE OBLIGATION.
--
-- while the slave is deselected, SCLK must sit at CPOL
--
-- That is Chapter 16.1's rule R1 and Chapter 17.1's property P5. It is about three lines of
-- anybody's assertion language, it is impossible to misunderstand, and there are at least four
-- ways to write it that do not work. This module implements all five and counts what each one
-- reports, because the differences between them are invisible in a review and obvious in a
-- measurement.
--
-- T1 CORRECT sampled on the OBSERVER's clock, guarded by reset, reported once
-- per offending cycle.
--
-- T2 CLOCKED ON SCLK the trap that looks like good practice: "check the SPI protocol on
-- the SPI clock". It is blind for TWO independent reasons, and the
-- second one is worse than the first.
--
-- First, SCLK STOPS between transactions, so there is no clock edge
-- during most of the interval this obligation is about.
--
-- Second -- and this is the one that cannot be fixed by adding
-- stimulus -- a block clocked on `posedge sclk` samples SCLK only at
-- the instants SCLK IS 1. With CPOL = 1 the obligation is "SCLK must
-- be 1", so every evaluation point is a compliant one BY
-- CONSTRUCTION. The property is not merely under-exercised; it is
-- unfalsifiable. A checker clocked on the signal it checks can only
-- ever observe that signal in one state.
--
-- T3 NO RESET GUARD the same check without `disable iff (!rst_n)`. Correct once the
-- design is running, and it fires throughout reset, when the pins
-- mean nothing. Noisy rather than dangerous -- and the usual fix
-- for the noise is T4.
--
-- T4 DISABLE OVERLAPS `disable iff (cs_n)` -- added by somebody silencing T3's noise, or
-- by somebody who reasoned that a deselected bus is not interesting.
-- The disable condition is EXACTLY the antecedent, so the property is
-- switched off precisely when it applies. It reports zero on every
-- stimulus, including the ones designed to break it. This is the
-- dangerous one.
--
-- T5 EDGE-REPORTED identical to T1 except that it reports once per OFFENCE rather than
-- once per offending cycle. Not a correctness difference; a reporting
-- difference, and the one people argue about while T4 sits in the same
-- file reporting nothing.
--
-- THE MEASUREMENT NEEDS THREE STIMULI, and the third is the one that separates T2.
--
-- S1 legal traffic
-- S2 SCLK parked off CPOL while deselected, WITH SCLK edges in the window
-- S3 SCLK parked off CPOL while deselected, with NO SCLK edges in the window
--
-- S3 is not a contrived stimulus. It is what a master does after its mode register is
-- reprogrammed and before its next transfer: the clock sits at the wrong level and does not
-- move. Chapter 16.4 found exactly that fault in its own driver.
--
-- WHAT VHDL ADDS TO THIS CHAPTER: the counters travel as a RECORD, so a sixth variant costs
-- nothing at any connection, and the five variants' blocks sit side by side in one file where
-- the differences between them are a diff rather than an argument.
--
-- And one VHDL-specific version of the same trap, worth naming because it is easier to write
-- here than in SystemVerilog: a process whose SENSITIVITY LIST omits a signal it reads is
-- evaluated only when the listed signals move. `process (sclk)` reading `cs_n` is the exact
-- structure of variant T2, and VHDL makes it a one-word mistake rather than a clocking
-- decision. The analyser says nothing; the checker simply never runs when the thing it checks
-- changes.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
package spi_trap_pkg is
type trap_counts_t is record
t1_correct : natural; -- sampled on the observer's clock, reset-guarded
t2_sclk_clocked : natural; -- clocked on SCLK
t3_no_reset_guard : natural; -- the same check, unguarded
t4_disable_overlaps : natural; -- the disable condition IS the antecedent
t5_edge_reported : natural; -- once per offence rather than per cycle
t1_evals : natural; -- how often T1 was evaluated
t2_evals : natural; -- how often T2 was -- the number that explains it
end record;
constant TRAPS_ZERO : trap_counts_t := (0, 0, 0, 0, 0, 0, 0);
end package spi_trap_pkg;
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use work.spi_trap_pkg.all;
entity spi_assert_traps is
port (
clk : in std_logic; -- the OBSERVER's clock
rst_n : in std_logic;
sclk : in std_logic;
cs_n : in std_logic;
cpol : in std_logic;
clr : in std_logic;
counts : out trap_counts_t
);
end entity spi_assert_traps;
architecture rtl of spi_assert_traps is
signal c : trap_counts_t := TRAPS_ZERO;
-- `bad` IS A FUNCTION, NOT A SIGNAL, and that is not a stylistic preference.
--
-- Written as a concurrent signal assignment -- one delta STALE inside every clocked process
-- that reads it -- the SCLK-clocked variant evaluates the PRE-EDGE value of SCLK, which is
-- the opposite level to the one its own clock edge has just established. It then reports
-- offences the SystemVerilog and Verilog versions of this same module do not: two languages,
-- one design, different numbers, from a derived signal that looked like a convenience.
--
-- This is Chapter 16.3's subject arriving inside a checker: where a derived event is
-- computed decides which instant the property is about.
pure function is_bad (s : std_logic; p : std_logic) return boolean is
begin
return s /= p;
end function is_bad;
begin
counts <= c;
-- ------------------------------------------------------------------
-- T1, T4, T5 -- all sampled on the observer's clock, all reset-guarded.
-- ------------------------------------------------------------------
observer : process (clk, rst_n) is
variable prev_bad_sel : boolean := false;
begin
if rst_n = '0' then
c.t1_correct <= 0;
c.t4_disable_overlaps <= 0;
c.t5_edge_reported <= 0;
c.t1_evals <= 0;
prev_bad_sel := false;
elsif rising_edge(clk) then
if clr = '1' then
c.t1_correct <= 0;
c.t4_disable_overlaps <= 0;
c.t5_edge_reported <= 0;
c.t1_evals <= 0;
end if;
-- T1 -- the obligation, reported once per offending cycle.
if cs_n = '1' then
c.t1_evals <= c.t1_evals + 1;
if is_bad(sclk, cpol) then
c.t1_correct <= c.t1_correct + 1;
end if;
end if;
-- T4 -- `disable iff (cs_n)`. The disable condition IS the antecedent, so the
-- consequent is never evaluated. Written out procedurally the defect is obvious;
-- written as one line between two correct-looking properties it is not.
if (cs_n = '1') and (cs_n = '0') then
c.t4_disable_overlaps <= c.t4_disable_overlaps + 1;
end if;
-- T5 -- the same obligation, reported on the TRANSITION into the offence.
if (cs_n = '1') and is_bad(sclk, cpol) and not prev_bad_sel then
c.t5_edge_reported <= c.t5_edge_reported + 1;
end if;
prev_bad_sel := (cs_n = '1') and is_bad(sclk, cpol);
end if;
end process observer;
-- T3 -- no reset guard. Deliberately NOT in the reset-sensitive process above, because that
-- is the whole point: the check runs while reset is asserted, and the pins mean nothing
-- then. The counter is still initialised at declaration, or the variant is unmeasurable
-- rather than merely wrong.
unguarded : process (clk) is
begin
if rising_edge(clk) then
if clr = '1' then
c.t3_no_reset_guard <= 0;
elsif (cs_n = '1') and is_bad(sclk, cpol) then
c.t3_no_reset_guard <= c.t3_no_reset_guard + 1;
end if;
end if;
end process unguarded;
-- ------------------------------------------------------------------
-- T2 -- clocked on SCLK.
--
-- The process is correct. Its condition is correct. It is sampled on a clock that stops
-- between transactions, and -- worse -- its every evaluation instant is one where SCLK is
-- '1', which with CPOL = '1' is the compliant value. The obligation cannot fail here.
--
-- Note also where `clr` lives: a checker whose clock the DESIGN controls is a checker the
-- TESTBENCH cannot reset either, so the bench measures it in deltas.
-- ------------------------------------------------------------------
sclk_clocked : process (sclk, rst_n) is
begin
if rst_n = '0' then
c.t2_sclk_clocked <= 0;
c.t2_evals <= 0;
elsif rising_edge(sclk) then
if clr = '1' then
c.t2_sclk_clocked <= 0;
c.t2_evals <= 0;
end if;
if cs_n = '1' then
c.t2_evals <= c.t2_evals + 1;
if is_bad(sclk, cpol) then
c.t2_sclk_clocked <= c.t2_sclk_clocked + 1;
end if;
end if;
end if;
end process sclk_clocked;
end architecture rtl;The Bench
Azvya Education Pvt. Ltd.VLSI Mentor
spi_assert_traps_tb.sv — three stimuli through all five variants, and the clear that never arrives
// spi_assert_traps_tb.sv
//
// FIVE WRITINGS OF ONE OBLIGATION, THREE STIMULI, AND A TABLE.
//
// The obligation is "while deselected, SCLK sits at CPOL". CPOL is 1 throughout, so the
// offending level is 0 -- which matters for stimulus 3 and is explained there.
//
// WHAT EACH STIMULUS IS FOR.
//
// S1 LEGAL TRAFFIC every variant must report zero. T3 is the exception and it is
// expected: it has no reset guard, so it counts the reset interval,
// during which the pins mean nothing.
//
// S2 THE FAULT, WITH SCLK MOVING IN THE WINDOW. SCLK is parked at the wrong level and toggled
// while the bus is idle, so a checker clocked on SCLK DOES get clock
// edges here -- and still reports nothing. Its evaluation instants
// are the rising edges of SCLK, and at a rising edge SCLK is 1,
// which with CPOL = 1 is exactly the compliant value. Giving it
// more clock does not help, because every clock it gets arrives at
// a moment when the obligation is satisfied.
//
// S3 THE FAULT, WITH SCLK STILL. SCLK is parked at 0 while CPOL is 1 and then returned. The
// only edges are the fall into the offence and the rise out of it,
// so the SCLK-clocked variant is evaluated ONCE -- at the compliant
// edge -- against the correct variant's twelve. This is the
// arithmetic of the first blindness, and the evaluation counters are
// what make it visible.
//
// This is not a contrived stimulus. It is what a master does after its mode register is
// reprogrammed and before its next transfer: the clock sits at the wrong level and does not
// move. Chapter 16.4 found exactly that fault in its own driver, and the rule monitor that
// caught it was clocked on the observer's clock.
//
// AND THE FOURTH MEASUREMENT: T4 reports ZERO ON ALL THREE STIMULI. Its `disable iff` condition
// is exactly its antecedent, so nothing it could ever report exists. A property like that is
// indistinguishable from a working one in every report a suite produces, and the number that
// exposes it is the evaluation count -- which is the same instrument Chapter 16.1 built for
// rules and Chapter 17.1 built for attempts.
`timescale 1ns/1ps
module spi_assert_traps_tb;
localparam int LEAD = 4;
localparam int HALF = 3;
localparam int LAG = 2;
localparam int GAP = 3;
localparam int DW = 32;
localparam int LEN_W = 6;
localparam int CNT_W = 16;
reg clk = 1'b0;
always #5 clk = ~clk;
reg rst_n = 1'b1;
// CPOL is 1 for the whole run, so the offending SCLK level is 0. Stimulus 3 depends on it.
localparam CPOL = 1'b1;
reg start = 1'b0;
wire busy, done;
wire [DW-1:0] drv_rx;
wire d_sclk, d_cs_n, d_mosi;
reg sel_bench = 1'b0;
reg b_sclk = CPOL, b_cs_n = 1'b1;
wire sclk = sel_bench ? b_sclk : d_sclk;
wire cs_n = sel_bench ? b_cs_n : d_cs_n;
wire mosi = d_mosi;
wire miso = ~mosi;
spi_driver #(.LEAD(LEAD), .HALF(HALF), .LAG(LAG), .GAP(GAP),
.DW(DW), .LEN_W(LEN_W), .CNT_W(16)) u_drv (
.clk(clk), .rst_n(rst_n),
.start(start), .tx_data(32'h0000_1A5C), .nbits(6'd8),
.cpol(CPOL), .cpha(1'b0), .lsb_first(1'b0), .fault(3'd0),
.busy(busy), .done(done), .rx_data(drv_rx),
.sclk(d_sclk), .cs_n(d_cs_n), .mosi(d_mosi), .miso(miso)
);
reg clr = 1'b0;
wire [CNT_W-1:0] t1, t2, t3, t4, t5, e1, e2;
spi_assert_traps #(.CNT_W(CNT_W)) u_t (
.clk(clk), .rst_n(rst_n),
.sclk(sclk), .cs_n(cs_n), .cpol(CPOL),
.clr(clr),
.t1_correct(t1), .t2_sclk_clocked(t2), .t3_no_reset_guard(t3),
.t4_disable_overlaps(t4), .t5_edge_reported(t5),
.t1_evals(e1), .t2_evals(e2)
);
integer errors = 0;
initial begin
#200_000;
$display("FAIL: the simulation did not finish within its time limit");
$finish;
end
task automatic clear_counts;
begin
@(negedge clk); clr = 1'b1;
@(negedge clk); clr = 1'b0;
@(negedge clk);
end
endtask
task automatic idle_n(input integer n);
integer i;
begin for (i = 0; i < n; i = i + 1) @(negedge clk); end
endtask
task automatic run_burst(input integer ntxn);
integer k;
begin
k = 0;
@(negedge clk);
start = 1'b1;
while (k < ntxn) begin
@(negedge clk);
if (done) begin k = k + 1; if (k == ntxn) start = 1'b0; end
end
idle_n(GAP + LAG + 8);
end
endtask
// The window length the fault lasts, in observer cycles. Every variant that works should
// report either WINDOW (once per cycle) or 1 (once per offence).
localparam int WINDOW = 6;
integer s1_t1, s1_t2, s1_t3, s1_t4, s1_t5;
integer s2_t1, s2_t2, s2_t3, s2_t4, s2_t5;
integer s3_t1, s3_t2, s3_t3, s3_t4, s3_t5, s3_e1, s3_e2;
integer b_t1, b_t2, b_t3, b_t4, b_t5, b_e1, b_e2;
integer clr_t2_before, clr_t2_after;
integer reset_hits;
// EVERY MEASUREMENT BELOW IS A DELTA, and that is a finding rather than a style choice.
// `clr` reaches four of the five variants immediately and reaches the SCLK-clocked one only
// when SCLK next moves -- so with the protocol's clock idle, its counters cannot be zeroed
// at all. Snapshot-and-subtract is the only way to measure a checker whose clock the
// testbench does not control.
task automatic snapshot;
begin
b_t1 = t1; b_t2 = t2; b_t3 = t3; b_t4 = t4; b_t5 = t5; b_e1 = e1; b_e2 = e2;
end
endtask
initial begin
// Reset, and the reset-interval measurement is taken WHILE RESET IS STILL ASSERTED.
// Sampling after the release would fold in a different artefact: the driver needs one
// cycle to park SCLK at CPOL once it leaves reset, so a correct checker legitimately
// reports one offending cycle there. That is the same settling artefact Chapter 16.4
// bracketed, and mixing it into this measurement would make the reset trap look
// one-count smaller than it is.
// Reset is asserted FIRST and the baseline is taken after it has settled, so the
// measured interval is exactly the reset interval. Baselining before the assert would
// fold in the cycles where the pins are still uninitialised -- and would make the
// reset-guarded variant's delta non-zero for a reason that has nothing to do with
// reset guarding.
// `rst_n` starts high and falls after a clock edge, so the reset is a real EDGE. Driving
// it low in the same time step as its declaration initialiser leaves the negedge
// unobserved in one of the three languages -- the counters then start at X, the whole
// run propagates X, and the bench hangs waiting for a handshake that never resolves.
rst_n = 1'b1;
@(negedge clk);
rst_n = 1'b0;
repeat (2) @(negedge clk);
snapshot();
repeat (6) @(negedge clk);
reset_hits = t3 - b_t3;
$display(" measured WHILE reset is asserted, when the pins mean nothing:");
$display(" T1 correct (reset-guarded) ..... %0d", t1 - b_t1);
$display(" T3 no reset guard .............. %0d", reset_hits);
if (reset_hits == 0) begin
$display(" FAIL: the unguarded variant counted nothing during reset, so this run cannot demonstrate the reset trap");
errors = errors + 1;
end
if ((t1 - b_t1) != 0) begin
$display(" FAIL: the reset-guarded variant counted %0d during reset", t1 - b_t1);
errors = errors + 1;
end
rst_n = 1'b1;
repeat (6) @(negedge clk);
// ============================================================
// S1 -- legal traffic.
// ============================================================
sel_bench = 1'b0;
snapshot();
run_burst(3);
s1_t1 = t1 - b_t1; s1_t2 = t2 - b_t2; s1_t3 = t3 - b_t3;
s1_t4 = t4 - b_t4; s1_t5 = t5 - b_t5;
// ============================================================
// S2 -- the fault, with SCLK moving inside the window.
// ============================================================
sel_bench = 1'b1;
b_cs_n = 1'b1; b_sclk = CPOL;
idle_n(4);
snapshot();
b_sclk = ~CPOL; // park at the wrong level
idle_n(2);
b_sclk = CPOL; idle_n(1); // ... and move it about inside the window
b_sclk = ~CPOL; idle_n(2);
b_sclk = CPOL;
idle_n(6);
s2_t1 = t1 - b_t1; s2_t2 = t2 - b_t2; s2_t3 = t3 - b_t3;
s2_t4 = t4 - b_t4; s2_t5 = t5 - b_t5;
// ============================================================
// S3 -- the fault, with SCLK still.
//
// CPOL is 1, so parking at the wrong level is a FALL and returning is a RISE. The
// rise happens on the cycle the fault ENDS, when the bus is already compliant -- so a
// checker clocked on `posedge sclk` is evaluated either not at all inside the window
// or only at its compliant edge.
// ============================================================
idle_n(4);
// AND FIRST, THE CLEAR THAT DOES NOT ARRIVE. `clr` is pulsed here with SCLK idle. Four
// of the five variants zero immediately; the SCLK-clocked one does not, because its
// clear is inside a block clocked on SCLK. This is measured rather than described.
clr_t2_before = t2 + e2;
clear_counts();
clr_t2_after = t2 + e2;
snapshot();
b_sclk = ~CPOL; // a FALLING edge into the offence
idle_n(WINDOW);
b_sclk = CPOL; // a RISING edge out of it
idle_n(6);
s3_t1 = t1 - b_t1; s3_t2 = t2 - b_t2; s3_t3 = t3 - b_t3;
s3_t4 = t4 - b_t4; s3_t5 = t5 - b_t5;
s3_e1 = e1 - b_e1; s3_e2 = e2 - b_e2;
// ============================================================
// The table.
// ============================================================
$display(" variant S1 legal S2 fault, SCLK moving S3 fault, SCLK still");
$display(" T1 correct %8d %21d %20d", s1_t1, s2_t1, s3_t1);
$display(" T2 clocked on SCLK %8d %21d %20d", s1_t2, s2_t2, s3_t2);
$display(" T3 no reset guard %8d %21d %20d", s1_t3, s2_t3, s3_t3);
$display(" T4 disable iff overlaps %8d %21d %20d", s1_t4, s2_t4, s3_t4);
$display(" T5 edge-reported %8d %21d %20d", s1_t5, s2_t5, s3_t5);
$display(" and the EVALUATION counts over S3: T1 evaluated %0d times, T2 evaluated %0d",
s3_e1, s3_e2);
$display(" the clear pulsed with SCLK idle: T2's counters went from %0d to %0d",
clr_t2_before, clr_t2_after);
if (clr_t2_before != clr_t2_after) begin
$display(" FAIL: the SCLK-clocked variant's counters DID clear with SCLK idle, so this run cannot demonstrate that its clear depends on the design's clock");
errors = errors + 1;
end
$display(" 0. before any of that: a clear pulsed while SCLK was idle left the SCLK-clocked variant's counters untouched, because its clear lives inside a block clocked on SCLK. A checker whose clock the DESIGN controls is a checker the TESTBENCH cannot reset either -- so every measurement below is a delta");
// ---- S1: nothing should fire on legal traffic ----
if (s1_t1 != 0 || s1_t2 != 0 || s1_t3 != 0 || s1_t4 != 0 || s1_t5 != 0) begin
$display(" FAIL: a variant fired on legal traffic (%0d %0d %0d %0d %0d)",
s1_t1, s1_t2, s1_t3, s1_t4, s1_t5);
errors = errors + 1;
end
$display(" 1. on legal traffic all five variants report zero, which is exactly the problem: five writings of one obligation, four of them defective, and a clean regression cannot tell them apart");
// ---- S2: the working variants must fire ----
if (s2_t1 == 0 || s2_t3 == 0 || s2_t5 == 0) begin
$display(" FAIL: a working variant missed the fault with SCLK moving (T1 %0d, T3 %0d, T5 %0d)",
s2_t1, s2_t3, s2_t5);
errors = errors + 1;
end
if (s2_t5 >= s2_t1) begin
$display(" FAIL: the edge-reported variant did not report FEWER times than the per-cycle one (%0d vs %0d)",
s2_t5, s2_t1);
errors = errors + 1;
end
if (s2_t2 != 0) begin
$display(" FAIL: the SCLK-clocked variant reported %0d with SCLK moving; every clock edge it gets arrives at a compliant instant, so it should be unable to report anything",
s2_t2);
errors = errors + 1;
end
$display(" 2. with SCLK MOVING in the window -- so the SCLK-clocked variant does get clock edges -- T1 reported %0d offending cycles, T5 reported %0d offences, and T2 still reported %0d. More clock does not help it: a block clocked on `posedge sclk` is evaluated only at instants where SCLK is 1, and with CPOL = 1 the obligation at every one of those instants is already satisfied. The property is not under-exercised, it is UNFALSIFIABLE -- a checker clocked on the signal it checks can only ever observe that signal in one state",
s2_t1, s2_t5, s2_t2);
// ---- S3: the SCLK-clocked variant must go blind ----
if (s3_t1 == 0) begin
$display(" FAIL: the correct variant missed the fault with SCLK still");
errors = errors + 1;
end
if (s3_t2 != 0) begin
$display(" FAIL: the SCLK-clocked variant reported %0d with SCLK still; this stimulus is supposed to leave it with no clock edge inside the window",
s3_t2);
errors = errors + 1;
end
if (s3_e2 >= s3_e1) begin
$display(" FAIL: the SCLK-clocked variant was evaluated %0d times against the correct variant's %0d; the point of this stimulus is that it is evaluated far less often",
s3_e2, s3_e1);
errors = errors + 1;
end
$display(" 3. with SCLK STILL, the correct variant reported %0d offending cycles and the SCLK-clocked one reported ZERO -- and its evaluation counter says why: it was evaluated %0d times against the correct variant's %0d. A checker clocked on the protocol's own clock has no clock during the interval this obligation is about",
s3_t1, s3_e2, s3_e1);
// ---- T4 must be silent everywhere ----
if (s1_t4 != 0 || s2_t4 != 0 || s3_t4 != 0) begin
$display(" FAIL: the overlapping-disable variant reported something; it is supposed to be structurally incapable of reporting");
errors = errors + 1;
end
$display(" 4. the overlapping-disable variant reported ZERO on all three stimuli, including both faults. Its disable condition IS its antecedent, so there is nothing it could ever report -- and in a suite's output it is indistinguishable from the correct variant. Somebody adds a `disable iff` to silence noise like T3's, and the property it lands on stops existing");
if (errors == 0)
$display("PASS: one obligation -- while deselected, SCLK sits at CPOL -- written five ways, and on legal traffic all five report zero, which is precisely why four of them survive review. With the fault present and SCLK MOVING in the window -- so the SCLK-clocked variant does receive clock edges -- the correct variant reported %0d offending cycles, the edge-reported variant reported %0d offences, and the SCLK-clocked variant reported %0d. More clock does not rescue it: a block clocked on `posedge sclk` is evaluated only at instants where SCLK is 1, and with CPOL = 1 the obligation is satisfied at every one of those instants, so the property is UNFALSIFIABLE rather than merely under-exercised. A checker clocked on the signal it checks can only ever observe that signal in one state. With the fault present and SCLK STILL -- which is what a master does after its mode register is reprogrammed and before its next transfer, and is the exact fault Chapter 16.4 found in its own driver -- the correct variant reported %0d and the SCLK-clocked one reported ZERO, evaluated %0d times against %0d, because the protocol's clock does not run during the interval an idle-time obligation is about. The unguarded variant fired %0d times during reset, when the pins mean nothing, and the usual fix for that noise is the fifth variant: a `disable iff` whose condition is exactly the antecedent, which reported ZERO on every stimulus including both faults and is indistinguishable in any report from the one that works. The instrument that separates them is not the failure count. It is the EVALUATION count, which is the same thing Chapter 16.1 called `exercised` and Chapter 17.1 called `attempts`",
s2_t1, s2_t5, s2_t2, s3_t1, s3_e2, s3_e1, reset_hits);
else
$display("FAIL: %0d error(s)", errors);
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_assert_traps_tb.v — the same bench in Verilog-2001
// spi_assert_traps_tb.v
//
// FIVE WRITINGS OF ONE OBLIGATION, THREE STIMULI, AND A TABLE.
//
// The obligation is "while deselected, SCLK sits at CPOL". CPOL is 1 throughout, so the
// offending level is 0 -- which matters for stimulus 3 and is explained there.
//
// WHAT EACH STIMULUS IS FOR.
//
// S1 LEGAL TRAFFIC every variant must report zero. T3 is the exception and it is
// expected: it has no reset guard, so it counts the reset interval,
// during which the pins mean nothing.
//
// S2 THE FAULT, WITH SCLK MOVING IN THE WINDOW. SCLK is parked at the wrong level and toggled
// while the bus is idle, so a checker clocked on SCLK DOES get clock
// edges here -- and still reports nothing. Its evaluation instants
// are the rising edges of SCLK, and at a rising edge SCLK is 1,
// which with CPOL = 1 is exactly the compliant value. Giving it
// more clock does not help, because every clock it gets arrives at
// a moment when the obligation is satisfied.
//
// S3 THE FAULT, WITH SCLK STILL. SCLK is parked at 0 while CPOL is 1 and then returned. The
// only edges are the fall into the offence and the rise out of it,
// so the SCLK-clocked variant is evaluated ONCE -- at the compliant
// edge -- against the correct variant's twelve. This is the
// arithmetic of the first blindness, and the evaluation counters are
// what make it visible.
//
// This is not a contrived stimulus. It is what a master does after its mode register is
// reprogrammed and before its next transfer: the clock sits at the wrong level and does not
// move. Chapter 16.4 found exactly that fault in its own driver, and the rule monitor that
// caught it was clocked on the observer's clock.
//
// AND THE FOURTH MEASUREMENT: T4 reports ZERO ON ALL THREE STIMULI. Its `disable iff` condition
// is exactly its antecedent, so nothing it could ever report exists. A property like that is
// indistinguishable from a working one in every report a suite produces, and the number that
// exposes it is the evaluation count -- which is the same instrument Chapter 16.1 built for
// rules and Chapter 17.1 built for attempts.
`timescale 1ns/1ps
module spi_assert_traps_tb;
localparam LEAD = 4;
localparam HALF = 3;
localparam LAG = 2;
localparam GAP = 3;
localparam DW = 32;
localparam LEN_W = 6;
localparam CNT_W = 16;
reg clk;
always #5 clk = ~clk;
reg rst_n;
// CPOL is 1 for the whole run, so the offending SCLK level is 0. Stimulus 3 depends on it.
localparam CPOL = 1'b1;
reg start;
wire busy, done;
wire [DW-1:0] drv_rx;
wire d_sclk, d_cs_n, d_mosi;
reg sel_bench;
reg b_sclk, b_cs_n;
wire sclk = sel_bench ? b_sclk : d_sclk;
wire cs_n = sel_bench ? b_cs_n : d_cs_n;
wire mosi = d_mosi;
wire miso = ~mosi;
spi_driver #(.LEAD(LEAD), .HALF(HALF), .LAG(LAG), .GAP(GAP),
.DW(DW), .LEN_W(LEN_W), .CNT_W(16)) u_drv (
.clk(clk), .rst_n(rst_n),
.start(start), .tx_data(32'h0000_1A5C), .nbits(6'd8),
.cpol(CPOL), .cpha(1'b0), .lsb_first(1'b0), .fault(3'd0),
.busy(busy), .done(done), .rx_data(drv_rx),
.sclk(d_sclk), .cs_n(d_cs_n), .mosi(d_mosi), .miso(miso)
);
reg clr;
wire [CNT_W-1:0] t1, t2, t3, t4, t5, e1, e2;
spi_assert_traps #(.CNT_W(CNT_W)) u_t (
.clk(clk), .rst_n(rst_n),
.sclk(sclk), .cs_n(cs_n), .cpol(CPOL),
.clr(clr),
.t1_correct(t1), .t2_sclk_clocked(t2), .t3_no_reset_guard(t3),
.t4_disable_overlaps(t4), .t5_edge_reported(t5),
.t1_evals(e1), .t2_evals(e2)
);
integer errors;
initial begin
#200_000;
$display("FAIL: the simulation did not finish within its time limit");
$finish;
end
task clear_counts;
begin
@(negedge clk); clr = 1'b1;
@(negedge clk); clr = 1'b0;
@(negedge clk);
end
endtask
task idle_n;
input integer n;
integer i;
begin for (i = 0; i < n; i = i + 1) @(negedge clk); end
endtask
task run_burst;
input integer ntxn;
integer k;
begin
k = 0;
@(negedge clk);
start = 1'b1;
while (k < ntxn) begin
@(negedge clk);
if (done) begin k = k + 1; if (k == ntxn) start = 1'b0; end
end
idle_n(GAP + LAG + 8);
end
endtask
// The window length the fault lasts, in observer cycles. Every variant that works should
// report either WINDOW (once per cycle) or 1 (once per offence).
localparam WINDOW = 6;
integer s1_t1, s1_t2, s1_t3, s1_t4, s1_t5;
integer s2_t1, s2_t2, s2_t3, s2_t4, s2_t5;
integer s3_t1, s3_t2, s3_t3, s3_t4, s3_t5, s3_e1, s3_e2;
integer b_t1, b_t2, b_t3, b_t4, b_t5, b_e1, b_e2;
integer clr_t2_before, clr_t2_after;
integer reset_hits;
// EVERY MEASUREMENT BELOW IS A DELTA, and that is a finding rather than a style choice.
// `clr` reaches four of the five variants immediately and reaches the SCLK-clocked one only
// when SCLK next moves -- so with the protocol's clock idle, its counters cannot be zeroed
// at all. Snapshot-and-subtract is the only way to measure a checker whose clock the
// testbench does not control.
task snapshot;
begin
b_t1 = t1; b_t2 = t2; b_t3 = t3; b_t4 = t4; b_t5 = t5; b_e1 = e1; b_e2 = e2;
end
endtask
initial begin
// Reset, and the reset-interval measurement is taken WHILE RESET IS STILL ASSERTED.
// Sampling after the release would fold in a different artefact: the driver needs one
// cycle to park SCLK at CPOL once it leaves reset, so a correct checker legitimately
// reports one offending cycle there. That is the same settling artefact Chapter 16.4
// bracketed, and mixing it into this measurement would make the reset trap look
// one-count smaller than it is.
// Reset is asserted FIRST and the baseline is taken after it has settled, so the
// measured interval is exactly the reset interval. Baselining before the assert would
// fold in the cycles where the pins are still uninitialised -- and would make the
// reset-guarded variant's delta non-zero for a reason that has nothing to do with
// reset guarding.
// `rst_n` starts high and falls after a clock edge, so the reset is a real EDGE. Driving
// it low in the same time step as its declaration initialiser leaves the negedge
// unobserved in one of the three languages -- the counters then start at X, the whole
// run propagates X, and the bench hangs waiting for a handshake that never resolves.
rst_n = 1'b1;
@(negedge clk);
rst_n = 1'b0;
repeat (2) @(negedge clk);
snapshot();
repeat (6) @(negedge clk);
reset_hits = t3 - b_t3;
$display(" measured WHILE reset is asserted, when the pins mean nothing:");
$display(" T1 correct (reset-guarded) ..... %0d", t1 - b_t1);
$display(" T3 no reset guard .............. %0d", reset_hits);
if (reset_hits == 0) begin
$display(" FAIL: the unguarded variant counted nothing during reset, so this run cannot demonstrate the reset trap");
errors = errors + 1;
end
if ((t1 - b_t1) != 0) begin
$display(" FAIL: the reset-guarded variant counted %0d during reset", t1 - b_t1);
errors = errors + 1;
end
rst_n = 1'b1;
repeat (6) @(negedge clk);
// ============================================================
// S1 -- legal traffic.
// ============================================================
sel_bench = 1'b0;
snapshot();
run_burst(3);
s1_t1 = t1 - b_t1; s1_t2 = t2 - b_t2; s1_t3 = t3 - b_t3;
s1_t4 = t4 - b_t4; s1_t5 = t5 - b_t5;
// ============================================================
// S2 -- the fault, with SCLK moving inside the window.
// ============================================================
sel_bench = 1'b1;
b_cs_n = 1'b1; b_sclk = CPOL;
idle_n(4);
snapshot();
b_sclk = ~CPOL; // park at the wrong level
idle_n(2);
b_sclk = CPOL; idle_n(1); // ... and move it about inside the window
b_sclk = ~CPOL; idle_n(2);
b_sclk = CPOL;
idle_n(6);
s2_t1 = t1 - b_t1; s2_t2 = t2 - b_t2; s2_t3 = t3 - b_t3;
s2_t4 = t4 - b_t4; s2_t5 = t5 - b_t5;
// ============================================================
// S3 -- the fault, with SCLK still.
//
// CPOL is 1, so parking at the wrong level is a FALL and returning is a RISE. The
// rise happens on the cycle the fault ENDS, when the bus is already compliant -- so a
// checker clocked on `posedge sclk` is evaluated either not at all inside the window
// or only at its compliant edge.
// ============================================================
idle_n(4);
// AND FIRST, THE CLEAR THAT DOES NOT ARRIVE. `clr` is pulsed here with SCLK idle. Four
// of the five variants zero immediately; the SCLK-clocked one does not, because its
// clear is inside a block clocked on SCLK. This is measured rather than described.
clr_t2_before = t2 + e2;
clear_counts();
clr_t2_after = t2 + e2;
snapshot();
b_sclk = ~CPOL; // a FALLING edge into the offence
idle_n(WINDOW);
b_sclk = CPOL; // a RISING edge out of it
idle_n(6);
s3_t1 = t1 - b_t1; s3_t2 = t2 - b_t2; s3_t3 = t3 - b_t3;
s3_t4 = t4 - b_t4; s3_t5 = t5 - b_t5;
s3_e1 = e1 - b_e1; s3_e2 = e2 - b_e2;
// ============================================================
// The table.
// ============================================================
$display(" variant S1 legal S2 fault, SCLK moving S3 fault, SCLK still");
$display(" T1 correct %8d %21d %20d", s1_t1, s2_t1, s3_t1);
$display(" T2 clocked on SCLK %8d %21d %20d", s1_t2, s2_t2, s3_t2);
$display(" T3 no reset guard %8d %21d %20d", s1_t3, s2_t3, s3_t3);
$display(" T4 disable iff overlaps %8d %21d %20d", s1_t4, s2_t4, s3_t4);
$display(" T5 edge-reported %8d %21d %20d", s1_t5, s2_t5, s3_t5);
$display(" and the EVALUATION counts over S3: T1 evaluated %0d times, T2 evaluated %0d",
s3_e1, s3_e2);
$display(" the clear pulsed with SCLK idle: T2's counters went from %0d to %0d",
clr_t2_before, clr_t2_after);
if (clr_t2_before != clr_t2_after) begin
$display(" FAIL: the SCLK-clocked variant's counters DID clear with SCLK idle, so this run cannot demonstrate that its clear depends on the design's clock");
errors = errors + 1;
end
$display(" 0. before any of that: a clear pulsed while SCLK was idle left the SCLK-clocked variant's counters untouched, because its clear lives inside a block clocked on SCLK. A checker whose clock the DESIGN controls is a checker the TESTBENCH cannot reset either -- so every measurement below is a delta");
// ---- S1: nothing should fire on legal traffic ----
if (s1_t1 != 0 || s1_t2 != 0 || s1_t3 != 0 || s1_t4 != 0 || s1_t5 != 0) begin
$display(" FAIL: a variant fired on legal traffic (%0d %0d %0d %0d %0d)",
s1_t1, s1_t2, s1_t3, s1_t4, s1_t5);
errors = errors + 1;
end
$display(" 1. on legal traffic all five variants report zero, which is exactly the problem: five writings of one obligation, four of them defective, and a clean regression cannot tell them apart");
// ---- S2: the working variants must fire ----
if (s2_t1 == 0 || s2_t3 == 0 || s2_t5 == 0) begin
$display(" FAIL: a working variant missed the fault with SCLK moving (T1 %0d, T3 %0d, T5 %0d)",
s2_t1, s2_t3, s2_t5);
errors = errors + 1;
end
if (s2_t5 >= s2_t1) begin
$display(" FAIL: the edge-reported variant did not report FEWER times than the per-cycle one (%0d vs %0d)",
s2_t5, s2_t1);
errors = errors + 1;
end
if (s2_t2 != 0) begin
$display(" FAIL: the SCLK-clocked variant reported %0d with SCLK moving; every clock edge it gets arrives at a compliant instant, so it should be unable to report anything",
s2_t2);
errors = errors + 1;
end
$display(" 2. with SCLK MOVING in the window -- so the SCLK-clocked variant does get clock edges -- T1 reported %0d offending cycles, T5 reported %0d offences, and T2 still reported %0d. More clock does not help it: a block clocked on `posedge sclk` is evaluated only at instants where SCLK is 1, and with CPOL = 1 the obligation at every one of those instants is already satisfied. The property is not under-exercised, it is UNFALSIFIABLE -- a checker clocked on the signal it checks can only ever observe that signal in one state",
s2_t1, s2_t5, s2_t2);
// ---- S3: the SCLK-clocked variant must go blind ----
if (s3_t1 == 0) begin
$display(" FAIL: the correct variant missed the fault with SCLK still");
errors = errors + 1;
end
if (s3_t2 != 0) begin
$display(" FAIL: the SCLK-clocked variant reported %0d with SCLK still; this stimulus is supposed to leave it with no clock edge inside the window",
s3_t2);
errors = errors + 1;
end
if (s3_e2 >= s3_e1) begin
$display(" FAIL: the SCLK-clocked variant was evaluated %0d times against the correct variant's %0d; the point of this stimulus is that it is evaluated far less often",
s3_e2, s3_e1);
errors = errors + 1;
end
$display(" 3. with SCLK STILL, the correct variant reported %0d offending cycles and the SCLK-clocked one reported ZERO -- and its evaluation counter says why: it was evaluated %0d times against the correct variant's %0d. A checker clocked on the protocol's own clock has no clock during the interval this obligation is about",
s3_t1, s3_e2, s3_e1);
// ---- T4 must be silent everywhere ----
if (s1_t4 != 0 || s2_t4 != 0 || s3_t4 != 0) begin
$display(" FAIL: the overlapping-disable variant reported something; it is supposed to be structurally incapable of reporting");
errors = errors + 1;
end
$display(" 4. the overlapping-disable variant reported ZERO on all three stimuli, including both faults. Its disable condition IS its antecedent, so there is nothing it could ever report -- and in a suite's output it is indistinguishable from the correct variant. Somebody adds a `disable iff` to silence noise like T3's, and the property it lands on stops existing");
if (errors == 0)
$display("PASS: one obligation -- while deselected, SCLK sits at CPOL -- written five ways, and on legal traffic all five report zero, which is precisely why four of them survive review. With the fault present and SCLK MOVING in the window -- so the SCLK-clocked variant does receive clock edges -- the correct variant reported %0d offending cycles, the edge-reported variant reported %0d offences, and the SCLK-clocked variant reported %0d. More clock does not rescue it: a block clocked on `posedge sclk` is evaluated only at instants where SCLK is 1, and with CPOL = 1 the obligation is satisfied at every one of those instants, so the property is UNFALSIFIABLE rather than merely under-exercised. A checker clocked on the signal it checks can only ever observe that signal in one state. With the fault present and SCLK STILL -- which is what a master does after its mode register is reprogrammed and before its next transfer, and is the exact fault Chapter 16.4 found in its own driver -- the correct variant reported %0d and the SCLK-clocked one reported ZERO, evaluated %0d times against %0d, because the protocol's clock does not run during the interval an idle-time obligation is about. The unguarded variant fired %0d times during reset, when the pins mean nothing, and the usual fix for that noise is the fifth variant: a `disable iff` whose condition is exactly the antecedent, which reported ZERO on every stimulus including both faults and is indistinguishable in any report from the one that works. The instrument that separates them is not the failure count. It is the EVALUATION count, which is the same thing Chapter 16.1 called `exercised` and Chapter 17.1 called `attempts`",
s2_t1, s2_t5, s2_t2, s3_t1, s3_e2, s3_e1, reset_hits);
else
$display("FAIL: %0d error(s)", errors);
$finish;
end
initial begin
b_sclk = CPOL;
b_cs_n = 1'b1;
clk = 1'b0;
rst_n = 1'b1;
start = 1'b0;
sel_bench = 1'b0;
clr = 1'b0;
errors = 0;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_assert_traps_tb.vhd — the same bench in VHDL
-- spi_assert_traps_tb.vhd
--
-- FIVE WRITINGS OF ONE OBLIGATION, THREE STIMULI, AND A TABLE.
--
-- The obligation is "while deselected, SCLK sits at CPOL". CPOL is 1 throughout, so the
-- offending level is 0 -- which matters for stimulus 3 and is explained there.
--
-- WHAT EACH STIMULUS IS FOR.
--
-- S1 LEGAL TRAFFIC every variant must report zero. T3 is the exception and it is
-- expected: it has no reset guard, so it counts the reset interval,
-- during which the pins mean nothing.
--
-- S2 THE FAULT, WITH SCLK MOVING IN THE WINDOW. SCLK is parked at the wrong level and toggled
-- while the bus is idle, so a checker clocked on SCLK DOES get clock
-- edges here -- and still reports nothing. Its evaluation instants
-- are the rising edges of SCLK, and at a rising edge SCLK is 1,
-- which with CPOL = 1 is exactly the compliant value. Giving it
-- more clock does not help, because every clock it gets arrives at
-- a moment when the obligation is satisfied.
--
-- S3 THE FAULT, WITH SCLK STILL. SCLK is parked at 0 while CPOL is 1 and then returned. The
-- only edges are the fall into the offence and the rise out of it,
-- so the SCLK-clocked variant is evaluated ONCE -- at the compliant
-- edge -- against the correct variant's twelve. This is the
-- arithmetic of the first blindness, and the evaluation counters are
-- what make it visible.
--
-- This is not a contrived stimulus. It is what a master does after its mode register is
-- reprogrammed and before its next transfer: the clock sits at the wrong level and does not
-- move. Chapter 16.4 found exactly that fault in its own driver, and the rule monitor that
-- caught it was clocked on the observer's clock.
--
-- AND THE FOURTH MEASUREMENT: T4 reports ZERO ON ALL THREE STIMULI. Its `disable iff` condition
-- is exactly its antecedent, so nothing it could ever report exists. A property like that is
-- indistinguishable from a working one in every report a suite produces, and the number that
-- exposes it is the evaluation count -- which is the same instrument Chapter 16.1 built for
-- rules and Chapter 17.1 built for attempts.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use work.spi_driver_pkg.all;
use work.spi_trap_pkg.all;
entity spi_assert_traps_tb is
end entity spi_assert_traps_tb;
architecture tb of spi_assert_traps_tb is
constant LEAD_C : natural := 4;
constant HALF_C : natural := 3;
constant LAG_C : natural := 2;
constant GAP_C : natural := 3;
constant HALF_T : time := 5 ns;
constant CPOL : std_logic := '1'; -- so the offending SCLK level is '0'
constant WINDOW : natural := 6;
signal clk : std_logic := '0';
signal rst_n : std_logic := '1';
signal done_sim : boolean := false;
signal start : std_logic := '0';
signal req : spi_req_t := (data => x"00001A5C",
nbits => to_unsigned(8, LEN_W),
cpol => CPOL,
cpha => '0',
lsb_first => '0',
fault => F_NONE);
signal busy, done : std_logic;
signal drv_rx : std_logic_vector(DW - 1 downto 0);
signal d_sclk, d_cs_n, d_mosi : std_logic;
signal sel_bench : boolean := false;
signal b_sclk : std_logic := CPOL;
signal b_cs_n : std_logic := '1';
signal sclk, cs_n, mosi, miso : std_logic;
signal clr : std_logic := '0';
signal c : trap_counts_t;
signal errors : integer := 0;
begin
sclk <= b_sclk when sel_bench else d_sclk;
cs_n <= b_cs_n when sel_bench else d_cs_n;
mosi <= d_mosi;
miso <= not mosi;
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_drv : entity work.spi_driver
generic map (LEAD => LEAD_C, HALF => HALF_C, LAG => LAG_C, GAP => GAP_C)
port map (clk => clk, rst_n => rst_n, start => start, req => req,
busy => busy, done => done, rx_data => drv_rx,
sclk => d_sclk, cs_n => d_cs_n, mosi => d_mosi, miso => miso);
u_t : entity work.spi_assert_traps
port map (clk => clk, rst_n => rst_n,
sclk => sclk, cs_n => cs_n, cpol => CPOL,
clr => clr, counts => c);
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 clear_counts is
begin
wait until falling_edge(clk); clr <= '1';
wait until falling_edge(clk); clr <= '0';
wait until falling_edge(clk);
end procedure clear_counts;
procedure run_burst (ntxn : natural) is
variable k : natural := 0;
begin
k := 0;
wait until falling_edge(clk);
start <= '1';
while k < ntxn loop
wait until falling_edge(clk);
if done = '1' then
k := k + 1;
if k = ntxn then start <= '0'; end if;
end if;
end loop;
idle_n(GAP_C + LAG_C + 8);
end procedure run_burst;
variable b : trap_counts_t;
variable s1, s2, s3 : trap_counts_t;
variable reset_hits : natural;
variable clr_t2_before, clr_t2_after : natural;
-- EVERY MEASUREMENT BELOW IS A DELTA, and that is a finding rather than a style choice.
-- `clr` reaches four of the five variants immediately and reaches the SCLK-clocked one
-- only when SCLK next moves -- so with the protocol's clock idle, its counters cannot be
-- zeroed at all. Snapshot-and-subtract is the only way to measure a checker whose clock
-- the testbench does not control.
impure function delta (now_c : trap_counts_t; base : trap_counts_t) return trap_counts_t is
begin
return (now_c.t1_correct - base.t1_correct,
now_c.t2_sclk_clocked - base.t2_sclk_clocked,
now_c.t3_no_reset_guard - base.t3_no_reset_guard,
now_c.t4_disable_overlaps - base.t4_disable_overlaps,
now_c.t5_edge_reported - base.t5_edge_reported,
now_c.t1_evals - base.t1_evals,
now_c.t2_evals - base.t2_evals);
end function delta;
begin
-- Reset, and the reset-interval measurement is taken WHILE RESET IS STILL ASSERTED.
-- Sampling after the release would fold in a different artefact: the driver needs one
-- cycle to park SCLK at CPOL once it leaves reset, so a correct checker legitimately
-- reports one offending cycle there. That is the same settling artefact Chapter 16.4
-- bracketed, and mixing it in would make the reset trap look one count smaller.
-- Reset is asserted FIRST and the baseline is taken after it has settled, so the
-- measured interval is exactly the reset interval. Baselining before the assert would
-- fold in the cycles where the pins are still uninitialised -- and would make the
-- reset-guarded variant's delta non-zero for a reason that has nothing to do with
-- reset guarding.
-- `rst_n` starts high and falls after a clock edge, so the reset is a real EDGE. Driving
-- it low in the same time step as its declaration initialiser leaves the negedge
-- unobserved in one of the three languages -- the counters then start undefined, the
-- whole run propagates it, and the bench hangs waiting for a handshake that never
-- resolves.
rst_n <= '1';
idle_n(1);
rst_n <= '0';
idle_n(2);
b := c;
idle_n(6);
reset_hits := c.t3_no_reset_guard - b.t3_no_reset_guard;
report " measured WHILE reset is asserted, when the pins mean nothing:";
report " T1 correct (reset-guarded) ..... " & integer'image(c.t1_correct - b.t1_correct);
report " T3 no reset guard .............. " & integer'image(reset_hits);
if reset_hits = 0 then
report " FAIL: the unguarded variant counted nothing during reset, so this run cannot demonstrate the reset trap";
errors <= errors + 1;
wait for 1 ns;
end if;
if (c.t1_correct - b.t1_correct) /= 0 then
report " FAIL: the reset-guarded variant counted during reset";
errors <= errors + 1;
wait for 1 ns;
end if;
rst_n <= '1';
idle_n(6);
-- ==============================================================
-- S1 -- legal traffic.
-- ==============================================================
sel_bench <= false;
b := c;
run_burst(3);
s1 := delta(c, b);
-- ==============================================================
-- S2 -- the fault, with SCLK moving inside the window.
-- ==============================================================
sel_bench <= true;
b_cs_n <= '1';
b_sclk <= CPOL;
idle_n(4);
b := c;
b_sclk <= not CPOL; idle_n(2);
b_sclk <= CPOL; idle_n(1);
b_sclk <= not CPOL; idle_n(2);
b_sclk <= CPOL;
idle_n(6);
s2 := delta(c, b);
-- ==============================================================
-- S3 -- the fault, with SCLK still.
-- ==============================================================
idle_n(4);
-- AND FIRST, THE CLEAR THAT DOES NOT ARRIVE. `clr` is pulsed here with SCLK idle. Four
-- of the five variants zero immediately; the SCLK-clocked one does not, because its
-- clear is inside a process clocked on SCLK. Measured rather than described.
clr_t2_before := c.t2_sclk_clocked + c.t2_evals;
clear_counts;
clr_t2_after := c.t2_sclk_clocked + c.t2_evals;
b := c;
b_sclk <= not CPOL; -- a FALLING edge into the offence
idle_n(WINDOW);
b_sclk <= CPOL; -- a RISING edge out of it
idle_n(6);
s3 := delta(c, b);
-- ==============================================================
-- The table.
-- ==============================================================
report " variant S1 legal S2 fault, SCLK moving S3 fault, SCLK still";
report " T1 correct " & integer'image(s1.t1_correct) & " " &
integer'image(s2.t1_correct) & " " & integer'image(s3.t1_correct);
report " T2 clocked on SCLK " & integer'image(s1.t2_sclk_clocked) & " " &
integer'image(s2.t2_sclk_clocked) & " " & integer'image(s3.t2_sclk_clocked);
report " T3 no reset guard " & integer'image(s1.t3_no_reset_guard) & " " &
integer'image(s2.t3_no_reset_guard) & " " & integer'image(s3.t3_no_reset_guard);
report " T4 disable iff overlaps " & integer'image(s1.t4_disable_overlaps) & " " &
integer'image(s2.t4_disable_overlaps) & " " & integer'image(s3.t4_disable_overlaps);
report " T5 edge-reported " & integer'image(s1.t5_edge_reported) & " " &
integer'image(s2.t5_edge_reported) & " " & integer'image(s3.t5_edge_reported);
report " and the EVALUATION counts over S3: T1 evaluated " &
integer'image(s3.t1_evals) & " times, T2 evaluated " &
integer'image(s3.t2_evals);
report " the clear pulsed with SCLK idle: T2's counters went from " &
integer'image(clr_t2_before) & " to " & integer'image(clr_t2_after);
if clr_t2_before /= clr_t2_after then
report " FAIL: the SCLK-clocked variant's counters DID clear with SCLK idle, so this run cannot demonstrate that its clear depends on the design's clock";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 0. before any of that: a clear pulsed while SCLK was idle left the SCLK-clocked variant's counters untouched, because its clear lives inside a process clocked on SCLK. A checker whose clock the DESIGN controls is a checker the TESTBENCH cannot reset either -- so every measurement below is a delta";
if s1.t1_correct /= 0 or s1.t2_sclk_clocked /= 0 or s1.t3_no_reset_guard /= 0
or s1.t4_disable_overlaps /= 0 or s1.t5_edge_reported /= 0 then
report " FAIL: a variant fired on legal traffic";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 1. on legal traffic all five variants report zero, which is exactly the problem: five writings of one obligation, four of them defective, and a clean regression cannot tell them apart";
if s2.t1_correct = 0 or s2.t3_no_reset_guard = 0 or s2.t5_edge_reported = 0 then
report " FAIL: a working variant missed the fault with SCLK moving";
errors <= errors + 1;
wait for 1 ns;
end if;
if s2.t5_edge_reported >= s2.t1_correct then
report " FAIL: the edge-reported variant did not report FEWER times than the per-cycle one";
errors <= errors + 1;
wait for 1 ns;
end if;
if s2.t2_sclk_clocked /= 0 then
report " FAIL: the SCLK-clocked variant reported with SCLK moving; every clock edge it gets arrives at a compliant instant, so it should be unable to report anything";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 2. with SCLK MOVING in the window -- so the SCLK-clocked variant does get clock edges -- T1 reported " &
integer'image(s2.t1_correct) & " offending cycles, T5 reported " &
integer'image(s2.t5_edge_reported) & " offences, and T2 still reported " &
integer'image(s2.t2_sclk_clocked) &
". More clock does not help it: a process clocked on rising SCLK is evaluated only at instants where SCLK is '1', and with CPOL = '1' the obligation at every one of those instants is already satisfied. The property is not under-exercised, it is UNFALSIFIABLE -- a checker clocked on the signal it checks can only ever observe that signal in one state";
if s3.t1_correct = 0 then
report " FAIL: the correct variant missed the fault with SCLK still";
errors <= errors + 1;
wait for 1 ns;
end if;
if s3.t2_sclk_clocked /= 0 then
report " FAIL: the SCLK-clocked variant reported with SCLK still";
errors <= errors + 1;
wait for 1 ns;
end if;
if s3.t2_evals >= s3.t1_evals then
report " FAIL: the SCLK-clocked variant was evaluated as often as the correct one; the point of this stimulus is that it is evaluated far less often";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 3. with SCLK STILL, the correct variant reported " &
integer'image(s3.t1_correct) &
" offending cycles and the SCLK-clocked one reported ZERO -- and its evaluation counter says why: it was evaluated " &
integer'image(s3.t2_evals) & " times against the correct variant's " &
integer'image(s3.t1_evals) &
". A checker clocked on the protocol's own clock has no clock during the interval an idle-time obligation is about";
if s1.t4_disable_overlaps /= 0 or s2.t4_disable_overlaps /= 0
or s3.t4_disable_overlaps /= 0 then
report " FAIL: the overlapping-disable variant reported something; it is supposed to be structurally incapable of reporting";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 4. the overlapping-disable variant reported ZERO on all three stimuli, including both faults. Its disable condition IS its antecedent, so there is nothing it could ever report -- and in a suite's output it is indistinguishable from the correct variant. Somebody adds a `disable iff` to silence noise like T3's, and the property it lands on stops existing";
wait for 1 ns;
if errors = 0 then
report "PASS: one obligation -- while deselected, SCLK sits at CPOL -- written five ways, and on legal traffic all five report zero, which is precisely why four of them survive review. With the fault present and SCLK MOVING in the window, so the SCLK-clocked variant does receive clock edges, the correct variant reported " &
integer'image(s2.t1_correct) & " offending cycles, the edge-reported variant " &
integer'image(s2.t5_edge_reported) & " offences, and the SCLK-clocked variant " &
integer'image(s2.t2_sclk_clocked) &
". More clock does not rescue it: a process clocked on rising SCLK is evaluated only at instants where SCLK is '1', and with CPOL = '1' the obligation is satisfied at every one of those instants, so the property is UNFALSIFIABLE rather than merely under-exercised -- a checker clocked on the signal it checks can only ever observe that signal in one state. With the fault present and SCLK STILL, which is what a master does after its mode register is reprogrammed and before its next transfer and is the exact fault Chapter 16.4 found in its own driver, the correct variant reported " &
integer'image(s3.t1_correct) & " and the SCLK-clocked one ZERO, evaluated " &
integer'image(s3.t2_evals) & " times against " & integer'image(s3.t1_evals) &
". The unguarded variant fired " & integer'image(reset_hits) &
" times while reset was asserted and the pins meant nothing, and the usual fix for that noise is the fifth variant: a `disable iff` whose condition is exactly the antecedent, which reported ZERO on every stimulus including both faults and is indistinguishable in any report from the one that works. A clear pulsed with SCLK idle did not even reach the SCLK-clocked variant's counters, so a checker whose clock the design controls is one the testbench cannot reset either. The instrument that separates all five is not the failure count -- it is the EVALUATION count, which is what Chapter 16.1 called `exercised` and Chapter 17.1 called `attempts`"
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;6. The Same Five Writings As SVA
Reviewed code — Icarus implements no SVA, per Chapter 16.3's toolchain note. Read them as a diff: the differences are one clock expression, one disable iff, and one $rose.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// T1 -- CORRECT. The observer's clock, a reset guard that names RESET and nothing else, and one
// report per offending cycle.
property p_idle_correct;
@(posedge clk) disable iff (!rst_n)
cs_n |-> (sclk == cpol);
endproperty
a_t1: assert property (p_idle_correct);
// T2 -- CLOCKED ON SCLK. The clock expression is the only difference from T1, and it makes the
// property UNFALSIFIABLE: `@(posedge sclk)` samples sclk only where sclk is 1, so with CPOL = 1
// the consequent holds at every evaluation instant by construction. It is also evaluated not at
// all while SCLK is idle, which is the whole interval the obligation is about.
property p_idle_sclk_clocked;
@(posedge sclk) disable iff (!rst_n)
cs_n |-> (sclk == cpol);
endproperty
a_t2: assert property (p_idle_sclk_clocked);
// T3 -- NO RESET GUARD. Correct once the design is running, and it fires throughout reset when
// the pins mean nothing.
property p_idle_unguarded;
@(posedge clk) cs_n |-> (sclk == cpol);
endproperty
a_t3: assert property (p_idle_unguarded);
// T4 -- THE DISABLE THAT OVERLAPS THE ANTECEDENT. Added to silence T3's reset noise, because the
// failing cycles all have the select high. The condition is exactly the antecedent, so the
// property reports nothing on any stimulus and is indistinguishable from T1 in any report.
//
// The general rule this violates: a `disable iff` condition must be ORTHOGONAL to the
// antecedent. Reset is orthogonal to the select. The select is not.
property p_idle_disabled;
@(posedge clk) disable iff (cs_n)
cs_n |-> (sclk == cpol);
endproperty
a_t4: assert property (p_idle_disabled);
// T5 -- EDGE-REPORTED. Correct, and it answers a different question: how many times did the bus
// go wrong, rather than for how many cycles was it wrong.
property p_idle_edge_reported;
@(posedge clk) disable iff (!rst_n)
$rose(cs_n && (sclk != cpol)) |-> 1'b0;
endproperty
a_t5: assert property (p_idle_edge_reported);
// AND THE COVER THAT DISTINGUISHES ALL FIVE, which is the point of the chapter. A failure count
// cannot tell a working property from T2 or T4; an evaluation count can, and `cover property` on
// the antecedent is how an assertion language spells it.
c_t1_ante: cover property (@(posedge clk) disable iff (!rst_n) cs_n);
c_t2_ante: cover property (@(posedge sclk) disable iff (!rst_n) cs_n); // will be tiny
c_t4_ante: cover property (@(posedge clk) disable iff (cs_n) cs_n); // will be ZEROc_t4_ante is the whole diagnosis in one line: an antecedent cover that can never fire, because the disable and the antecedent are the same condition. A signoff step that reads antecedent covers finds T4 in seconds; one that reads failure counts never finds it at all.
7. Why a Verification Engineer Cares
Because two of these five defects produce a permanently silent checker, and neither is visible in a failure count.
The instrument is the same one Chapter 16.1 built for rules and Chapter 17.1 built for attempts: count evaluations, not just failures. T2 and T4 are both caught in one line by an antecedent cover, and neither is caught by anything else.
The second habit is a rule about disable iff that is easy to state and almost never written down: the disable condition must be orthogonal to the antecedent. Reset is orthogonal to a chip select. A chip select is not. Every guard added to silence noise is a candidate for this check, and the noise is usually real — T3's reset firing is a genuine problem with a genuine fix, and the fix that gets applied is the one that deletes the property.
And a rule about clocks: a checker's clock is a property of the observer, not of the protocol. Choosing the protocol's clock feels protocol-aware and costs you the intervals in which the protocol's clock is not running — which for SPI is most of the time, and for the idle-level obligation is all of the time.
8. Why an FPGA or ASIC Engineer Cares
Because the obligation in this chapter is the one your slave device cares about most, and the fault it forbids is the one that comes out of a mode change.
SCLK parked at the wrong level while deselected is what a master produces between reprogramming its mode register and starting its next transfer. Some slaves tolerate it; some interpret the transition into it as an edge and shift a bit. Chapter 16.4 found exactly that fault in its own driver, and the checker that caught it was clocked on the observer's clock. A checker clocked on SCLK would have found nothing, forever, while looking like the most protocol-aware check in the file.
9. Failure Signature — A Checker That Cannot Be Made To Fire
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
Symptom a fault is injected that the checker exists for. It does not
fire. Legal traffic is clean, every other checker behaves,
and the fault is definitely present in the waveform.
What happened one of two things, and they need different fixes: the
checker's clock does not run during the interval the
obligation covers, or its `disable iff` condition overlaps
its antecedent.
What would have an evaluation count per checker. The first case shows a
caught it small number; the second shows ZERO, and zero is
unambiguous.
The tell ask whether the checker CAN fail, not whether it did.
A checker clocked on the signal it checks observes that
signal in one state only -- which for a level obligation
means the obligation is satisfied at every evaluation
instant by construction.10. Common Misconceptions
"Check the protocol on the protocol's clock." The protocol's clock stops. Worse, a checker clocked on a signal samples that signal in one state only, so a level obligation on that same signal cannot fail. The clock belongs to the observer.
"All five variants report zero on legal traffic, so they are equivalent." They are indistinguishable, which is different. Four of them are defective and the clean column is exactly why they survive review.
"disable iff scopes a property to when it matters." It does when the condition is orthogonal to the antecedent. When it overlaps, the property stops existing and reports nothing on any stimulus — including the faults it was written for.
"A noisy checker is worse than a quiet one." A checker firing during reset is visible and fixable. A checker that has been silenced is invisible. The noisy one is a better state to be in, and the fix for the noise must not be a condition that overlaps the antecedent.
"Reporting once per offence rather than per cycle is a correctness issue." It is a reporting choice between two different questions — for how many cycles was the bus wrong, and how many times did it go wrong. Both are correct, and it is the argument people have while the silent variant sits in the same file.
"The bench can always reset a checker between phases." Not one clocked on a signal the design controls. A clear pulsed while SCLK was idle never reached T2's counters at all, which is why every measurement here is a delta.
11. Reason It Through
S2 gives the SCLK-clocked variant clock edges and it still reports nothing. Explain why, without referring to SCLK stopping.
Its evaluation instants are the rising edges of SCLK, and at a rising edge SCLK is 1. With CPOL = 1 the obligation is SCLK must be 1, so every instant at which the property is evaluated is one where it already holds. The property is unfalsifiable rather than under-exercised, and no amount of extra stimulus changes it.
T4 and T1 produce identical output on every stimulus in this chapter. Name the one measurement that separates them and say why it works.
The evaluation count — or in SVA, a cover property on the antecedent. T4's disable condition is its antecedent, so the antecedent cover can never fire and reads exactly zero. Failure counts cannot separate them because neither fails.
Why is T3's defect less dangerous than T4's, and how does one become the other?
T3 fires during reset, which is visible and prompts a fix. T4 fires never, which is invisible. The transition happens when somebody silences T3's noise with a guard built from the condition the failing cycles have in common — the select being high — which is the antecedent.
The VHDL version initially reported different numbers from the SystemVerilog one. What was the cause, and what is the general form of the lesson?
bad <= (sclk /= cpol) as a concurrent signal assignment is one delta stale inside a clocked process, so the SCLK-clocked variant evaluated the pre-edge SCLK — the opposite level to the one its own edge had just established. The general form: where a derived event is computed decides which instant the property is about, which is the same lesson as the pre-edge sampling copy in Chapter 16.3.
State the disable iff rule this chapter implies, in one sentence.
Every term of a disable condition must be orthogonal to every antecedent in the property set it guards — reset is orthogonal to a chip select, and a chip select is not orthogonal to a property about the chip select.
12. Understanding Check
13. Summary
One obligation — while deselected, SCLK sits at CPOL — written five ways, and on legal traffic all five report zero, which is precisely why four of them survive review. With the fault present and SCLK moving in the window, so the SCLK-clocked variant does receive clock edges, the correct variant reported 4 offending cycles, the edge-reported variant 2 offences, and the SCLK-clocked variant 0: more clock does not rescue it, because a block clocked on posedge sclk is evaluated only where SCLK is 1 and with CPOL = 1 the obligation holds at every one of those instants. The property is unfalsifiable rather than under-exercised. With SCLK still — what a master produces between reprogramming its mode register and its next transfer, and the exact fault Chapter 16.4 found in its own driver — the correct variant reported 6 and the SCLK-clocked one 0, evaluated once against twelve. The unguarded variant fired 6 times during reset, and the usual fix for that noise is the fifth variant: a disable iff whose condition is exactly the antecedent, which reported zero on every stimulus including both faults and is indistinguishable in any report from the one that works. The instrument that separates all five is not the failure count. It is the evaluation count — what Chapter 16.1 called exercised and Chapter 17.1 called attempts.
14. What Comes Next
The checks are sound. Chapter 17.3 turns to what the stimulus reached, and measures a coverage number that can never read full alongside one that can.
Continue learning
Related tutorials
- Related topic
SPI Protocol Assertions
A property attempt has four outcomes, not two, and the two that are not failures are where a suite's silence comes from. Seven SPI properties measured for passes, vacuous evaluations and attempts still open at the end of the test, with the same six obligations run a second time as PSL assertions by a real assertion engine.
- Related topic
From Protocol to Design Requirements
Turning a device transaction specification into RTL requirements a simulator can disagree with: why every requirement needs an independent violation, why measured intervals beat asserted ones, and the six properties an SPI master must satisfy.
- Related topic
UCIe Assertions
Writing SVA that describes UCIe architectural contracts rather than implementation details — triggers that mean the right event, reset and disable scoping that does not sleep through the bug, overlapping transactions that outgrow local variables, liveness with its assumptions written down, and the four wrong properties that pass a regression while checking nothing.
- Related topic
Assertions — Executable Statements About Ownership Over Time
A PCIe assertion is not a syntax exercise. It is a claim about who owns an item, what must stay true while they own it, and which event transfers it — and the hardest part is proving the assertion was ever reached.