I²C · Module 22
Asserting Legal START, Repeated START and STOP
Framing legality as executed properties, the bus-free interval, and a negative test that could not violate the rule it targeted because it was assembled from the procedures that obey it — found by latching the antecedent at the moment of judgement.
Framing is where I²C's rules are most easily stated and most easily mis-asserted. A START is an SDA fall while SCL is high; a STOP is an SDA rise while SCL is high; a repeated START is a START with a transfer already open. Three sentences.
The properties that follow from them are not three sentences, because each one has a precondition that the bus does not carry.
1. A STOP Requires an Open Transfer
-- psl STOP_NEEDS_OPEN_TRANSFER : assert always (
-- (stop_now = '1' and active = '0') -> false)
-- report "22.3 a STOP arrived with no transfer open";A STOP on an idle bus is not a harmless no-op. It means some device produced an SDA rise while SCL was high without a transfer in progress — which is either a device that has lost track of the framing, or noise that every other device will also interpret as a STOP.
The precondition is active, and active is not on the bus. It is derived by the tracker described in 22.2 §4, which is the recurring cost of framing properties: the interesting ones are all conditional on state that has to be reconstructed.
2. A START Needs a Bus-Free Interval
-- psl START_AFTER_BUS_FREE : assert always (
-- (start_now = '1' and active = '0' and idle_cnt < BUS_FREE_CLKS) -> false)
-- report "22.3 a START arrived before the bus-free interval elapsed";After a STOP the bus must stay idle for a minimum time before a new START — tBUF in the specification — so that every device sees the bus released and can arbitrate fairly for it.
3. The Scenario That Could Not Violate Its Own Rule
This is the most useful thing in the chapter, and it was not planned.
The first version of the bus-free test was the obvious one — do a transfer, stop, and immediately start again:
b_start;
b_put(ADDRV & '0', ackbit);
b_stop;
b_start; -- "no bus-free interval at all"
b_stop;The property did not fire, and the natural conclusion is that the property is broken.
It was not. The diagnostic that settled it was a counter inside the property entity, latching the bus-free count at the moment of each START rather than reading it twenty cycles later:
B3 diag: starts = 2, early = 0, idle_cnt at the last START = 17The general shape is worth naming because it recurs: a negative test assembled from the environment's ordinary building blocks tends to inherit their correctness. The building blocks exist to obey the protocol, so a violation built out of them is usually not a violation at all — and the resulting silence is blamed on the property.
4. Counting the Antecedent Separately
The diagnostic that made this findable is worth generalising. The property entity exports two counters per rule: how many times the event occurred, and how many of those were violations.
if start_now = '1' then
c_starts <= c_starts + 1;
last_start_idle <= idle_cnt;
if active = '0' and idle_cnt < BUS_FREE_CLKS then
c_start_early <= c_start_early + 1;
end if;
end if;Without the event counter, a silent property has two indistinguishable explanations: the situation never arose, or it arose and the property failed to notice. With it, starts = 2, early = 0 says immediately that the STARTs happened and were judged legal — which points at the scenario rather than at the property, and that is a different afternoon's work.
5. The Bench
-- ---------------------------------------------------------------------------
-- i2c_assert_tb.vhd
-- The property set against Module 18's real target, and a scenario per property
-- that makes it FIRE.
--
-- EVIDENCE: SIMULATED -- NVC 1.23, analysed with `--psl`.
--
-- THE WHOLE POINT OF THIS FILE IS THE SECOND HALF. Running a legal transfer and seeing
-- no assertion fire establishes almost nothing: an assertion whose antecedent is never
-- true is silent, and silence is exactly what a passing suite looks like. The probe in
-- `probe/capability.sh` makes this concrete rather than theoretical -- it found three
-- constructs NVC accepts and never evaluates, so a property written with `rose(scl)`
-- would pass forever while checking nothing.
--
-- So: PHASE A drives legal traffic and every property must stay quiet. PHASE B drives
-- one deliberate violation per property and that property must fire. A property with no
-- Phase B scenario is a property nobody has seen work.
-- ---------------------------------------------------------------------------
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use std.env.finish;
entity i2c_assert_tb is end entity i2c_assert_tb;
architecture tb of i2c_assert_tb is
constant HALFP : integer := 8; -- sampling clocks per half bit period
constant ADDRV : std_logic_vector(6 downto 0) := "1010000"; -- 0x50
constant NREG : integer := 8;
constant FREE : natural := 8; -- bus-free clocks a START needs
signal clk : std_logic := '0';
signal rst_n : std_logic := '0';
signal halt : boolean := false;
-- device 0 = the bench acting as controller, device 1 = the DUT
signal m_scl_low, m_sda_low : std_logic := '0';
signal d_scl_low, d_sda_low : std_logic;
signal scl_drv, sda_drv : std_logic_vector(2 downto 0);
signal scl, sda : std_logic;
signal scl_in, sda_in : std_logic_vector(2 downto 0);
signal scl_rbl, sda_rbl : std_logic_vector(2 downto 0);
signal scl_holders, sda_holders : unsigned(7 downto 0);
signal stall_req : std_logic := '0';
signal dut_regs : std_logic_vector(8*NREG-1 downto 0);
signal dut_pointer : std_logic_vector(7 downto 0);
signal dut_selected, dut_stretching : std_logic;
signal dut_phases, dut_restarts, dut_writes : unsigned(15 downto 0);
signal dut_refused, dut_reads, dut_aborts, dut_conflict : unsigned(15 downto 0);
-- a SECOND puller on SDA, used only by the Phase B scenario for the
-- one-driver-per-slot property. Idle for every other test.
signal x_sda_low : std_logic := '0';
signal n_fired : natural;
signal p_active, p_in_byte : std_logic;
signal p_bitcnt, p_idle : natural;
signal p_starts, p_stops, p_stop_mid, p_start_early : natural;
signal p_last_start_idle : natural;
signal errors : integer := 0;
begin
-- THREE separate devices, and the third one matters. The first version OR-ed the
-- extra puller into the bench's own drive bit, which meant there was never a second
-- device at all -- the holder count stayed at one and the property it was meant to
-- violate could not fire. A contention test whose two contenders share a drive bit
-- is not a contention test.
scl_drv <= '0' & d_scl_low & m_scl_low;
sda_drv <= x_sda_low & d_sda_low & m_sda_low;
clk_gen : process is
begin
while not halt loop
clk <= '0'; wait for 5 ns;
clk <= '1'; wait for 5 ns;
end loop;
wait;
end process clk_gen;
bus_model : entity work.i2c_line_model
generic map (N_DEV => 3)
port map (scl_drive_low => scl_drv, sda_drive_low => sda_drv,
scl => scl, sda => sda, scl_in => scl_in, sda_in => sda_in,
scl_released_but_low => scl_rbl, sda_released_but_low => sda_rbl,
scl_holders => scl_holders, sda_holders => sda_holders);
dut : entity work.i2c_slave
generic map (MY_ADDR => ADDRV, N_REG => NREG, RO_MASK => 4,
IDLE_CYCLES => 200000, SYNC_DEPTH => 2, CNT_W => 16)
port map (clk => clk, rst_n => rst_n,
scl_pin => scl, sda_pin => sda,
scl_drive_low => d_scl_low, sda_drive_low => d_sda_low,
stall_req => stall_req,
reg_flat => dut_regs, pointer => dut_pointer,
selected => dut_selected, stretching => dut_stretching,
n_phases => dut_phases, n_restarts => dut_restarts,
n_writes => dut_writes, n_refused => dut_refused,
n_reads => dut_reads, n_aborts => dut_aborts,
n_sda_conflict => dut_conflict);
-- The properties, bound to the RESOLVED bus and to nothing inside the design.
props : entity work.i2c_props
generic map (BUS_FREE_CLKS => FREE)
port map (clk => clk, rst_n => rst_n, scl => scl, sda => sda,
scl_holders => to_integer(scl_holders),
sda_holders => to_integer(sda_holders),
n_fired => n_fired,
o_active => p_active, o_in_byte => p_in_byte,
o_bitcnt => p_bitcnt, o_idle_cnt => p_idle,
n_starts => p_starts, n_stops => p_stops,
n_stop_mid_byte => p_stop_mid, n_start_early => p_start_early,
o_last_start_idle => p_last_start_idle);
stim : process is
variable ackbit : std_logic;
variable rdbyte : std_logic_vector(7 downto 0);
variable before : natural;
procedure step is
begin
wait until rising_edge(clk);
wait until falling_edge(clk);
end procedure;
procedure phase is
begin
for i in 1 to HALFP loop step; end loop;
end procedure;
procedure do_reset is
begin
wait until falling_edge(clk);
rst_n <= '0'; m_scl_low <= '0'; m_sda_low <= '0';
x_sda_low <= '0'; stall_req <= '0';
step; step; step;
wait until falling_edge(clk);
rst_n <= '1';
-- Long enough for the bus-free interval to elapse, so a legal START at the
-- start of a test does not itself trip START_AFTER_BUS_FREE.
for i in 1 to 40 loop step; end loop;
end procedure;
procedure b_start is
begin
wait until falling_edge(clk); m_sda_low <= '0'; m_scl_low <= '0'; phase;
wait until falling_edge(clk); m_sda_low <= '1'; phase;
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end procedure;
procedure b_restart is
begin
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
wait until falling_edge(clk); m_sda_low <= '1'; phase;
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end procedure;
procedure b_stop is
begin
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '1'; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
wait until falling_edge(clk); m_sda_low <= '0'; phase;
end procedure;
procedure b_bit (b : std_logic) is
begin
wait until falling_edge(clk); m_scl_low <= '1'; phase;
wait until falling_edge(clk); m_sda_low <= not b; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end procedure;
-- Release SDA on the SAME falling edge that pulls SCL low, which is what a
-- correct controller does. The first version released it a half period later, so
-- the bench went on pulling SDA while the target began its acknowledge -- a
-- sustained two-driver overlap on every single byte. The property was right and
-- the BENCH was wrong, which is the more common way round than people expect.
procedure b_ack_slot (a : out std_logic) is
begin
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
for i in 1 to HALFP-2 loop step; end loop;
a := sda;
step; step;
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end procedure;
procedure b_put (d : std_logic_vector(7 downto 0); a : out std_logic) is
begin
for k in 7 downto 0 loop b_bit(d(k)); end loop;
b_ack_slot(a);
end procedure;
-- A deliberate data-valid violation: change SDA in the MIDDLE of a high SCL
-- phase, part way through a byte. No conforming controller does this.
procedure b_bit_with_sda_glitch (b : std_logic) is
begin
wait until falling_edge(clk); m_scl_low <= '1'; phase;
wait until falling_edge(clk); m_sda_low <= not b; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
-- SCL is HIGH here, and we move SDA
wait until falling_edge(clk); m_sda_low <= b; phase;
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end procedure;
-- One byte IN: SDA released for eight slots so the TARGET drives them, then the
-- controller drives the ninth. Test A2 originally appended a bare acknowledge slot
-- instead, which is ONE bit followed by a STOP -- so A2 was itself an illegal trace
-- and the mid-byte property was right to fire on it. When a property fires on
-- "legal" traffic, the first thing to doubt is the claim that it was legal.
procedure b_get (send_ack : std_logic; d : out std_logic_vector(7 downto 0)) is
variable v : std_logic_vector(7 downto 0) := (others => '0');
begin
for k in 7 downto 0 loop
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
for i in 1 to HALFP-2 loop step; end loop;
v(k) := sda;
step; step;
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end loop;
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= send_ack; phase;
wait until falling_edge(clk); m_scl_low <= '0'; phase;
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;
d := v;
end procedure;
-- A STOP immediately followed by a START. Entered with SCL pulled low and SDA
-- released, which is where b_put leaves the bus.
--
-- THE HALF-PERIOD WAITS ARE DELIBERATELY ABSENT between the STOP and the START.
-- Composing the ordinary b_stop and b_start instead -- which is what this test did
-- first -- puts a half period inside each, so the gap measured seventeen cycles and
-- SATISFIED the very rule the scenario existed to break. A scenario meant to
-- violate a timing rule has to be written tighter than the procedures that obey it,
-- and the diagnostic that revealed it was the bus-free counter latched AT the
-- START rather than read twenty cycles later.
procedure b_stop_then_start_immediately is
begin
wait until falling_edge(clk); m_sda_low <= '1'; step; -- SDA low while SCL low
wait until falling_edge(clk); m_scl_low <= '0'; step; -- SCL rises
wait until falling_edge(clk); m_sda_low <= '0'; step; -- STOP
wait until falling_edge(clk); m_sda_low <= '1'; step; -- START, ~2 cycles later
wait until falling_edge(clk); m_scl_low <= '1'; phase;
end procedure;
procedure note (s : string) is
begin
report s severity note;
end procedure;
procedure expect_quiet (what : string) is
begin
if n_fired /= before then
report " FAIL " & what & ": a property fired on LEGAL traffic ("
& integer'image(n_fired - before) & " times)" severity error;
errors <= errors + 1;
end if;
end procedure;
procedure expect_fired (what : string) is
begin
if n_fired = before then
report " FAIL " & what & ": the property did NOT fire on a deliberate violation"
severity error;
errors <= errors + 1;
end if;
end procedure;
begin
report "=== i2c_assert: properties against the real target, and each one made to fire ===";
-- ================================================================
-- PHASE A -- legal traffic. Every property must stay QUIET.
-- Without this half, a suite of properties that fire on everything would
-- look identical to a suite that works.
-- ================================================================
do_reset;
before := n_fired;
b_start;
b_put(ADDRV & '0', ackbit);
b_put(x"01", ackbit);
b_put(x"5A", ackbit);
b_stop;
for i in 1 to 20 loop step; end loop;
note("A1 a legal write: no property fires");
expect_quiet("A1 legal write");
-- a legal write-then-read, joined by a REPEATED START and never releasing the bus
before := n_fired;
b_start;
b_put(ADDRV & '0', ackbit);
b_put(x"01", ackbit);
b_restart;
b_put(ADDRV & '1', ackbit);
b_get('0', rdbyte); -- a whole byte, NACKed to end the read
b_stop;
for i in 1 to 20 loop step; end loop;
note("A2 a legal write-then-read across a repeated START: no property fires");
expect_quiet("A2 legal repeated START");
-- a legal transfer during which the TARGET stretches SCL. Two devices pull SCL
-- at once here, which the SCL conflict property must NOT flag while the line is
-- low -- that is what a stretch is.
before := n_fired;
stall_req <= '1';
b_start;
b_put(ADDRV & '0', ackbit);
stall_req <= '0';
b_put(x"02", ackbit);
b_stop;
for i in 1 to 20 loop step; end loop;
note("A3 a legal clock stretch: no property fires");
expect_quiet("A3 legal stretch");
-- ================================================================
-- PHASE B -- one deliberate violation per property. Each MUST fire.
-- ================================================================
-- B1: SDA moved while SCL was high, mid-byte.
do_reset;
before := n_fired;
b_start;
b_bit('0'); b_bit('1');
b_bit_with_sda_glitch('0');
b_stop;
for i in 1 to 20 loop step; end loop;
note("B1 SDA changed while SCL was high, mid-byte");
expect_fired("B1 SDA_STABLE_WHILE_SCL_HIGH");
-- B2: a STOP with no transfer open. Framing on an idle bus.
do_reset;
before := n_fired;
b_stop;
for i in 1 to 20 loop step; end loop;
note("B2 a STOP arrived with no transfer open");
expect_fired("B2 STOP_NEEDS_OPEN_TRANSFER");
-- B3: a START before the bus-free interval has elapsed. A STOP, then a START
-- immediately, with no idle gap.
do_reset;
before := n_fired;
b_start;
b_put(ADDRV & '0', ackbit);
b_stop_then_start_immediately;
b_stop;
for i in 1 to 20 loop step; end loop;
report " B3 diag: starts = " & integer'image(p_starts)
& ", early = " & integer'image(p_start_early)
& ", idle_cnt at the last START = " & integer'image(p_last_start_idle)
severity note;
note("B3 a START arrived before the bus-free interval elapsed");
expect_fired("B3 START_AFTER_BUS_FREE");
-- B4: a STOP part way through a byte -- a truncated transfer.
do_reset;
before := n_fired;
b_start;
b_put(ADDRV & '0', ackbit);
-- The last bit must leave SDA PULLED LOW. With a '1' the line is already
-- released, so the STOP's release of SDA produces no rising edge, no STOP is
-- framed at all, and the scenario violates nothing while appearing to.
b_bit('1'); b_bit('1'); b_bit('0'); -- three bits, SDA left low, then framing
b_stop;
for i in 1 to 20 loop step; end loop;
report " B4 diag: stops seen = " & integer'image(p_stops)
& ", of which mid-byte = " & integer'image(p_stop_mid) severity note;
note("B4 a STOP arrived mid-byte");
expect_fired("B4 NO_STOP_MID_BYTE");
-- B5: a second device pulls SDA while the bench is already pulling it. Invisible
-- from the resolved line -- low is low -- so this is the property that can only
-- be written against the holder count.
do_reset;
before := n_fired;
wait until falling_edge(clk); m_sda_low <= '1';
for i in 1 to 4 loop step; end loop;
wait until falling_edge(clk); x_sda_low <= '1'; -- now TWO devices pull SDA
-- Held for longer than a whole bit period, because that is what the property is
-- about: an overlap shorter than a handover cannot be distinguished from one.
for i in 1 to 24 loop step; end loop;
wait until falling_edge(clk); x_sda_low <= '0'; m_sda_low <= '0';
for i in 1 to 20 loop step; end loop;
note("B5 two devices pulled SDA at once");
expect_fired("B5 ONE_SDA_DRIVER");
if errors = 0 then
report "=== i2c_assert: ALL CHECKS PASSED ===" severity note;
else
report "=== i2c_assert: " & integer'image(errors) & " CHECK(S) FAILED ==="
severity note;
end if;
halt <= true;
finish;
end process stim;
watchdog : process is
begin
wait for 40 ms;
report " FAIL watchdog: the assertion bench did not finish" severity error;
report "=== i2c_assert: 1 CHECK(S) FAILED ===" severity note;
finish;
end process watchdog;
end architecture tb;6. A Legal Trace That Was Not
One more finding from building this, because it inverts the usual suspicion.
Test A2 drives a write-then-read across a repeated START and asserts that nothing fires. It fired — the mid-byte property of 22.4 reported a truncated transfer.
The property was right. A2 was appending a bare acknowledge slot where it should have read a whole byte, so the trace really was one bit followed by a STOP:
-- before: an acknowledge slot with no byte in front of it
b_put(ADDRV & '1', ackbit);
b_ack_slot(ackbit);
b_stop;
-- after: eight slots released so the target drives, then the ninth
b_put(ADDRV & '1', ackbit);
b_get('0', rdbyte); -- a whole byte, NACKed to end the read
b_stop;The negative test that was too polite to break anything
Pitfall — a violation assembled from procedures that obey the rule
// A test for the bus-free interval, built from the library's framing procedures:
//
// b_start;
// b_put(ADDR & '0', ackbit);
// b_stop;
// b_start; -- "immediately", with no gap
// b_stop;
//
// The property does not fire. The obvious conclusion -- and the wrong one -- is
// that START_AFTER_BUS_FREE is broken.
//
// It is not. b_stop ENDS with a half-period wait and b_start BEGINS with one, so
// the two compose into a full bit period of idle between the STOP and the START.
// The scenario satisfies the rule it was written to break.
//
// Hours go into the property: re-reading the PSL, checking the antecedent, trying
// different operators -- all on a property that was correct the whole time.Reusable stimulus procedures encode protocol-conforming timing, so composing them cannot produce a timing violation — the gap the test was trying to eliminate is built into the procedures themselves. The failure is expensive because silence is attributed to the property rather than the stimulus, and the fix is diagnostic before it is corrective: latch the value the rule was judged against, at the moment of judgement, and the question answers itself.
// FIRST, make the antecedent observable, so the question is answerable in one run:
//
// -- in the property entity
// if start_now = '1' then
// c_starts <= c_starts + 1;
// last_start_idle <= idle_cnt; -- LATCHED at the event
// if active = '0' and idle_cnt < BUS_FREE_CLKS then
// c_start_early <= c_start_early + 1;
// end if;
// end if;
//
// which reports, in the failing run:
//
// B3 diag: starts = 2, early = 0, idle_cnt at the last START = 17
//
// Seventeen. The STARTs happened and were JUDGED LEGAL. That is a statement about
// the scenario, and it takes one line of output instead of an afternoon.
//
// THEN write the violation tighter than the procedures that obey the rule:
//
// procedure b_stop_then_start_immediately is
// begin
// wait until falling_edge(clk); m_sda_low <= '1'; step;
// wait until falling_edge(clk); m_scl_low <= '0'; step;
// wait until falling_edge(clk); m_sda_low <= '0'; step; -- STOP
// wait until falling_edge(clk); m_sda_low <= '1'; step; -- START, 2 cycles later
// wait until falling_edge(clk); m_scl_low <= '1'; phase;
// end procedure;
//
// => idle_cnt at the last START = 1, early = 1.
//
// RULE: a negative test built from the environment's ordinary building blocks
// inherits their correctness. The blocks exist to obey the protocol.Pitfall — relaxing a property to accommodate a malformed test
// Test A2 is supposed to be a legal write-then-read across a repeated START,
// and the mid-byte property fires on it:
//
// b_start;
// b_put(ADDR & '0', ackbit);
// b_put(x"01", ackbit);
// b_restart;
// b_put(ADDR & '1', ackbit);
// b_ack_slot(ackbit); -- "the read data byte"
// b_stop;
//
// => 22.4 a STOP arrived mid-byte, truncating a transfer
//
// The tempting fix is to loosen the property -- add a condition, lower the
// severity, or exclude the last transfer of a test.
//
// That would remove a working check to accommodate a broken test. b_ack_slot
// drives ONE bit slot. It is not a byte. So the trace really is one bit followed
// by a STOP, and the property is describing it correctly.A property firing on supposedly legal traffic is a claim about the traffic first, and relaxing the property is the one response that cannot be undone safely — the check is gone for the real case too. Here the test was driving a single acknowledge slot where a nine-slot byte belonged, so the STOP genuinely arrived mid-byte and the property was the only thing in the environment reporting it correctly.
// Fix the TRACE. A read data byte is eight slots with SDA released so the target
// drives them, then a ninth that the controller drives:
//
// procedure b_get (send_ack : std_logic; d : out std_logic_vector(7 downto 0)) is
// begin
// for k in 7 downto 0 loop
// wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;
// wait until falling_edge(clk); m_scl_low <= '0'; phase;
// for i in 1 to HALFP-2 loop step; end loop;
// v(k) := sda; -- sample mid-high, target driving
// step; step;
// wait until falling_edge(clk); m_scl_low <= '1'; phase;
// end loop;
// wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= send_ack; phase;
// ...
// end procedure;
//
// b_put(ADDR & '1', ackbit);
// b_get('0', rdbyte); -- a whole byte, NACKed to end the read
// b_stop;
//
// => A2 passes, and the mid-byte property is still capable of firing, which B4
// proves on the same run.
//
// THE ORDER OF INVESTIGATION when a property fires on "legal" traffic:
// 1. establish the trace is legal, reading it as a protocol engineer
// 2. only then look at the property
// Doing it the other way round removes checks to make tests pass.7. What 22.3 Settled
Framing properties are conditional on state the bus does not carry, so each one inherits the reliability of a derived tracker.
A cycle count is not a timing parameter. The bus-free property checks that some idle interval elapsed, against a threshold this environment chose, and says nothing about tBUF.
A negative test built from the stimulus library inherits the library's correctness. The bus-free violation had seventeen cycles of idle in it, contributed by the procedures that exist to obey the rule.
Count the event and the violation separately. Without the event counter, a silent property is ambiguous between "never arose" and "arose and was missed".
When a property fires on legal traffic, doubt the traffic first. One of this module's "legal" traces was a single bit followed by a STOP.
Next, byte boundaries — and a tracker that counted the STOP sequence's own clock edge as a data bit. Chapter 22.4 — Asserting ACK Timing and Byte Boundaries.
Continue learning
Related tutorials
- Related topic
Asserting the Data-Valid Rule — SDA Stable While SCL Is High
The central I²C property and its two framing exceptions, plus three PSL constructs this toolchain accepts and never evaluates — a property built on rose() passes forever while checking nothing, and no report distinguishes it from one that held.
- Related topic
The Data-Valid Rule — SDA Stable While SCL Is High
One sentence governs every bit on an I²C bus, and it is derived rather than decreed: the receiver needs a settled value at the instant it looks. What falls out is that an SDA edge while SCL is HIGH cannot be data — which is why the bus reserves it for framing.
- Related topic
Bus Idle and the Framing Primitives
Module 4 proved that an SDA edge while SCL is high cannot be data, and that the bus reserves the pattern. This chapter collects that debt: what an idle bus is, why a shared bus must delimit its own transfers, and why exactly two reserved edges produce exactly three framing events.
- Related topic
The START Condition
START is SDA falling while SCL is high, it is generated only by the controller, and it makes the bus busy. Derive what every device must do in response, then build a detector in three languages and find out why its two guard terms and its reset value are all load-bearing.