A case on 1'b1 with one item per select bit looks parallel, but it is not: Yosys evaluates the items top to bottom and the first match wins, exactly like an if and else-if chain. The genuinely parallel circuit is the third form here: a one-hot AND-OR that masks each byte with its select bit and ORs the results. It agrees with the chain only while at most one select bit is high.
The three forms below share ports, widths and the zero default: (a) the priority chain, (b) the same function as case (1'b1), and (c) the one-hot AND-OR. Form (b) proves equal to (a) on every vector. Form (c) proves equal only while at most one select bit is high, via a decoder wrapper that drives the select through its five legal values.
Forms (a) and (b) prove equal on every vector, and form (c) only under the decoder wrapper. The generic counts are 4 select cells for the chain, 4 select cells for the case spelling, and 4 $and, 3 $or for the AND-OR.
The script has nine phases and one PASS line. Phases one to three elaborate each form and record ltp, stat and the JSON netlist. Phases four and five prove the priority pair equal and the AND-OR equal under the decoder wrapper. Phases six to eight map the three forms with a loose target. Phase nine elaborates the incomplete case (1'b1) seven ways plus the if-chain twin.
read_verilog <<EOV
module prio_chain (
input wire [3:0] s,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] d,
output reg [7:0] y
);
always @* begin
if (s[0]) y = a;
else if (s[1]) y = b;
else if (s[2]) y = c;
else if (s[3]) y = d;
else y = 8'd0;
end
endmodule
EOV
hierarchy -check -top prio_chain
proc
opt
tee -o ltp_chain.txt ltp
tee -o stat_chain_generic.txt stat
write_json net_chain_generic.json
select -assert-none t:$dlatch
select -assert-min 1 t:$mux t:$pmux %u
design -save d_chain
design -reset
read_verilog <<EOV
module parallel_sel (
input wire [3:0] s,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] d,
output reg [7:0] y
);
always @* begin
case (1'b1)
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
default: y = 8'd0;
endcase
end
endmodule
EOV
hierarchy -check -top parallel_sel
proc
opt
tee -o ltp_par.txt ltp
tee -o stat_par_generic.txt stat
write_json net_par_generic.json
select -assert-none t:$dlatch
select -assert-min 1 t:$mux t:$pmux %u
design -save d_par
design -reset
read_verilog <<EOV
module onehot_ao (
input wire [3:0] s,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] d,
output wire [7:0] y
);
assign y = ({8{s[0]}} & a) | ({8{s[1]}} & b) | ({8{s[2]}} & c) | ({8{s[3]}} & d);
endmodule
EOV
hierarchy -check -top onehot_ao
proc
opt
tee -o ltp_ao.txt ltp
tee -o stat_ao_generic.txt stat
write_json net_ao_generic.json
select -assert-none t:$dlatch
select -assert-min 1 t:$and t:$or %u
design -save d_ao
design -reset
design -load d_chain
rename prio_chain gold
design -stash m_gold
design -load d_par
rename parallel_sel gate
design -copy-from m_gold -as gold gold
miter -equiv -flatten -make_outputs gold gate m
hierarchy -top m
sat -prove trigger 0 -verify m
design -reset
design -load d_chain
design -copy-from d_ao -as onehot_ao onehot_ao
read_verilog <<EOV
module oh_miter (
input wire [2:0] code,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] d,
output wire trig
);
wire [3:0] s;
assign s = (code == 3'd1) ? 4'b0001 : (code == 3'd2) ? 4'b0010 : (code == 3'd3) ? 4'b0100 : (code == 3'd4) ? 4'b1000 : 4'b0000;
wire [7:0] yg;
wire [7:0] ya;
prio_chain g (.s(s), .a(a), .b(b), .c(c), .d(d), .y(yg));
onehot_ao h (.s(s), .a(a), .b(b), .c(c), .d(d), .y(ya));
assign trig = (yg != ya);
endmodule
EOV
hierarchy -check -top oh_miter
proc
opt
flatten oh_miter
sat -prove trig 0 -verify oh_miter
design -reset
design -load d_chain
read_liberty -lib course.lib
synth -top prio_chain -flatten
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
tee -o abc_chain.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_chain_map.txt stat -liberty course.lib
select -assert-none t:$dlatch
design -reset
design -load d_par
read_liberty -lib course.lib
synth -top parallel_sel -flatten
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
tee -o abc_par.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_par_map.txt stat -liberty course.lib
select -assert-none t:$dlatch
design -reset
design -load d_ao
read_liberty -lib course.lib
synth -top onehot_ao -flatten
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
tee -o abc_ao.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_ao_map.txt stat -liberty course.lib
select -assert-none t:$dlatch
design -reset
read_verilog -sv <<EOV
module q_unique (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always_comb begin
unique case (1'b1)
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
endcase
end
endmodule
EOV
hierarchy -check -top q_unique
proc
write_json net_q_unique.json
select -assert-none t:$dlatch
select -assert-count 1 t:$pmux
design -reset
read_verilog -sv <<EOV
module q_prio (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always_comb begin
priority case (1'b1)
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
endcase
end
endmodule
EOV
hierarchy -check -top q_prio
proc
write_json net_q_prio.json
select -assert-none t:$dlatch
select -assert-min 1 t:$mux
design -reset
read_verilog <<EOV
module q_fconly (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always @* begin
case (1'b1) // synthesis full_case
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
endcase
end
endmodule
EOV
hierarchy -check -top q_fconly
proc
write_json net_q_fconly.json
select -assert-none t:$dlatch
select -assert-min 1 t:$mux
design -reset
read_verilog <<EOV
module q_pconly (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always @* begin
case (1'b1) // synthesis parallel_case
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
endcase
end
endmodule
EOV
hierarchy -check -top q_pconly
proc
write_json net_q_pconly.json
select -assert-count 1 t:$dlatch
select -assert-min 1 t:$pmux
design -reset
read_verilog <<EOV
module q_chainbare (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always @* begin
if (s[0]) y = a;
else if (s[1]) y = b;
else if (s[2]) y = c;
else if (s[3]) y = d;
end
endmodule
EOV
hierarchy -check -top q_chainbare
proc
write_json net_q_chainbare.json
select -assert-count 1 t:$dlatch
design -reset
read_verilog <<EOV
module q_bare (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always @* begin
case (1'b1)
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
endcase
end
endmodule
EOV
hierarchy -check -top q_bare
proc
write_json net_q_bare.json
select -assert-count 1 t:$dlatch
design -reset
read_verilog <<EOV
module q_pragma (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output reg [7:0] y
);
always @* begin
case (1'b1) // synthesis full_case parallel_case
s[0]: y = a;
s[1]: y = b;
s[2]: y = c;
s[3]: y = d;
endcase
end
endmodule
EOV
hierarchy -check -top q_pragma
proc
write_json net_q_pragma.json
select -assert-none t:$dlatch
log PASS: chain and case prove identical and bare-form qualifier and pragma spellings elaborate as recordedElaboration sees the spelling, not the proof. The chain and the case spelling elaborate to the same select structure, while the AND-OR elaborates to masking and mixing gates. Every count below is recorded from the JSON netlists and the ltp reports, all pre-mapping.
Form | Recorded generic cells | Recorded ltp length |
|---|---|---|
(a) if / else-if chain | 4 $mux | 4 |
(b) case (1'b1), same function | 4 $mux | 4 |
(c) one-hot AND-OR | 4 $and, 3 $or | 4 |
Recorded longest paths (generic netlists, ltp counts cells, not delay):
chain
Longest topological path in prio_chain (length=4):
0: \s [3]
1: $4\y[7:0] [0] (via $procmux$3)
2: $3\y[7:0] [0] (via $procmux$15)
3: $2\y[7:0] [0] (via $procmux$24)
4: \y [0] (via $procmux$30)
case (1'b1)
Longest topological path in parallel_sel (length=4):
0: \s [3]
1: $procmux$34_Y [0] (via $procmux$34)
2: $procmux$36_Y [0] (via $procmux$36)
3: $procmux$38_Y [0] (via $procmux$38)
4: \y [0] (via $procmux$40)
and-or
Longest topological path in onehot_ao (length=4):
0: \s [1]
1: $and$<inlined>:9$43_Y [0] (via $and$<inlined>:9$43)
2: $or$<inlined>:9$44_Y [0] (via $or$<inlined>:9$44)
3: $or$<inlined>:9$46_Y [0] (via $or$<inlined>:9$46)
4: \y [0] (via $or$<inlined>:9$48)The two priority spellings are structurally identical, while the AND-OR is a different circuit at a similar depth. Ltp only counts cells on the longest structural path. Either way the unit is cells, never picoseconds.
SystemVerilog's qualifiers are promises about the case, not new logic. unique promises exactly one item matches: disjoint items covering every value. priority promises at least one item matches: full, with overlaps allowed and first-match-wins. Both are checked in simulation and trusted in synthesis. The last phase tests each promise on the incomplete overlapping case (1'b1) with no default, where a bare spelling must hold y.
Spelling on the bare case | Recorded $dlatch | Recorded select cells | Reading |
|---|---|---|---|
bare (no promise) | 1 | 5 $not, 3 $and, 1 $dlatch, 3 $mux | The uncovered value must hold y. |
| 0 | 1 $pmux | Disjoint and full: one bare $pmux, no latch. |
| 0 | 4 $mux | Full with overlaps: the $mux cascade stays. |
| 0 | 4 $mux | Full removes the hold; priority stays. |
| 1 | 5 $not, 3 $and, 1 $dlatch, 1 $pmux | Parallel without full: the hold stays. |
both pragmas | 0 | 1 $pmux | Matches |
Every spelling that promises full drops the latch; only the spellings that also promise disjoint collapse the cascade to one bare $pmux, and the if-chain twin records the same latch as the bare case. The frontend help documents no pragma handling, yet the runs show the comments change elaboration. Simulation never sees them: a false parallel_case promise simulates first-match-wins while synthesizing parallel. Read the both-pragmas row as a hazard, not advice.
The if-spelling twin | Recorded $dlatch | Reading |
|---|---|---|
if-chain, no else | 1 | Incompleteness infers a latch in either spelling. |
Mapping is where the proofs meet the library. ABC receives one Boolean function per form: the miter proof says (a) and (b) match everywhere, and the decoder proof says (c) matches only on legal inputs. The mapper knows nothing about the wrapper, so it optimises (c) for all sixteen select patterns. Gates and delay come from the abc summaries, area from the stat -liberty chip totals.
Form | Mapped gates (abc) | Chip area (stat -liberty) | Mapped delay (abc) |
|---|---|---|---|
(a) if / else-if chain | 60 | 149 | 508.21 ps |
(b) case (1'b1), same function | 60 | 149 | 508.21 ps |
(c) one-hot AND-OR | 40 | 104 | 373.48 ps |
The first two rows match because ABC saw one function behind two spellings and built one netlist twice. The third row is the honest surprise: fewer gates at less chip area, because the AND-OR earns its smaller cover by answering the overlap patterns differently, and those are exactly the patterns the proof excludes. Cheaper is a different function that agrees under one-hot.
The AND-OR proof holds only because the wrapper hides the overlaps. The script below drops it: it miters the chain against the AND-OR with no constraints and asks sat for any input that drives the differ flag. A passing run that finds such a model is the counterexample, recorded with overlapping select bits (s = 1100). A failing proof cannot pass the runner.
read_verilog <<EOV
module prio_chain (
input wire [3:0] s,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire [7:0] d,
output reg [7:0] y
);
always @* begin
if (s[0]) y = a;
else if (s[1]) y = b;
else if (s[2]) y = c;
else if (s[3]) y = d;
else y = 8'd0;
end
endmodule
EOV
hierarchy -check -top prio_chain
proc
opt
design -save d_chain
design -reset
read_verilog <<EOV
module onehot_ao (
input wire [3:0] s,
input wire [7:0] a, b, c, d,
output wire [7:0] y
);
assign y = ({8{s[0]}} & a) | ({8{s[1]}} & b) | ({8{s[2]}} & c) | ({8{s[3]}} & d);
endmodule
EOV
hierarchy -check -top onehot_ao
proc
opt
design -save d_ao
design -reset
design -load d_chain
rename prio_chain gold
design -stash m_gold
design -load d_ao
rename onehot_ao gate
design -copy-from m_gold -as gold gold
miter -equiv -flatten -make_outputs gold gate m
hierarchy -top m
flatten m
select -assert-none t:$dlatch t:$dff
tee -o sat_counter.txt sat -set trigger 1 -show-inputs
log PASS: unconstrained miter is satisfiable so the forms differ on overlapsTake s = 4'b0011 by hand to see why the solver succeeds: the chain picks a, the AND-OR yields a|b. Use the AND-OR only where a one-hot guarantee already exists upstream; when priority is the requirement, keep (a) or (b). The default-free qualifier rows are the same gap on the case spelling, already recorded.
Same function and same netlist, so the choice is documentation. The chain states the priority order; the case lists items a reader may wrongly assume are parallel.
The smaller cover is a different function: on overlaps it mixes bytes where the chain picks the first. Equality holds only under one-hot.
Every number on this page comes from Yosys 0.70+post runs recorded by the course checker: all three forms run proc and opt plus ltp on the generic netlist with design -save reuse, an unconstrained miter with sat -prove proves the two priority spellings equal, a decoder-wrapper miter proves the AND-OR equal under one-hot, all three run synth with dfflegalize, abc -liberty course.lib and stat -liberty course.lib, and a ninth phase elaborates seven spellings of the incomplete case (1'b1) with no default for their recorded netlists. A second recorded unit miters the chain against the AND-OR with no wrapper and asks sat for an input that drives the differ flag: the satisfying model is the recorded counterexample. Costs are read from those recordings, and the ltp longest-path bodies are shown with the run-numbered header stripped.