DCRouter is a 4-port packet router, small enough to read in an afternoon and rich enough to need every technique in this course. It has valid/ready inputs, credit-based outputs, two priority classes with round-robin arbitration, a CRC check on every packet, an APB register block and an idle low-power mode.
It also hides 24 planted bugs, the Bug Zoo. Each is switched on by a define (` define BUG_7``) and each breaks exactly one rule below. With no bug defined, DCRouter meets every rule.
Flit | Bits | Meaning |
|---|---|---|
Header |
| Output port, priority (1 = high), payload length 1 to 15 |
Payload |
| len flits of data |
Tail |
| CRC-8 (x^8 + x^2 + x + 1, initial 0) over header and payload, each flit high byte first |
Rule | DCRouter must |
|---|---|
R1 | Accept a flit only when the input FIFO has room, the port is enabled and it is awake |
R2 | Keep exact FIFO occupancy when a push and a pop happen together |
R3 | Forward each packet whole to its output; never interleave two packets on one output |
R4 | Honour every payload length from 1 to 15 |
R5 | Forward a header with len 0 with out_err on its tail, and count it as an error |
R6 | Arbitrate round-robin per output; with prio_en, serve high priority first |
R7 | Start each output with 4 credits, send only with a credit, count simultaneous send and return correctly |
R8 | Check every CRC; on a mismatch set out_err on the tail and count it |
R9 | Count each input's errors in ERR_CNT, saturating at 255; a write clears only that counter |
R10 | Count every packet sent per output in PKT_CNT, including tails on several outputs at once; a write clears it |
R11 | Reset CTRL to all ports enabled, prio_en and lp_en set |
R12 | Answer unmapped APB addresses with pslverr |
R13 | Sleep only when fully idle for 8 cycles, wake on any input valid, and keep counting returned credits while asleep |
Address | Name | Access | Fields |
|---|---|---|---|
0x00 | CTRL | RW |
|
0x04 | STATUS | RO |
|
0x10 to 0x1C | ERR_CNT0 to 3 | RO, write clears |
|
0x20 to 0x2C | PKT_CNT0 to 3 | RO, write clears |
|
The 24 bugs, by class. Part 1 uses many of them as examples; the complete list, with which technique caught each, is laid out in Part 14. Part 1 asks you to predict which technique will catch each class.
Bug | Class |
|---|---|
BUG_1 | Corner case and boundary |
BUG_2 | Concurrency and race |
BUG_3 | Corner case and boundary |
BUG_4 | Error handling and specification |
BUG_5 | Performance and fairness |
BUG_6 | Configuration and mode |
BUG_7 | Configuration and mode |
BUG_8 | Corner case and boundary |
BUG_9 | Concurrency and race |
BUG_10 | Performance and fairness |
BUG_11 | Concurrency and race |
BUG_12 | Corner case and boundary |
BUG_13 | Configuration and mode |
BUG_14 | Registers and integration |
BUG_15 | Corner case and boundary |
BUG_16 | Registers and integration |
BUG_17 | Reset |
BUG_18 | Error handling and specification |
BUG_19 | Registers and integration |
BUG_20 | Low power |
BUG_21 | Low power |
BUG_22 | Low power |
BUG_23 | Configuration and mode |
BUG_24 | Concurrency and race |
A reference regression written for the course catches all 24 bugs and passes on the clean design, which proves every bug is detectable at DCRouter's pins. The smoke test below catches only 2 of them.
// snippet: the DCRouter RTL. Every DCRouter testbench in the course runs against it.
// DCRouter: the 4-port packet router verified across First Principles of Verification Strategy.
// Specification: docs/verification-fp-dcrouter.md. Define BUG_1 .. BUG_24 (one at a time) to
// switch on a planted bug from the Bug Zoo; with none defined, every rule R1-R13 holds.
//
// Packet: header {dst[1:0], prio, len[3:0], 9'b0}, len payload flits, tail {8'b0, crc8}.
// Ingress: valid/ready per port. Egress: credits (4 per output). Registers: APB.
module dcr_fifo (
input logic clk, rst, push, pop,
input logic [16:0] din,
output logic [16:0] dout,
output logic full, empty
);
logic [16:0] mem [0:7];
logic [2:0] wp, rp;
logic [3:0] count;
`ifdef BUG_1
assign full = (count > 4'd8); // BUG_1: full flag one entry late
`else
assign full = (count == 4'd8);
`endif
assign empty = (count == 4'd0);
assign dout = mem[rp];
always_ff @(posedge clk) begin
if (rst) begin
wp <= 0; rp <= 0; count <= 0;
end else begin
if (push) begin mem[wp] <= din; wp <= wp + 3'd1; end
if (pop) rp <= rp + 3'd1;
case ({push, pop})
2'b10: count <= count + 4'd1;
2'b01: count <= count - 4'd1;
`ifdef BUG_2
2'b11: count <= count + 4'd1; // BUG_2: push and pop together counted as a push
`endif
default: ;
endcase
end
end
`ifdef FORMAL
// Designer properties (R1, R2), checked by formal tools only: occupancy never exceeds the
// depth, and the count agrees with the pointers (the invariant that makes induction work).
always @(posedge clk) if (!rst) begin
assert (count <= 4'd8);
assert (count[2:0] == 3'(wp - rp));
end
`endif
endmodule
module dcrouter (
input logic clk, rst,
input logic [3:0] in_vld,
output logic [3:0] in_rdy,
input logic [63:0] in_data,
input logic [3:0] in_last,
output logic [3:0] out_vld,
output logic [63:0] out_data,
output logic [3:0] out_last,
output logic [3:0] out_err,
input logic [3:0] out_crd,
input logic psel, penable, pwrite,
input logic [7:0] paddr,
input logic [31:0] pwdata,
output logic [31:0] prdata,
output logic pready, pslverr,
output logic sleeping
);
function automatic logic [7:0] crc8(input logic [7:0] c, input logic [15:0] d);
logic [7:0] x;
x = c;
for (int k = 15; k >= 0; k--) x = (x[7] ^ d[k]) ? {x[6:0], 1'b0} ^ 8'h07 : {x[6:0], 1'b0};
crc8 = x;
endfunction
// ---------------- registers ----------------
logic [3:0] port_en;
logic prio_en, lp_en;
logic [7:0] err_cnt [0:3];
logic [15:0] pkt_cnt [0:3];
// ---------------- input FIFOs ----------------
logic [3:0] push, pop, full, empty;
logic [16:0] head [0:3];
genvar gi;
generate for (gi = 0; gi < 4; gi++) begin : g_in
dcr_fifo u_fifo (.clk(clk), .rst(rst), .push(push[gi]), .pop(pop[gi]),
.din({in_last[gi], in_data[16*gi +: 16]}), .dout(head[gi]),
.full(full[gi]), .empty(empty[gi]));
`ifdef BUG_23
assign in_rdy[gi] = !full[gi] && !sleeping; // BUG_23: disabled port still ready
`else
assign in_rdy[gi] = !full[gi] && port_en[gi] && !sleeping;
`endif
assign push[gi] = in_vld[gi] && in_rdy[gi];
end endgenerate
// ---------------- per-input packet state ----------------
logic [3:0] fwd; // input is forwarding a granted packet
logic [3:0] plen [0:3]; // payload length of the packet being forwarded
logic [4:0] idx [0:3]; // flits of it sent so far
logic [7:0] crc [0:3]; // running CRC
logic [3:0] hprio; // its priority
logic [1:0] last_dst [0:3];
logic [3:0] prev_tail; // a tail left this input in the previous cycle
logic [3:0] req;
logic [1:0] rdst [0:3];
logic [3:0] rprio;
always_comb begin
for (int i = 0; i < 4; i++) begin
req[i] = !empty[i] && !fwd[i];
rprio[i] = head[i][13];
`ifdef BUG_24
rdst[i] = prev_tail[i] ? last_dst[i] : head[i][15:14]; // BUG_24: back-to-back packet uses previous dst
`else
rdst[i] = head[i][15:14];
`endif
end
end
// ---------------- outputs: lock, arbitration, credits ----------------
logic [3:0] lock;
logic [1:0] owner [0:3];
logic [1:0] rr [0:3];
logic [2:0] credits [0:3];
logic [3:0] send, is_tail, bad;
// grant[o] / gidx[o]: arbitration result for a free output this cycle
logic [3:0] grant;
logic [1:0] gidx [0:3];
always_comb begin
for (int o = 0; o < 4; o++) begin
logic [3:0] cand, hi;
logic use_prio;
cand = 4'b0;
for (int i = 0; i < 4; i++) cand[i] = req[i] && (rdst[i] == 2'(o));
hi = cand & rprio;
`ifdef BUG_6
use_prio = 1'b0; // BUG_6: priority ignored
`elsif BUG_7
use_prio = (hi != 0); // BUG_7: priority even when prio_en is clear
`else
use_prio = prio_en && (hi != 0);
`endif
if (use_prio) cand = hi;
grant[o] = !lock[o] && (cand != 0) && !sleeping;
gidx[o] = 2'd0;
for (int k = 3; k >= 0; k--) if (cand[2'(rr[o] + 2'(k))]) gidx[o] = 2'(rr[o] + 2'(k));
end
end
// sending: an owned output with a non-empty FIFO and a credit
always_comb begin
pop = 4'b0;
for (int o = 0; o < 4; o++) begin
logic [1:0] g;
logic crd_ok;
g = owner[o];
crd_ok = (credits[o] != 0);
send[o] = lock[o] && !empty[g] && crd_ok && !sleeping;
`ifdef BUG_3
is_tail[o] = (idx[g] == {1'b0, (plen[g] == 4'd15 ? 4'd0 : plen[g])} + 5'd1); // BUG_3: len 15 treated as 0
`elsif BUG_8
is_tail[o] = (idx[g] == {1'b0, plen[g]}); // BUG_8: lock released one flit early
`else
is_tail[o] = (idx[g] == {1'b0, plen[g]} + 5'd1);
`endif
bad[o] = (plen[g] == 4'd0) || (head[g][7:0] != crc[g]);
`ifdef BUG_4
bad[o] = (head[g][7:0] != crc[g]); // BUG_4: len 0 not flagged
`endif
`ifdef BUG_13
if (hprio[g]) bad[o] = 1'b0; // BUG_13: no error report for high priority
`endif
out_vld[o] = send[o];
out_data[16*o +: 16] = head[g][15:0];
out_last[o] = send[o] && is_tail[o];
out_err[o] = send[o] && is_tail[o] && bad[o];
if (send[o]) pop[g] = 1'b1;
end
end
// idle and sleep
logic [3:0] idle_cnt;
logic idle_now;
`ifdef BUG_20
assign idle_now = lp_en && (empty == 4'hF) && (in_vld == 4'h0); // BUG_20: ignores locks
`else
assign idle_now = lp_en && (empty == 4'hF) && (lock == 4'h0) && (in_vld == 4'h0);
`endif
logic wake;
`ifdef BUG_21
assign wake = |in_vld[2:0]; // BUG_21: port 3 cannot wake it
`else
assign wake = |in_vld;
`endif
always_ff @(posedge clk) begin
if (rst) begin
lock <= 0; fwd <= 0; hprio <= 0; prev_tail <= 0; sleeping <= 0; idle_cnt <= 0;
for (int k = 0; k < 4; k++) begin
owner[k] <= 0; rr[k] <= 0; plen[k] <= 0; idx[k] <= 0; crc[k] <= 0; last_dst[k] <= 0;
`ifdef BUG_10
credits[k] <= 3'd3; // BUG_10: 3 credits after reset
`else
credits[k] <= 3'd4;
`endif
end
end else begin
prev_tail <= 0;
for (int o = 0; o < 4; o++) begin
// credits
`ifdef BUG_9
if (send[o]) credits[o] <= credits[o] - 3'd1; // BUG_9: a return in the same cycle is lost
else if (out_crd[o]) credits[o] <= credits[o] + 3'd1;
`elsif BUG_22
if (!sleeping || send[o]) credits[o] <= credits[o] + (out_crd[o] ? 3'd1 : 3'd0) - (send[o] ? 3'd1 : 3'd0); // BUG_22: returns lost while sleeping
`else
credits[o] <= credits[o] + (out_crd[o] ? 3'd1 : 3'd0) - (send[o] ? 3'd1 : 3'd0);
`endif
// grant a free output
if (grant[o]) begin
lock[o] <= 1'b1;
owner[o] <= gidx[o];
`ifndef BUG_5
rr[o] <= gidx[o] + 2'd1; // BUG_5 leaves the pointer where it is
`endif
fwd[gidx[o]] <= 1'b1;
idx[gidx[o]] <= 0;
hprio[gidx[o]] <= rprio[gidx[o]];
last_dst[gidx[o]] <= rdst[gidx[o]];
end
// forward a flit
if (send[o]) begin
logic [1:0] g;
g = owner[o];
idx[g] <= idx[g] + 5'd1;
if (idx[g] == 0) begin
plen[g] <= head[g][12:9];
crc[g] <= crc8(8'h00, head[g][15:0]);
end else if (!is_tail[o]) begin
`ifdef BUG_12
if (plen[g] != 4'd1) crc[g] <= crc8(crc[g], head[g][15:0]); // BUG_12: single payload flit not in CRC
`else
crc[g] <= crc8(crc[g], head[g][15:0]);
`endif
end
if (is_tail[o] && idx[g] != 0) begin
lock[o] <= 1'b0;
fwd[g] <= 1'b0;
prev_tail[g] <= 1'b1;
end
end
end
// sleep entry and exit; locks are not retained in sleep
if (sleeping) begin
if (wake) sleeping <= 1'b0;
end else if (idle_now && idle_cnt == 4'd7) begin
sleeping <= 1'b1;
lock <= 0;
fwd <= 0;
end
idle_cnt <= (idle_now && !sleeping) ? (idle_cnt == 4'd7 ? idle_cnt : idle_cnt + 4'd1) : 4'd0;
end
end
// ---------------- APB registers ----------------
logic [3:0] tail_err; // per input: an errored tail left this cycle
logic [3:0] tail_any; // per input: a tail left this cycle
always_comb begin
tail_err = 0; tail_any = 0;
for (int o = 0; o < 4; o++) if (send[o] && is_tail[o] && idx[owner[o]] != 0) begin
tail_any[owner[o]] = 1'b1;
if (bad[o]) tail_err[owner[o]] = 1'b1;
end
end
wire acc = psel && penable;
wire known = (paddr == 8'h00) || (paddr == 8'h04) || (paddr[7:4] == 4'h1 && paddr[1:0] == 2'b00) || (paddr[7:4] == 4'h2 && paddr[1:0] == 2'b00);
assign pready = 1'b1;
`ifdef BUG_18
assign pslverr = 1'b0; // BUG_18: unmapped addresses not reported
`else
assign pslverr = acc && !known;
`endif
always_comb begin
case (paddr)
8'h00: prdata = {26'b0, lp_en, prio_en, port_en};
8'h04: prdata = {27'b0, sleeping, lock};
8'h10: prdata = {24'b0, err_cnt[0]};
8'h14: prdata = {24'b0, err_cnt[1]};
8'h18: prdata = {24'b0, err_cnt[2]};
8'h1C: prdata = {24'b0, err_cnt[3]};
8'h20: prdata = {16'b0, pkt_cnt[0]};
8'h24: prdata = {16'b0, pkt_cnt[1]};
8'h28: prdata = {16'b0, pkt_cnt[2]};
8'h2C: prdata = {16'b0, pkt_cnt[3]};
default: prdata = 32'b0;
endcase
end
always_ff @(posedge clk) begin
if (rst) begin
`ifdef BUG_17
port_en <= 4'h7; // BUG_17: port 3 disabled after reset
`else
port_en <= 4'hF;
`endif
prio_en <= 1'b1; lp_en <= 1'b1;
for (int k = 0; k < 4; k++) begin err_cnt[k] <= 0; pkt_cnt[k] <= 0; end
end else begin
for (int k = 0; k < 4; k++) begin
`ifdef BUG_14
if (tail_err[k] || (k == 2 && tail_any[k])) // BUG_14: port 2 counts good packets too
`else
if (tail_err[k])
`endif
`ifdef BUG_15
err_cnt[k] <= err_cnt[k] + 8'd1; // BUG_15: wraps instead of saturating
`else
err_cnt[k] <= (err_cnt[k] == 8'hFF) ? 8'hFF : err_cnt[k] + 8'd1;
`endif
end
`ifdef BUG_11
begin : g_pktcnt // BUG_11: simultaneous tails, only the lowest output counts
logic done;
done = 1'b0;
for (int o = 0; o < 4; o++) if (!done && send[o] && is_tail[o] && idx[owner[o]] != 0) begin
pkt_cnt[o] <= pkt_cnt[o] + 16'd1;
done = 1'b1;
end
end
`else
for (int o = 0; o < 4; o++) if (send[o] && is_tail[o] && idx[owner[o]] != 0) pkt_cnt[o] <= pkt_cnt[o] + 16'd1;
`endif
if (acc && pwrite) begin
if (paddr == 8'h00) begin port_en <= pwdata[3:0]; prio_en <= pwdata[4]; lp_en <= pwdata[5]; end
for (int k = 0; k < 4; k++) begin
`ifdef BUG_19
if (paddr == 8'h10 + 8'(4 * k) || paddr == 8'h10) err_cnt[k] <= 0; // BUG_19: ERR_CNT0 clears all four
`else
if (paddr == 8'h10 + 8'(4 * k)) err_cnt[k] <= 0;
`endif
`ifdef BUG_16
if (paddr == 8'h20 + 8'(4 * k) && k != 3) pkt_cnt[k] <= 0; // BUG_16: PKT_CNT3 not cleared
`else
if (paddr == 8'h20 + 8'(4 * k)) pkt_cnt[k] <= 0;
`endif
end
end
end
end
`ifdef FORMAL
// Designer properties (R3, R6, R7), checked by formal tools only (read_verilog -formal
// defines FORMAL; simulators never see this block). A wrapper supplies the environment.
logic f_past = 1'b0;
always @(posedge clk) f_past <= 1'b1;
// R7: an output's credits plus the flits its sink still holds always total 4
logic [2:0] f_held [0:3];
always @(posedge clk)
for (int o = 0; o < 4; o++)
f_held[o] <= rst ? 3'd0 : f_held[o] + (send[o] ? 3'd1 : 3'd0) - (out_crd[o] ? 3'd1 : 3'd0);
// environment: a sink returns a credit only for a flit it holds
always @(*) for (int o = 0; o < 4; o++) if (out_crd[o]) assume (f_held[o] != 3'd0);
// R6: the specification's choice of winner for each free output: the first requester at or
// after the round-robin pointer, among high-priority requesters if prio_en is set and any exist
logic [3:0] f_any, f_hi;
logic [1:0] f_win [0:3];
always_comb
for (int o = 0; o < 4; o++) begin
f_any[o] = 1'b0; f_hi[o] = 1'b0; f_win[o] = 2'd0;
for (int i = 0; i < 4; i++) if (req[i] && head[i][15:14] == 2'(o)) begin
f_any[o] = 1'b1;
if (head[i][13]) f_hi[o] = 1'b1;
end
for (int k = 3; k >= 0; k--) begin
logic [1:0] i;
i = 2'(rr[o] + 2'(k));
if (req[i] && head[i][15:14] == 2'(o) && (!(prio_en && f_hi[o]) || head[i][13])) f_win[o] = i;
end
end
always @(posedge clk) if (f_past && !rst)
for (int o = 0; o < 4; o++) begin
assert ({1'b0, credits[o]} + {1'b0, f_held[o]} == 4'd4); // R7
if (!lock[o] && !sleeping && f_any[o]) assert (grant[o] && gidx[o] == f_win[o]); // R6, R3
if ($past(grant[o] && !rst)) assert (rr[o] == $past(gidx[o]) + 2'd1); // R6 rotation
end
`endif
endmoduleOne packet in, one packet out. It is the cheapest possible test, and it shows how little a smoke test proves.
// uses: dcrouter
// DCRouter smoke test: one 3-payload packet from input 0 to output 2, with a sink that
// returns a credit for every flit. The checker compares every output flit with the
// packet sent and confirms the tail is marked and no error is reported.
module tb;
logic clk = 0;
always #5 clk = ~clk;
logic rst = 1;
logic [3:0] in_vld = 0, in_last = 0, in_rdy, out_vld, out_last, out_err, out_crd;
logic [63:0] in_data = 0, out_data;
logic psel = 0, penable = 0, pwrite = 0, pready, pslverr, sleeping;
logic [7:0] paddr = 0;
logic [31:0] pwdata = 0, prdata;
dcrouter dut (.*);
function automatic logic [7:0] crc8(input logic [7:0] c, input logic [15:0] d);
logic [7:0] x;
x = c;
for (int k = 15; k >= 0; k--) x = (x[7] ^ d[k]) ? {x[6:0], 1'b0} ^ 8'h07 : {x[6:0], 1'b0};
return x;
endfunction
logic [15:0] pkt [0:4];
int sent = 0, got = 0, bad = 0, tails = 0;
initial begin
logic [7:0] c;
pkt[0] = {2'd2, 1'b0, 4'd3, 9'd0}; // header: dst 2, low priority, 3 payload flits
pkt[1] = 16'hA001; pkt[2] = 16'hB002; pkt[3] = 16'hC003;
c = crc8(8'h00, pkt[0]);
for (int k = 1; k <= 3; k++) c = crc8(c, pkt[k]);
pkt[4] = {8'h00, c}; // tail: CRC-8
repeat (3) @(posedge clk); rst <= 0;
end
// source: valid/ready on input 0
always @(posedge clk) if (!rst) begin
if (in_vld[0] && in_rdy[0]) sent <= sent + 1;
in_vld[0] <= (sent + (in_vld[0] && in_rdy[0] ? 1 : 0)) < 5;
in_data[15:0] <= pkt[(sent + (in_vld[0] && in_rdy[0] ? 1 : 0)) % 5];
in_last[0] <= (sent + (in_vld[0] && in_rdy[0] ? 1 : 0)) == 4;
end
// sink on output 2: check each flit, return one credit per flit
always @(posedge clk) begin
out_crd <= {1'b0, out_vld[2], 2'b0};
if (out_vld[2]) begin
if (out_data[47:32] !== pkt[got]) bad++;
if (out_last[2]) begin tails++; if (got != 4 || out_err[2]) bad++; end
got <= got + 1;
end
if (out_vld[0] || out_vld[1] || out_vld[3]) bad++;
end
initial begin
#600;
if (got == 5 && tails == 1 && bad == 0) $display("PASS: one packet routed from input 0 to output 2, all 5 flits intact, tail marked, no error");
else $display("FAIL: got %0d flits, %0d tails, %0d mismatches", got, tails, bad);
$finish;
end
endmoduleWhen run, it prints a PASS line. Run against the Bug Zoo, it catches 2 of the 24 bugs (a FIFO count error and a lock released early); the other 22 pass it.