Case / diagnostic | Planted mechanism | Correction | Regression and legal control |
|---|---|---|---|
A / EARLY_B (1) | BVALID is offered before captured AW and final W prerequisites. | Gate the response using previously accepted write context; do not rely on BREADY to hide an early offer. | Detect premature B with BREADY=0; preserve legal W-first/AW-first/simultaneous arrivals. |
B / STALLED_W (2) | The pending W payload changes from 16 to 0 while stalled, and the target later commits 0. | Retain the whole pending VALID/payload tuple through acceptance; do not refill or clear it early. | Vary payload and stall duration, including a change on the accepting edge; check one target commit. |
C / READ_ORDER (4) | The second pending ID 3 address is selected before the first. | Return each same-port same-ID queue head; keep different-ID service independent. | Two distinct same-ID words plus ID 7 overlap; legal C,A,B passes, C,B,A fails. |
D / DECODE (8) | The default address-class response is changed from DECERR to OKAY. | Restore correct unmapped decode response without changing valid mapped windows. | Test unmapped controls and both mapped window classes; distinguish DECERR from target SLVERR. |
E / ORPHAN_R (16) | DUT-side pending read state survives coordinated cancellation while observer/new-epoch state clears. | Apply the chosen cancellation policy to all participants and discard/isolate old responses before reopening admission. | Pending work, reset, idle interval before new AR, then reused ID; no stale response and correct new data. |
The trace establishes violated obligations under the lab contract. In a real implementation, pipeline selection, routing, buffering, monitor state and reset distribution remain candidates until internal evidence identifies the faulty element. The chosen reset cancellation policy must not be copied to a product that instead requires draining, retained work or a different recovery contract.
The task-driven model supplies CPU0 register-write and DMA0 read events. Its reference queues derive expected values from the declared initial-memory contract; responses use a separate pending-address queue and memory lookup. Each mutation changes the modelled observed behaviour, while the checker predicates remain unchanged. Queue bounds and work accounting fail separately if the harness itself loses context.
Default operation audits six selections and three data seeds, then runs mutation-disabled clean baselines after each faulty selection. That is 33 scenario runs by source construction, not a reported execution result. The known faults are intentionally visible in this Solutions-side source; the Brief, Evidence and Checks pages do not embed it.
// Solutions-side source for the bounded Bus Protocols integration lab.
// This is a task-driven transaction/event model, NOT CPU/DMA/CDC RTL.
// No physical cycle timing, arbitration fairness or metastability is modelled.
// Default: self-audit baseline + five mutations + repaired replays.
// +CASE=0..5: audit that selection only, with event logging for seed zero.
module bus_integration_lab_tb;
localparam EARLY_B=1, STALLED_W=2, READ_ORDER=4, DECODE=8, ORPHAN_R=16;
reg [31:0] errors, len_bytes;
reg saw_aw, saw_w, held_w;
reg [63:0] held_data, accepted_data;
reg [31:0] dut_q [0:15][0:3];
reg [63:0] ref_q [0:15][0:3];
integer dut_n [0:15], ref_n [0:15];
reg [63:0] memory [0:3];
integer mode, seed, event_no, selected, first_case, last_case;
integer aw_count, w_count, b_count, apb_count, ar_count, matched_r, cancelled;
integer checks=0, runs=0;
bit logging;
task require(input bit ok, input [767:0] why);
begin
checks=checks+1;
if (!ok) $fatal(1, "FAIL: %0s", why);
end
endtask
task event_note(input [767:0] message);
begin
event_no=event_no+1;
if (logging) $display("EVENT %0d: %0s", event_no, message);
end
endtask
// Reference data is derived from the frozen initial-memory contract.
// DUT reads use its independent request queue and memory indexing below.
function [63:0] expected_word(input [31:0] addr);
begin
case (addr)
32'h2000_0000: expected_word=64'h11+seed*256;
32'h2000_0008: expected_word=64'h22+seed*256;
32'h2000_0010: expected_word=64'h33+seed*256;
32'h2000_0018: expected_word=64'h44+seed*256;
default: expected_word=0;
endcase
end
endfunction
task write_sample(input bit av, wv, wr, input [63:0] data,
input bit bv, br);
begin
event_note("CPU0 write-channel sample (AWREADY=1 when AWVALID)");
if (logging) $display(" AWV=%0b WV=%0b WR=%0b WD=%h BV=%0b BR=%0b",
av,wv,wr,data,bv,br);
if (held_w && (!wv || data !== held_data)) errors=errors|STALLED_W;
if (bv && !(saw_aw && saw_w)) errors=errors|EARLY_B;
held_w=wv && !wr;
held_data=data;
// Update history after testing this event's response prerequisites.
if (av) begin saw_aw=1; aw_count=aw_count+1; end
if (wv && wr) begin saw_w=1; accepted_data=data; w_count=w_count+1; end
if (bv && br) begin saw_aw=0; saw_w=0; b_count=b_count+1; end
end
endtask
task request_read(input [3:0] id, input [31:0] addr);
begin
require(dut_n[id]<4 && ref_n[id]<4, "lab queue capacity, not a protocol limit");
event_note("DMA0 AR accepted");
if (logging) $display(" ID=%0d ADDR=%h",id,addr);
dut_q[id][dut_n[id]]=addr; dut_n[id]=dut_n[id]+1;
ref_q[id][ref_n[id]]=expected_word(addr); ref_n[id]=ref_n[id]+1;
ar_count=ar_count+1;
end
endtask
task return_read(input [3:0] id, input integer slot);
reg [31:0] addr;
reg [63:0] data;
begin
require(slot<dut_n[id], "model response has a real DUT-side pending request");
addr=dut_q[id][slot];
require(addr>=32'h2000_0000 && addr<=32'h2000_0018 && addr[2:0]==0,
"model memory index is in range");
data=memory[(addr-32'h2000_0000)/8];
event_note("DMA0 R accepted; RLAST=1, RRESP=OKAY");
if (logging) $display(" RID=%0d DATA=%h",id,data);
// No address/sequence/epoch field is invented on the R interface.
if (ref_n[id]==0) errors=errors|ORPHAN_R;
else begin
matched_r=matched_r+1;
if (data !== ref_q[id][0]) errors=errors|READ_ORDER;
for (integer n=0; n<3; n=n+1) ref_q[id][n]=ref_q[id][n+1];
ref_n[id]=ref_n[id]-1;
end
for (integer n=slot; n<3; n=n+1) dut_q[id][n]=dut_q[id][n+1];
dut_n[id]=dut_n[id]-1;
end
endtask
function [1:0] dut_decode_status(input [31:0] addr);
begin
if ((addr>=32'h2000_0000 && addr<=32'h2000_ffff) ||
(addr>=32'h4000_0000 && addr<=32'h4000_ffff)) dut_decode_status=0;
else dut_decode_status=(mode==4 ? 2'b00 : 2'b11);
end
endfunction
task run_case(input integer mutation, input integer initial_seed);
reg [63:0] offered;
reg [1:0] decode_result;
begin
mode=mutation; seed=initial_seed; event_no=0; runs=runs+1;
logging=(selected>=0 && initial_seed==0);
errors=0; len_bytes=0; saw_aw=0; saw_w=0; held_w=0;
held_data=0; accepted_data=0;
aw_count=0; w_count=0; b_count=0; apb_count=0;
ar_count=0; matched_r=0; cancelled=0;
for (integer id=0; id<16; id=id+1) begin
dut_n[id]=0; ref_n[id]=0;
for (integer n=0; n<4; n=n+1) begin dut_q[id][n]=0; ref_q[id][n]=0; end
end
for (integer n=0; n<4; n=n+1) memory[n]=64'h11*(n+1)+seed*256;
if (logging) $display("CASE %0d seed=%0d", mode, seed);
// CPU0: one 32-bit LEN_BYTES write at 0x4000_0008, AWID=1,
// AWLEN=0, AWSIZE=2, WSTRB=0x0f, WLAST=1 throughout.
write_sample(0,1,0,64'h10,0,0);
offered=(mode==2 ? 64'h0 : 64'h10);
write_sample(0,1,0,offered,mode==1,0);
write_sample(0,1,1,offered,mode==1,0);
write_sample(1,0,0,0,mode==1,0);
event_note("APB_BRIDGE command delivered; SETUP to DMA_CFG");
event_note("APB ACCESS waits; PREADY=0; LEN_BYTES remains 0");
require(saw_aw && saw_w, "APB work requires both captured write parts");
len_bytes=accepted_data[31:0]; apb_count=apb_count+1;
event_note("APB ACCESS completes; PREADY=1, PSLVERR=0");
if (logging) $display(" LEN_BYTES=%0d", len_bytes);
if (len_bytes!==32'h10) errors=errors|STALLED_W;
write_sample(0,0,0,0,1,0);
write_sample(0,0,0,0,1,1);
request_read(3,32'h2000_0000); request_read(3,32'h2000_0008);
request_read(7,32'h2000_0010);
return_read(7,0);
return_read(3,mode==3 ? 1 : 0); return_read(3,0);
event_note("CPU0 single-beat read probes unmapped 0x5000_0000");
decode_result=dut_decode_status(32'h5000_0000);
if (logging) $display(" RRESP=%0b",decode_result);
if (decode_result!==2'b11) errors=errors|DECODE;
require(dut_decode_status(32'h2000_0000)==0 &&
dut_decode_status(32'h4000_0008)==0, "mapped decode positive controls");
request_read(3,32'h2000_0000);
event_note("Coordinated reset cancels pending work; memory is retained");
// Chosen system policy: all participants acknowledge reset, source stops,
// LEN_BYTES resets, and no pre-reset response may enter the new epoch.
// Diagnostic error history is retained outside that reset domain.
len_bytes=0; saw_aw=0; saw_w=0; held_w=0;
for (integer id=0; id<16; id=id+1) begin
cancelled=cancelled+ref_n[id]; ref_n[id]=0;
if (mode!=5) dut_n[id]=0;
end
event_note("Reset release acknowledged by all model participants");
if (dut_n[3]>0) return_read(3,0);
else event_note("No R offered before the new request");
request_read(3,32'h2000_0008); return_read(3,0);
require(aw_count==1 && w_count==1 && b_count==1 && apb_count==1,
"one real register transfer completed through each boundary");
require(ar_count==5 && matched_r==4 && cancelled==1,
"read work accounted as responses or explicit cancellation");
for (integer id=0; id<16; id=id+1)
require(dut_n[id]==0 && ref_n[id]==0, "DUT and reference read queues drain");
if (logging) $display("OBSERVED: diagnostic_mask=%0d",errors);
end
endtask
initial begin
selected=-1;
if ($value$plusargs("CASE=%d",selected))
require(selected>=0 && selected<=5, "CASE selection must be 0..5");
first_case=(selected<0 ? 0 : selected);
last_case=(selected<0 ? 5 : selected);
for (integer c=first_case; c<=last_case; c=c+1)
for (integer s=0; s<3; s=s+1) begin
run_case(c,s);
require(errors==(c==0 ? 0 : (1 << (c-1))),
"baseline clean or mutation detected by exactly its intended rule");
if (c!=0) begin
run_case(0,s);
require(errors==0, "repaired baseline replay passes after mutation");
end
end
require(runs>0 && checks>50, "selected campaign performed nonzero work");
$display("PASS: lab harness audited baseline, selected mutations and clean replays");
$finish;
end
endmodule# From the repository root, by an operator permitted to run checks:
iverilog -g2012 -s bus_integration_lab_tb -o /tmp/protocols-bus-lab.vvp scripts/data/protocols-course/rich/protocol-verification/models/bus-integration-lab.sv
vvp /tmp/protocols-bus-lab.vvp
vvp /tmp/protocols-bus-lab.vvp +CASE=1These commands are provided for later review and have not been run in this authoring pass. Changing source to repair a selected mutation requires updating the expected-verdict campaign deliberately; do not simply waive a failed checker. Preserve the original negative control in a separate reviewed regression.
Pin-level AXI/APB protocol checking, all channel payloads, arbitrary supported bursts/strobes, real response errors and bridge transformations.
Actual asynchronous request/response crossing, capacity, backpressure, clock/reset/power sequences and a reviewed recovery policy.
DMA START, data movement, target side effects, IRQ routing, software ordering/ownership and concurrency at every implemented boundary.
Independent tests/models, workload coverage, justified progress bounds and reviewed evidence for each requirement. A bounded harness PASS is not signoff.