I²C · Module 22
Asserting Clock-Stretching, Arbitration and Bus-Idle Behavior
The behaviours where two devices legitimately drive one line, a property that fired 84 times on legal traffic until its threshold was measured rather than guessed, and the temporal shape a restricted assertion language pushes back into ordinary logic.
Clock stretching and arbitration share one awkward feature: in both, two devices drive the same line at the same time, legitimately. Every other rule on this bus is about one device doing something wrong. These are about several devices doing something right, and a property that does not know the difference fires constantly.
1. Stretching Is Two Devices Pulling SCL, and It Is Correct
A target that needs time holds SCL low after the acknowledge. The controller has already released it, so during a stretch both the controller's and the target's drive intents are low — one because it is waiting, one because it is stalling.
Test A3 drives exactly that against Module 18's target:
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");The property about SCL contention therefore cannot be "never two SCL drivers". It has to be narrower:
-- psl NO_SCL_CONFLICT_WHEN_HIGH : assert never (scl_holders > 1 and scl = '1')
-- report "22.5 SCL reads high while more than one device pulls it";Two devices pulling while the line reads low is a stretch. Two devices pulling while the line reads high is impossible on a wired-AND bus and means a modelling fault — a drive intent that is not taking effect, which is worth catching because it silently invalidates every contention result that depends on it.
2. The Property That Fired on Every Legal Byte
The SDA version of the same rule went wrong, and the way it went wrong is the chapter's main lesson.
The first formulation was the obvious one:
-- psl ONE_SDA_DRIVER : assert never (sda_holders > 1);It fired 84 times across three legal transfers.
And there is a sharper version of the finding underneath it. The first debugging instinct was that the property was too strict. It was — but the bench was also wrong:
-- before
wait until falling_edge(clk); m_scl_low <= '1'; phase;
wait until falling_edge(clk); m_sda_low <= '0'; phase; -- released HERE
-- after: released on the same edge that pulls SCL low
wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;A correct controller releases SDA at the same edge it takes SCL low. The bench held it for an extra half period on every byte, so the target's acknowledge overlapped it every time. Fixing the bench dropped the firing count from 84 to 27 — and only then was the residual overlap the genuine, unavoidable handover.
The property was right and the stimulus was wrong, which is the more common direction than people expect, and it is worth checking before relaxing anything.
3. The Rule With No Bus-Level Formulation
Both properties above read scl_holders and sda_holders — counts of how many devices are pulling each line. Those are not derivable from the bus.
Low is low. The wired-AND of one puller and two is bit-identical, so no amount of monitoring the resolved lines can reveal a second driver. The bus model exports the count precisely because this rule cannot otherwise be asked, and 22.1 notes that this is what keeps the rule on the assertion side of the line at all — with only the resolved line available it would be uncheckable by any mechanism.
4. Where the Temporal Shape Had to Go
"Two devices for more than N consecutive cycles" is a temporal statement, and the natural way to write it is a repetition inside the directive:
-- psl ONE_SDA_DRIVER : assert never {(sda_holders > 1)[*20]};5. Liveness, and the One Property That Reports a Hang
-- psl EVERY_TRANSFER_ENDS : assert always (
-- (start_now = '1') -> eventually! (active = '0'))
-- report "22.5 a transfer opened and never closed";eventually! is a strong operator: if the condition never holds, it fails at the end of simulation rather than never being evaluated. That makes it the only property in the set that reports a hang rather than a wrong value — a bus wedged by a device that never releases a line produces no illegal edge and no wrong data, so every other property here is silent on it.
The probe confirms eventually! is evaluated and fires when its condition is never satisfied, which matters because a strong operator that is quietly ignored would turn the module's only liveness check into decoration.
6. What This Environment Cannot Assert About Arbitration
Eighty-four violations on traffic that was entirely legal
Pitfall — a contention property with no tolerance for a handover
// The rule reads "only one device may drive the acknowledge slot", so:
//
// -- psl ONE_SDA_DRIVER : assert never (sda_holders > 1)
// -- report "more than one device is pulling SDA";
//
// It fires 84 times across three ordinary, legal transfers.
//
// Because at EVERY acknowledge slot the outgoing driver releases SDA and the
// incoming one starts pulling it, and those are not simultaneous. For a short
// interval both drive intents are low. The wired-AND is unharmed -- low is low --
// and the transfer is completely correct.
//
// The property is not stricter than the rule. It contradicts the protocol, and a
// property that fires on every byte of good traffic will be waived within a day.A rule stated for a single moment becomes wrong when the hardware's correct behaviour spans moments, and on a wired-AND bus a driver handover necessarily does. The instinct to relax the property was right, but checking the stimulus first turned out to matter more — most of the firing was a real bench defect, and only the remainder was the unavoidable handover. Measuring the residual rather than guessing is what makes the final threshold defensible, and naming the resulting weakness is what stops the property being trusted for more than it does.
// TWO fixes, and the first one is the one nobody looks for.
//
// 1. THE BENCH WAS ALSO WRONG. It released SDA half a period after taking SCL
// low, where a real controller releases both on the same edge:
//
// -- before
// wait until falling_edge(clk); m_scl_low <= '1'; phase;
// wait until falling_edge(clk); m_sda_low <= '0'; phase;
// -- after
// wait until falling_edge(clk); m_scl_low <= '1'; m_sda_low <= '0'; phase;
//
// That alone dropped the firing count from 84 to 27. The property had been
// reporting a real -- if harmless -- defect in the stimulus.
//
// 2. MEASURE the residual overlap rather than guessing a threshold. Against the
// real target the genuine handover runs to about six cycles, so the tolerance
// has to exceed a whole bit period to be unambiguous:
//
// if sda_holders > 1 then sda_overlap <= sda_overlap + 1;
// else sda_overlap <= 0; end if;
//
// -- psl ONE_SDA_DRIVER : assert never (sda_overlap >= OVERLAP_CLKS)
// -- report "more than one device pulled SDA for a sustained interval";
//
// The result is SOUND AND WEAK, and saying so is part of the deliverable: it
// catches a line held across a bit boundary and cannot catch a short illegal
// overlap. Catching that needs to know who OWNS the slot, which is protocol state
// rather than a count -- so it is a scoreboard question.Pitfall — a stretch reported as a bus fault
// A property written to catch two devices fighting over the clock:
//
// -- psl NO_SCL_CONFLICT : assert never (scl_holders > 1)
// -- report "more than one device is pulling SCL";
//
// It fires on every clock stretch -- which is to say, on the feature the target
// is SUPPOSED to have.
//
// During a stretch the controller has released SCL and is waiting for it to rise,
// while the target holds it low. Both drive intents are asserted. That is not a
// conflict; it is the mechanism by which stretching works, and a controller that
// did not release would not be honouring the stretch at all.
//
// So the property fires on correct behaviour, gets waived, and stops catching the
// case it was written for.Clock stretching is defined by two devices driving the same line, so a property forbidding that forbids the feature. Narrowing it to the case that is physically impossible keeps a real check — a drive intent not taking effect — while permitting the legal overlap. Pairing it with a cover point closes the remaining gap: a quiet property plus a zero-hit cover point means the situation never occurred, which is a different result from the property holding.
// Ask what a CONFLICT would look like that a stretch does not:
//
// -- psl NO_SCL_CONFLICT_WHEN_HIGH : assert never (scl_holders > 1 and scl = '1')
// -- report "SCL reads high while more than one device pulls it";
//
// Two devices pulling while the line reads LOW is a stretch, and legal.
// Two devices pulling while the line reads HIGH is IMPOSSIBLE on a wired-AND bus,
// so it means a drive intent is not taking effect -- a modelling fault that
// silently invalidates every contention result depending on it.
//
// AND PROVE THE STRETCH CASE IS EXERCISED, or the property is only known to be
// quiet because nothing ever stretched:
//
// stall_req <= '1'; -- ask the REAL target to stretch
// b_start;
// b_put(ADDR & '0', ackbit);
// stall_req <= '0';
// ...
// expect_quiet("A3 legal stretch");
//
// -- and a cover point, so an unexercised run is visible rather than assumed:
// -- psl COV_STRETCH : cover {scl_holders > 1};
//
// The cover point reports 6 hits on this bench. A run reporting 0 would mean the
// property stayed quiet because the situation never arose.7. What 22.5 Settled
Stretching and arbitration are the cases where simultaneous driving is correct, so properties about them must permit what every other rule forbids.
Narrow the property to what is actually impossible. Two SCL drivers while the line reads high cannot happen on a wired-AND bus; two while it reads low is a stretch.
Measure the legal overlap before setting a threshold — and check the stimulus first, because most of the firing here was a bench defect rather than the protocol.
Name the weakness the threshold buys. Sound and weak is an acceptable property; sound and weak described as strict is not.
A restricted assertion language pushes temporal shape into ordinary logic, where the property engine no longer checks it.
Arbitration itself is not asserted here, because this environment cannot produce a contended bus, and that stays on the uncovered list rather than being implied.
Next: what was actually exercised, which neither assertions nor scoreboards answer — and a cover form this toolchain accepts that never matches. Chapter 22.6 — A Functional Coverage Model for I²C.
Continue learning
Related tutorials
- Related topic
I²C Transaction Atomicity and Bus Ownership Across Phases
What is and is not atomic on an I²C bus, stated precisely. Three things end bus ownership and one that looks like it should does not — and telling them apart needs one input the wire cannot supply.
- Related topic
Bus Feedback — Clock Stretching and Arbitration From One Comparison
Clock stretching and arbitration loss are not two features. They are one comparison — a line this master released that reads back low — applied to two wires, differing only in a timing qualifier and an intent gate. Builds both from a single comparator and shows why a master can only ever lose by trying to send a one.
- Related topic
Verifying Stretching and Arbitration Without Flaky Tests
A feature that was implemented, correct and never executed; how to place a behaviour instead of hoping for it; and why a test whose checks pass whether or not the case occurred is flaky even when it is green every time.
- Related topic
Clock-Stretching and Arbitration Failures in the Field
Why a timeout is the least informative evidence an I²C controller produces, and what to record instead. Six situations that all report the same timeout, a classifier that separates them, and the one failure in the set that never times out at all — a controller that does not honour stretching, corrupting data silently and blaming the target.