When two case items match, the first one in source order wins in simulation. Synthesis builds the same priority, so overlap is a priority encoder rather than parallel logic.
A designer who assumed one-hot requests reads the overlap vector wrong. The table below fixes the reading for a two-request arbiter.
| First match | Grant | One-hot reading |
|---|---|---|---|
| default | none | Idle, agrees |
|
| g0 | Agrees |
|
| g1 | Agrees |
|
| g1 | Expects both grants: the surprise |
casez treats ? in the items as wildcards, which suits masked decodes. casex additionally treats x and z in the selector as wildcards, so an unknown selector can match an unintended item.
Prefer plain case with a default, or casez with ? only in the items. Avoid casex in synthesizable code.
The sketch below is illustrative and not runnable: directive-style promises vary by flow, and the wording here is generic rather than a command of any tool.
illustrative promise sketch (not runnable; spelling varies by flow)
designer promise: exactly one request bit is ever high (one-hot)
designer promise: the case covers every reachable selector (full case)
gates built under a parallel promise drop the priority logic and the default arm
simulation still shows first-match priority, so vector 11 is where the two views partIf the one-hot promise is wrong even once, the gates answer vector 11 with parallel logic while simulation shows priority. Prove one-hot with an assertion instead of promising it in a comment.
The testbench below builds the arbiter twice: once with a sensitivity bug plus overlapping items, once in the fixed priority form. It expects exactly two stale steps and one overlap surprise, and passes only on those counts.
module arb_fixed (
input logic r0,
input logic r1,
output logic g0,
output logic g1
);
always_comb begin
g0 = 1'b0;
g1 = 1'b0;
if (r1) g1 = 1'b1;
else if (r0) g0 = 1'b1;
end
endmodule
module arb_buggy (
input logic r0,
input logic r1,
output logic g0,
output logic g1
);
always @(r1) begin
g0 = 1'b0;
g1 = 1'b0;
casez ({r1, r0})
2'b1?: g1 = 1'b1;
2'b?1: g0 = 1'b1;
default: begin g0 = 1'b0; g1 = 1'b0; end
endcase
end
endmodule
The Yosys script proves the fixed point: the overlapping casez form is equivalent to the plain priority chain, so the chain is the intent the gates keep.
read_verilog <<EOV
module gold(r0, r1, g0, g1);
input r0;
input r1;
output g0;
output g1;
reg g0;
reg g1;
always @* begin
g0 = 1'b0;
g1 = 1'b0;
if (r1) g1 = 1'b1;
else if (r0) g0 = 1'b1;
end
endmodule
module gate(r0, r1, g0, g1);
input r0;
input r1;
output g0;
output g1;
reg g0;
reg g1;
always @* begin
g0 = 1'b0;
g1 = 1'b0;
casez ({r1, r0})
2'b1?: g1 = 1'b1;
2'b?1: g0 = 1'b1;
default: begin g0 = 1'b0; g1 = 1'b0; end
endcase
end
endmodule
EOV
hierarchy -check
proc
opt
miter -equiv -flatten -make_outputs gold gate m
hierarchy -top m
sat -prove trigger 0 -verify m
log PASS: overlapping casez matches the priority chain{r1, r0} reads 11 in the casez arbiter. Which grant issues, and why?g1. Item 1? matches first, so source order picks it; the second item never sees the vector.
Proof that the casez form and the if-else chain are the same function on every input. The testbench only samples the vectors it runs.