Title: ALU shiftReverse includes FN_ROR unconditionally, leaving residual logic when useZbb=false
Summary
In the default RocketCoreParams configuration (useZbb = false), the ALU function code FN_ROR (18, 5'h12) participates in the shift-input mux via shiftReverse, but has no corresponding output mux arm. The result is a small amount of dead wiring in the synthesized netlist.
This is not a correctness issue — the decoder never emits FN_ROR when Zbb is disabled, and the ALU output is identically zero for this fn code. We are reporting this as an observation from formal verification research, in case the team considers it worth addressing.
Details
shiftReverse in the ALU companion object unconditionally includes FN_ROR:
// ALU.scala:64 (companion object — no parameter guard)
def shiftReverse(cmd: UInt) = !cmd.isOneOf(FN_SR, FN_SRA, FN_ROR, FN_BEXT)
This generates an io_fn == 5'h12 comparator in the shin mux of the elaborated RTL (RocketALU.sv), regardless of configuration.
However, the output MuxLookup only includes FN_ROR -> rotout inside the if (coreParams.useZbb) guard:
// ALU.scala:163-174
val out = MuxLookup(io.fn, shift_logic_cond)(Seq(
FN_ADD -> io.adder_out,
FN_SUB -> io.adder_out
) ++ (if (coreParams.useZbb) Seq(
...
FN_ROL -> rotout,
FN_ROR -> rotout, // only present when useZbb=true
) else Nil))
And the decoder (ZbbDecode in IDecode.scala:466) is similarly gated:
// RocketCore.scala:243
(if (coreParams.useZbb) Seq(new ZbbDecode, ...) else Nil)
So fn=18 is dead from both ends: the decoder never produces it, and the output mux never selects it.
Verification
We confirmed this with Z3 on the Yosys-generated SMT2 model of RocketALU.sv (from commit 885dd59, CIRCT firtool-1.62.1, default params):
- Asserting
io_out != 0 with io_fn = 5'b10010 returns UNSAT for both dw=1 (DW_64) and dw=0 (DW_32), confirming the output is identically zero over all 2^129 input combinations.
An exhaustive scan of all 32 fn codes shows fn=0x12 is the only dead code that leaves residual hardware in the shin mux. All other dead fn codes (e.g., FN_UNARY, FN_ROL, FN_MAX/FN_MIN) are cleanly eliminated because they have no unconditional references.
Impact
- Correctness: None. The ALU produces zero, and no decode path triggers it.
- Area: Minimal. One 5-bit comparator + one OR gate in the shin mux select. Likely optimized by downstream synthesis tools.
- Timing: Negligible.
Possible fix
Move the FN_ROR reference in shiftReverse behind the same parameter guard:
// Option A: inline in class ALU (parameter-aware)
val shin = Mux(!io.fn.isOneOf(
Seq(FN_SR, FN_SRA) ++
(if (coreParams.useZbs) Seq(FN_BEXT) else Nil) ++
(if (coreParams.useZbb) Seq(FN_ROR) else Nil)
: _*), Reverse(shin_r), shin_r)
Or keep the current behavior — it is functionally correct and the overhead is negligible.
Environment
- rocket-chip commit:
885dd59 (chipsalliance/rocket-chip, Feb 25 2026)
- CIRCT: firtool-1.62.1
- Configuration: default
RocketCoreParams() (useZbb=false, useZbs=false)
- Verification: Yosys 0.38+ → SMT2 → Z3 4.12+
Title: ALU
shiftReverseincludesFN_RORunconditionally, leaving residual logic whenuseZbb=falseSummary
In the default
RocketCoreParamsconfiguration (useZbb = false), the ALU function codeFN_ROR(18,5'h12) participates in the shift-input mux viashiftReverse, but has no corresponding output mux arm. The result is a small amount of dead wiring in the synthesized netlist.This is not a correctness issue — the decoder never emits
FN_RORwhen Zbb is disabled, and the ALU output is identically zero for this fn code. We are reporting this as an observation from formal verification research, in case the team considers it worth addressing.Details
shiftReversein theALUcompanion object unconditionally includesFN_ROR:This generates an
io_fn == 5'h12comparator in theshinmux of the elaborated RTL (RocketALU.sv), regardless of configuration.However, the output
MuxLookuponly includesFN_ROR -> rotoutinside theif (coreParams.useZbb)guard:And the decoder (
ZbbDecodeinIDecode.scala:466) is similarly gated:So fn=18 is dead from both ends: the decoder never produces it, and the output mux never selects it.
Verification
We confirmed this with Z3 on the Yosys-generated SMT2 model of
RocketALU.sv(from commit885dd59, CIRCT firtool-1.62.1, default params):io_out != 0withio_fn = 5'b10010returns UNSAT for bothdw=1(DW_64) anddw=0(DW_32), confirming the output is identically zero over all 2^129 input combinations.An exhaustive scan of all 32 fn codes shows fn=0x12 is the only dead code that leaves residual hardware in the shin mux. All other dead fn codes (e.g.,
FN_UNARY,FN_ROL,FN_MAX/FN_MIN) are cleanly eliminated because they have no unconditional references.Impact
Possible fix
Move the
FN_RORreference inshiftReversebehind the same parameter guard:Or keep the current behavior — it is functionally correct and the overhead is negligible.
Environment
885dd59(chipsalliance/rocket-chip, Feb 25 2026)RocketCoreParams()(useZbb=false,useZbs=false)