Clock Synchronisation and Arbitration
Draw two controllers' clocks merging on SCL, mark the bit where one loses arbitration, say what the loser must do next, and read what the formal lab proves.
- Lesson
- P8.6
- Time
- 40 min
- Runs on
- Your browser
- Check
- 4 questions
Two microcontrollers shared a bus to one EEPROM, each sure it was alone. Once a week both started within a microsecond, and each clocked out its address without reading SDA back. The EEPROM stored a byte neither had sent, and both logs said "write OK".
Read phases and sample points (quarter bit)
- bit 0: columns 1 through 4.
- bit 1: columns 5 through 8.
- bit 2: columns 9 through 12.
- bit 3: columns 13 through 16.
- bit 4: columns 17 through 20.
- bit 5: columns 21 through 24.
- bit 6: columns 25 through 28.
- bit 7: columns 29 through 32.
- SDA sampled at 3, 7, 11, 15, 19, 23, 27, 31.
- Cycle 2
Bit 0 (address bit 6): both send 1. Neither pulls, SDA is high, nobody notices the other.
- Cycle 25
Address bit 0: controller 1 sends 0 and pulls; controller 2 sends 1 and lets go.
- Cycle 27
While SCL is high, controller 2 reads 0 where it sent 1. It has lost: it stops driving SDA for the rest of the byte.
- Cycle 31
The R/W bit is controller 1's alone. The wire carried 0xA0 exactly: no bit was damaged.
Generated and decoded back (the decoder checks SDA equals the AND of both drivers, and the loser never drives again). The bench measures the same drop: other lost after SCL pulse 7.
One Clock from Two
When either controller pulls SCL low, SCL is low, and every controller starts counting its own LOW from that edge. A short LOW lets go but waits; the line rises only when the last one lets go. Then all count HIGH, and the first to finish pulls (§3.1.7).
ctrl (TLOW 1300, THIGH 1200) and other (TLOW 2600, THIGH 1500) both drive SCL during the address byte. 100 ns per column.A low lane of 1 pulls the net down. The pull-up raises it only when every device releases.
- Cycle 2
SCL falls. Both controllers start counting their own LOW time from this edge and both pull.
- Cycle 15
ctrl's 1300 ns are up and it lets go.otherstill pulls, so SCL stays low andctrlwaits. - Cycle 29
otherlets go too and SCL rises: a LOW of 2601 ns,other's. Both now count HIGH. - Cycle 41
ctrlfinishes its HIGH first and pulls: a HIGH of 1209 ns,ctrl's. That fall restarts both LOW counts.
Measured on the bench: SCL LOW 2601 ns, SCL HIGH 1209 ns. The extra ns come from the controllers polling SCL every 10 ns.
Reading SCL back, the rule from P8.5, is what makes this work. A controller that does not read SCL back is not synchronised.
Arbitration, Bit by Bit
Two controllers may START within tHD;STA of each other, and both see one valid START (§3.1.8). While SCL is high each compares SDA with what it sent. The first to send 1 and read 0 has lost and turns off its SDA driver; the winner's transfer goes on unharmed.
On the bench ctrl sends 0x50 and other 0x51: other loses after SCL pulse 7, address bit 0. There is no priority and no arbiter; the lower address wins more often simply because 0 wins.
After the Drop
The loser may keep clocking to the end of the byte in which it lost, no further. It must try again when the bus is free. If it also has a target function it must switch to target mode at once, because the winner may be addressing it (§3.1.8).
Bench switch on other | What it breaks | Measured |
|---|---|---|
| none (correct loser) | nothing: releases SDA at once, retries when the bus is free, becomes a target | ctrl: ack 1 lost 0 | other: ack 0 lost 1 target_mode 1 | broken 0 |
loser_keeps_clocking_past_byte | keeps clocking after the byte; reads the winner's ACK as its own | ctrl: ack 1 lost 0 | other: ack 1 lost 1 target_mode 1 | broken 0, other pulled SCL low 3 times after it lost |
loser_no_target_mode | does not switch to target mode, although the winner may be addressing it | ctrl: ack 1 lost 0 | other: ack 0 lost 1 target_mode 0 | broken 0 |
ctrl_ignores_sda (0x52 against a correct 0x51) | never drops; the target sees the AND of both addresses | I2C S 50 W A P, ctrl: ack 0 lost 1 | other: ack 1 lost 0 target_mode 0 | broken 0 |
drops_on_identical (both 0x50) | drops on bits that agree | other lost after SCL pulse 1 |
arb_on_scl_low (both 0x50) | compares while SCL is low, when SDA may still be moving | other lost after SCL pulse 0 |
Measured. A loser may clock to the end of the byte in which it lost (§3.1.8); this bench's correct loser stops at once. Identical traffic completes for both: ctrl: ack 1 lost 0 | other: ack 1 lost 0 target_mode 0 | broken 0.
Three Cases Without a Defined Result
| Controller 1 sends | while controller 2 sends |
|---|---|
| a repeated START | a data bit |
| a STOP | a data bit |
| a repeated START | a STOP |
UM10204 §3.1.8: if arbitration is still in progress when one controller sends a condition and the other is still sending, the result is not defined. Arbitration compares data bits; here the two are not sending like with like. A design must never get there.
The Formal Lab
The lab states the rule on a two-controller model. After the first high-SCL bit where their outputs differ, at most one still drives, and neither sends STOP while the other pulls SDA. prove checks it for every input sequence; cover shows each side can win.
arbitrationFormal): live0 and live1 are the controllers still in the game; bug: true keeps controller 0 alive after it loses.module top(input clk,input scl_high,input bit0,input bit1,input stop0,input stop1);
reg live0=1,live1=1,differed=0;
wire low0=live0&&!bit0,low1=live1&&!bit1;
wire sda=!(low0||low1);
wire p0=live0&&stop0&&!live1,p1=live1&&stop1&&!live0;
always @(posedge clk)begin
if(scl_high)begin
if(live0&&bit0&&!sda)live0<=0;
if(live1&&bit1&&!sda)live1<=0;
if(live0&&live1&&(bit0!=bit1))differed<=1;
end
if(differed)assert(!(live0&&live1));assert(!(p0&&low1));assert(!(p1&&low0));
end
endmodule| Variant | Task | Verdict |
|---|---|---|
| correct controllers | prove, abc pdr, depth 40 | PASS in 503 ms |
bug: true (controller 0 never drops) | prove, abc pdr | FAIL at step 2 |
| cover: each controller can win | cover, smtbmc yices | PASS by step 2 |
Measured on the site's formal runner (SymbiYosys). The model is a synchronous abstraction of the rule, not a proof of the event-driven bench.
Try It
The two controllers start in the same instant. ctrl sends 0x50 W and other 0x51 W; the probe prints when other drops out. ck.broken is 0: the merged clock meets every Fast-mode minimum.
Give both the same address, then set other.drops_on_identical = 1; or other.ctrl_ignores_sda = 1; (with 0x51 against 0x52) and compare the flags.
other lost after SCL pulse 7 ctrl: ack 1 lost 0 | other: ack 0 lost 1 target_mode 1 | broken 0Read included file: i2c_ctrl.sv
`timescale 1ns/1ns
module i2c_ctrl(inout wire scl,sda,output reg scl_low=0,sda_low=0);
parameter time TLOW=1300,THIGH=1200,HOLD=100,TBUF=1300,TIMEOUT=20000,THD_STA=600,TSU_STA=600,TSU_STO=600;
bit ctrl_ignores_scl=0,ctrl_ignores_sda=0,eight_bit_addr=0,stop_between=0,data_change_scl_high=0,clear_eight_clocks=0,no_stop_after_clear=0,hold_zero_early=0,short_tbuf=0,fast_scl=0;
bit loser_keeps_clocking_past_byte=0,loser_no_target_mode=0,drops_on_identical=0,arb_on_scl_low=0;
bit lost=0,timed_out=0,active=0,target_mode=0;int clear_pulses=0;time stopped=0;
assign scl=scl_low?1'b0:1'bz;assign sda=sda_low?1'b0:1'bz;
task automatic wait_clock();time began;began=$time;
if(!ctrl_ignores_scl)while(scl!==1'b1&&!timed_out)begin #10;if($time-began>=TIMEOUT)begin timed_out=1;scl_low=0;sda_low=0;end end
endtask
task automatic high_time();time began;began=$time-1;while(scl===1'b1&&$time-began<(fast_scl?100:THIGH))#1;endtask
task automatic start();
if(!active)begin lost=0;timed_out=0;target_mode=0;if($time-stopped<(short_tbuf?100:TBUF))#((short_tbuf?100:TBUF)-($time-stopped));end
else begin scl_low=1;#(TLOW);end
sda_low=0;#(HOLD);scl_low=0;wait_clock();#(TSU_STA);
if(!timed_out)begin sda_low=1;#(THD_STA);scl_low=1;active=1;end
endtask
task automatic stop();
if(!lost&&!timed_out)begin scl_low=1;#(HOLD);sda_low=1;#(TLOW);scl_low=0;wait_clock();#(TSU_STO);sda_low=0;stopped=$time;#1;end
active=0;scl_low=0;sda_low=0;
endtask
task automatic bit_cycle(input bit value,input bit arbitrate,output bit sampled);
sampled=1;
if(!timed_out&&(!lost||loser_keeps_clocking_past_byte))begin
scl_low=1;#(hold_zero_early?1:HOLD);sda_low=!value;
if(arb_on_scl_low&&arbitrate&&value&&sda===0)lost=1;
#(fast_scl?100:TLOW-(hold_zero_early?1:HOLD));scl_low=0;wait_clock();#1;sampled=sda;
if(arbitrate&&!ctrl_ignores_sda&&((value&&!sampled)||drops_on_identical))begin
lost=1;sda_low=0;target_mode=!loser_no_target_mode;
end
if(data_change_scl_high)begin #100;sda_low=!sda_low;end
high_time();scl_low=1;
if(lost&&!loser_keeps_clocking_past_byte)begin scl_low=0;sda_low=0;end
end
endtask
task automatic write_byte(input reg [7:0] value,output bit ack);bit sampled;
for(int b=7;b>=0;b--)bit_cycle(value[b],1,sampled);
bit_cycle(1,0,sampled);ack=!sampled;sda_low=0;
endtask
task automatic read_byte(input bit ack,output reg [7:0] value);bit sampled;
for(int b=7;b>=0;b--)begin bit_cycle(1,0,sampled);value[b]=sampled;end
bit_cycle(!ack,0,sampled);sda_low=0;
endtask
task automatic address7(input reg [6:0] addr,input bit rd,output bit ack);
write_byte(eight_bit_addr?{1'b0,addr}:{addr,rd},ack);
endtask
task automatic combined_read(input reg [6:0] addr,input reg [7:0] pointer,output reg [7:0] value);
bit ack;start();address7(addr,0,ack);write_byte(pointer,ack);if(stop_between)stop();start();address7(addr,1,ack);read_byte(0,value);stop();
endtask
task automatic bus_clear(output bit cleared);
bit sampled;clear_pulses=0;lost=0;timed_out=0;active=1;sda_low=0;scl_low=0;wait_clock();
while(sda===0&&clear_pulses<(clear_eight_clocks?8:9)&&!timed_out)begin bit_cycle(1,0,sampled);#(HOLD);if(!timed_out)clear_pulses++;end
cleared=sda===1&&!timed_out;
if(!no_stop_after_clear)stop();else begin active=0;scl_low=0;sda_low=0;end
endtask
endmodule
Read included file: i2c_target.sv
`timescale 1ns/1ns
module i2c_target #(parameter [9:0] ADDRESS=10'h050,parameter TEN_BIT=0)
(inout wire scl,sda,output reg scl_low=0,sda_low=0,output wire high_drive);
bit ack_not_released=0,ack_wrong_clock=0,stretch_never_released=0,wrong_addr_ack=0,no_stop_detect=0,autoinc_wrap_bug=0,push_pull_target=0,ignores_sr=0;
// Legal receiver responses, not faults. rx_limit counts post-address bytes,
// including the pointer byte; -1 is unlimited. A busy address is declined once.
bit busy_nack=0;int rx_limit=-1,rx_count=0;
// Optional general-call software reset: UM10204 §§3.1.13–14. This model
// restores mem[i]=i and ptr=0; ADDRESS is fixed, not a programmable register.
// Fault switches and bench configuration are not device reset state.
time stretch_ns=0;bit general_call=1,software_reset=1,general_selected=0,reset_pending=0;int resets=0;
reg [7:0] mem[0:255];reg [7:0] ptr=0,shift=0,tx=0;
int state=0,count=0,bytes=0;bit active=0,selected=0,reading=0,need_ptr=1,ack_value=0,ack_active=0,low_addr_next=0,addressed10=0,reading_ack=0;
// state: 0 receive, 1 receiver ACK, 2 transmit, 3 controller ACK, 4 ignore.
assign high_drive=push_pull_target&&!sda_low;
assign sda=sda_low?1'b0:high_drive?1'b1:1'bz;assign scl=scl_low?1'b0:1'bz;
initial for(int i=0;i<256;i++)mem[i]=i[7:0];
function automatic [7:0] increment(input reg [7:0] p);increment=autoinc_wrap_bug?((p+1)&8'h0f):p+1'b1;endfunction
always @(negedge sda)if(scl===1)begin
if(!(ignores_sr&&active))begin active=1;selected=0;state=0;count=0;bytes=0;rx_count=0;shift=0;reading=0;ack_active=0;sda_low=0;low_addr_next=0;general_selected=0;reset_pending=0;end
end
always @(posedge sda)if(scl===1&&active&&!no_stop_detect)begin active=0;selected=0;state=0;count=0;sda_low=0;addressed10=0;end
always @(posedge scl)if(active)begin
if(state==0)begin
shift={shift[6:0],sda};count++;
if(count==8)begin
ack_value=0;
if(bytes==0)begin
reading=shift[0];
general_selected=general_call&&shift==0;
if(general_selected)begin selected=1;low_addr_next=0;end
else if(TEN_BIT)begin selected=(shift[7:3]==5'b11110&&shift[2:1]==ADDRESS[9:8]&&(!reading||addressed10));low_addr_next=!reading;end
else selected=(shift[7:1]==ADDRESS[6:0]||(wrong_addr_ack&&shift[7:1]==ADDRESS[6:0]+1'b1));
if(selected&&busy_nack)begin selected=0;busy_nack=0;end
ack_value=selected;need_ptr=1;
end else if(low_addr_next)begin selected=selected&&shift==ADDRESS[7:0];ack_value=selected;addressed10=selected;low_addr_next=0;end
else if(selected)begin
ack_value=rx_limit<0||rx_count<rx_limit;
if(general_selected)begin
// Unsupported general-call commands are NACKed, never register writes.
ack_value=ack_value&&bytes==1&&software_reset&&shift==8'h06;
reset_pending=ack_value;
end else if(ack_value)begin rx_count++;if(need_ptr)begin ptr=shift;need_ptr=0;end else begin mem[ptr]=shift;ptr=increment(ptr);end end
if(!ack_value)selected=0;
end
bytes++;state=1;ack_active=0;count=0;
end
end else if(state==2)begin count++;if(count==8)begin state=3;count=0;reading_ack=0;end end
else if(state==3&&reading_ack)begin if(sda===0)begin ptr=increment(ptr);tx=mem[ptr];state=2;count=0;end else state=4;end
end
always @(negedge scl)if(active)begin
// Deliberate early-ACK fault: after seven samples, pull for clock 8.
// The address prefix is already known; its R/W bit has not arrived yet.
if(state==0&&count==7&&ack_wrong_clock)begin
if(bytes==0)sda_low=!busy_nack&&((general_call&&shift[6:0]==0)||(TEN_BIT?(shift[6:2]==5'b11110&&shift[1:0]==ADDRESS[9:8]):(shift[6:0]==ADDRESS[6:0]||(wrong_addr_ack&&shift[6:0]==ADDRESS[6:0]+1'b1))));
else sda_low=selected&&(rx_limit<0||rx_count<rx_limit);
end else if(state==1)begin
if(!ack_active)begin
sda_low=ack_value&&!ack_wrong_clock;ack_active=1;
end else begin
sda_low=ack_not_released&&ack_value;ack_active=0;
if(reset_pending)begin
// Finish the ninth ACK clock before resetting and releasing the bus.
for(int i=0;i<256;i++)mem[i]=i[7:0];
ptr=0;shift=0;tx=0;count=0;bytes=0;rx_count=0;need_ptr=1;
selected=0;reading=0;reading_ack=0;low_addr_next=0;addressed10=0;
general_selected=0;reset_pending=0;resets++;sda_low=0;scl_low=0;state=4;
end else if(!selected)state=4;
else if(reading)begin state=2;tx=mem[ptr];count=0;sda_low=!tx[7];end
else state=0;
// Byte-level stretch after the ACK, as in UM10204 §3.1.9. Prepare
// outgoing data before releasing SCL; overlap the controller's LOW.
if(selected&&ack_value&&(stretch_ns>0||stretch_never_released))begin scl_low=1;if(!stretch_never_released)begin #(stretch_ns);scl_low=0;end end
end
end else if(state==2)sda_low=!tx[7-count];
else if(state==3)begin sda_low=0;reading_ack=1;end
else if(state==4)sda_low=0;
end
endmodule
Read included file: i2c_checker.sv
`timescale 1ns/1ns
// Logical Fm timing only. Instantaneous digital pins cannot measure RC rise/fall or
// establish which high-SCL SDA edge was intended as data; driver intent is separate.
module i2c_checker #(parameter time TLOW=1300,THIGH=600,TBUF=1300,THD_STA=600,TSU_STA=600,TSU_DAT=100,THD_DAT=0,TSU_STO=600)
(input wire scl,sda,input wire [2:0] sda_lows,scl_lows,input wire high_drive);
int broken=0,starts=0,stops=0,pulses=0;bit active=0,seen_rise=0,seen_fall=0,start_pending=0;
time rise=0,fall=0,changed=0,stop_time=0,start_time=0;
task automatic bad(input string rule);broken++;$display("I2C CHECK %s at %0t",rule,$time);endtask
always @(posedge scl)begin
if(seen_fall&&$time-fall<TLOW)bad("tlow");
if(active&&$time-changed<TSU_DAT)bad("tsu_dat");rise=$time;seen_rise=1;if(active)pulses++;
end
always @(negedge scl)begin
if(active&&seen_rise&&$time-rise<THIGH)bad("thigh");
if(start_pending&&$time-start_time<THD_STA)bad("thd_sta");start_pending=0;fall=$time;seen_fall=1;
end
always @(sda)begin
if(scl===1)begin
if(sda===0)begin
if(!active&&stops>0&&$time-stop_time<TBUF)bad("tbuf");
if(active&&$time-rise<TSU_STA)bad("tsu_sta");starts++;active=1;start_pending=1;start_time=$time;
end else if(sda===1&&active)begin if($time-rise<TSU_STO)bad("tsu_sto");stops++;active=0;stop_time=$time;end
end else if(seen_fall&&$time-fall<THD_DAT)bad("thd_dat");
changed=$time;
end
always @(high_drive or sda_lows)begin #1;if(high_drive&&|sda_lows)bad("push_pull_contention");end
// A separate intent-aware bench checks ACK ownership/ninth slot, lost-controller
// withdrawal, timeouts and accidental START/STOP. Those are not inferable from SDA alone.
endmodule
Read included file: i2c_mon.sv
`timescale 1ns/1ns
module i2c_mon(input wire scl,sda);
bit active=0,header=1,trace=0;int count=0,frames=0,starts=0,stops=0;reg [7:0] value=0;
// Assemble the whole S ... Sr ... P transaction before one atomic report.
// Incomplete/stuck transactions produce no line; counters remain live.
string text="";
always @(negedge sda)if(scl===1)begin if(active)text={text," Sr"};else text="I2C S";active=1;header=1;count=0;starts++;end
always @(posedge sda)if(scl===1&&active)begin if(trace)$display("%s P",text);text="";active=0;count=0;frames++;stops++;end
always @(posedge scl)if(active)begin
if(count<8)begin value={value[6:0],sda};count++;end
else begin
if(header)text=$sformatf("%s %02h %s",text,value[7:1],value[0]?"R":"W");
else text=$sformatf("%s %02h",text,value);
text={text,sda?" NA":" A"};header=0;count=0;
end
end
endmodule
// Trusted recovery observer. Driver intent distinguishes the STOP setup edge
// from recovery pulses, including when a stuck target prevents an actual STOP.
module i2c_clear_mon(input wire scl,sda,ctrl_sda_low,enabled,done,timed_out);
int pulses=0;bit stopped=0;
always @(posedge enabled)begin pulses=0;stopped=0;end
always @(posedge scl)if(enabled&&!ctrl_sda_low)pulses++;
always @(posedge sda)if(enabled&&scl===1)stopped=1;
always @(posedge done)$display("I2C CLEAR PULSES %0d STOP %0d CLEARED %0d TIMEOUT %0d",pulses,stopped,(sda===1&&!timed_out),timed_out);
endmodule
Check Yourself
Remember
- On a shared SCL the LOW is the longest controller LOW and the HIGH is the shortest controller HIGH.
- Arbitration compares SDA while SCL is high; the first to send 1 and read 0 drops out and nothing is lost.
- The loser may finish the byte's clocks, must retry when the bus is free, and must become a target if it can.
- Identical transfers both complete; three combinations of conditions and data bits have no defined result.
- The formal lab proves the withdrawal rule on an abstraction, not on the event-driven bench.
Practice
- Separate Five Arbitration Failures Break it · Hard
- Prove Arbitration Withdrawal Verify · Hard
- A Controller That Withdraws on Arbitration Loss Implement · Hard