This task
This text quotes sky130 numbers and compares the designs on sky130, the default library; the score, the boards and the charts of this page are on ASAP7, where the order of the designs can differ.
IEEE 754 division for every binary format at once: the exponent width W and the precision P are
parameters, a value is W + P bits, and the divider must be right for every W ≥ 2 and P ≥ 2
(binary16 is (5, 11), bfloat16 (8, 8), binary32 (8, 24)). Rounding is to nearest with ties to even,
subnormals are kept, and every NaN result is the format's canonical quiet NaN, exactly as the trusted
function SvGolf.IEEE754.divide says.
Run-time / % ** are banned; + - * and the comparisons are allowed. The score is taken at (W, P) = (5, 11). The first proved reference, a
word-level netlist with the normalizer and the restoring steps as generate loops, has 9675.5 µm² and a
38.0 ns critical path on sky130 (2166.076 GE, depth 289); par is the proved radix-4 SRT
divider, 12 357 µm² at 27.6 ns, 340 950 µm²·ns. Each proof covers every format and
every pair of operands.
Interface #
Write a module with exactly this header: port names, directions, widths and order matter, and so do the module's name and its parameters.
module fdiv #(parameter int W = 5, parameter int P = 11) (
input logic [W+P-1:0] a,
input logic [W+P-1:0] b,
output logic [W+P-1:0] q
);| port | direction | width (bits) |
|---|---|---|
a | input | W+P |
b | input | W+P |
q | output | W+P |
The trusted statement #
A proof must establish the task's trusted statement, the constant SvGolf.Tasks.FdivP.Statement of Spec.lean (module tasks.fdivp.Spec). Below it is split into the properties a circuit must have, one card each: what the property guarantees in plain words, and its exact Lean text. Every proved reference has all of them. The last tab, what does not count, lists the designs the checker rejects.
Properties
A design meets the trusted statement exactly when, for every format (W, P) with 2 ≤ W, 2 ≤ P and W + P + 1 < 2^31, it has all of the properties below. Lean checks that, together, they say exactly what the statement says, nothing less and nothing more (the theorem statement_iff_properties).
PARAMS_IN_RANGE is the range the statement covers, not a property: every other card must hold at each value in it.
PARAMS_IN_RANGErangeThe formats the statement covers: every exponent width W ≥ 2 and precision P ≥ 2 with W + P + 1 < 2^31 (so that the widths W + P and W + P + 1, int expressions of the module, stay below 2^31, the values an int holds).
The statement covers every binary floating-point format with an exponent field of W ≥ 2 bits and a precision of P ≥ 2 significand bits (the hidden bit included): binary16 (W = 5, P = 11, the scoring point), bfloat16 (8, 8), binary32 (8, 24), binary64 (11, 53) and every other with W + P + 1 < 2^31 (the module's widths, such as W + P, are int expressions, and an int holds no value of 2^31 or more). One proof covers all of them, and every property below must hold at each format.
/-- The formats the statement covers: every exponent width `W ≥ 2` and precision `P ≥ 2` with
`W + P + 1 < 2^31` (so that the widths `W + P` and `W + P + 1`, `int` expressions of the module, stay
below `2^31`, the values an `int` holds). -/
def ParamsInRange (W P : Nat) : Prop :=
2 ≤ W ∧ 2 ≤ P ∧ W + P + 1 < 2 ^ 31INTERFACEExactly these ports, in this order, with these widths.
The module has exactly the input ports a and b (W + P bits each) and exactly the output port q (W + P bits), with these widths, in this order. Nothing is missing and nothing is extra: an extra input could serve as a hidden mode pin, and the checker and the scoring tools drive and read the design by these names and widths.
/-- Exactly these ports, in this order, with these widths. -/
def Interface (W P : Nat) (d : Design2) : Prop :=
inputPorts d = [("a", W + P), ("b", W + P)] ∧ outputPorts d = [("q", W + P)]UNCLOCKEDNo process runs at a clock edge (no always_ff, no always @(posedge …)).
No process of the design runs at a clock edge: no always_ff, no always @(posedge …), no asynchronous-reset block; only continuous assignments and always_comb blocks. The task is combinational, so it never needs one. The rule closes a gap between Lean's model of SystemVerilog, which the proof is about, and real tools: the model runs every clocked block once per cycle whatever its clock does, so a design that registers correct outputs on a clock nothing drives would look right there, while a simulator sees a clock that never ticks and synthesis removes the registers.
/-- No process runs at a clock edge (no `always_ff`, no `always @(posedge …)`). -/
def Unclocked (d : Design2) : Prop :=
∀ p ∈ d.processes.toList, p.isEdgePhase = falseLOOP_FREENo combinational loop: the design lowers to continuous assigns (Design2.lowerComb) that are ranked (Acyclic): each reads only what lower-ranked ones write.
The design has no combinational loop: written as continuous assignments (each always_comb block becomes one), its processes can be ranked so that each reads only what lower-ranked ones write. A latch (an always_comb block that keeps a value on some path) is refused with it. Lean's model starts every signal at x and settles, so it would read a loop at one state, while a circuit powers up in any 0/1 state the loop can hold and keeps it; the rule removes that question instead of answering it. The ranking is of processes, not bits, so a process that reads a part of a signal it writes itself is refused too, even when no bit depends on itself: write such bits as separate assignments.
/-- No combinational loop: the design lowers to continuous assigns (`Design2.lowerComb`) that are
ranked (`Acyclic`): each reads only what lower-ranked ones write. -/
def LoopFree (d : Design2) : Prop :=
∃ d', d.lowerComb = some d' ∧ Acyclic d'TERMINATESUnder every schedule and every stimulus, the run completes.
Whatever order the simulator picks for processes that are ready at the same moment (the schedule), and whatever values the inputs take, simulating the design completes: every cycle settles. A combinational loop that oscillates fails this, and so does a design the tools could not read. It is also what gives the next property its teeth: that one is about completed runs, and a design with no completed run would satisfy it without computing anything.
/-- Under every schedule and every stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
∀ (σ : ScheduleOracle) (stim : List SvState), ∃ tr, Runs2 d σ stim trCOMPUTES_QUOTIENTIn every completed run, every cycle whose stimulus drives a and b with known values ends with q holding the IEEE 754 quotient a / b in the format (W, P), rounded to nearest, ties to even (fdivBits).
In every cycle in which the inputs a and b are driven with known 0/1 values, the output q settles to the IEEE 754 quotient a / b of the two bit patterns in the format (W, P), rounded to nearest with ties to even: correctly rounded, with subnormal results exact (no flush to zero), overflow to infinity, and zeros, infinities and NaNs handled as the standard prescribes. Every NaN result is the one canonical quiet NaN (0x7E00 in binary16), so the result is a function of the operand bits. The outputs must be fully known 0/1 values in every cycle of every run, whatever the earlier cycles were, so they cannot depend on history.
/-- In every completed run, every cycle whose stimulus drives `a` and `b` with known values ends
with `q` holding the IEEE 754 quotient `a / b` in the format `(W, P)`, rounded to nearest, ties
to even (`fdivBits`). -/
def ComputesQuotient (W P : Nat) (d : Design2) : Prop :=
d ⊨₂ spec2 fun stim tr =>
∀ (c : Nat) (inputs st : SvState), stim[c]? = some inputs → tr[c]? = some st →
∀ (a b : BitVec (W + P)),
HoldAll inputs [("a", W + P), ("b", W + P)] (a, b, ()) →
HoldAll st [("q", W + P)] (fdivBits W P a b, ())Definitions
The names the properties use, each with its Lean text. Trusted text is what a proof is about; a helper of Properties.lean is not trusted: Lean checks it as part of statement_iff_properties.
This task's trusted text
fdivBitsSpec.leanfdivBits W P a b: the IEEE 754 division of the spec, divide ⟨W, P⟩ roundTiesToEven a b, on (W + P)-bit patterns (the casts only restate the width as W + P).
/-- **The function of the task**: `divide ⟨W, P⟩ .roundTiesToEven` on `(W + P)`-bit patterns,
for `2 ≤ W` and `2 ≤ P` (the spec's `Format` requires both). The `BitVec.cast`s only transport a
pattern along the equation `Format.k = W + P` (they leave `toNat` unchanged:
`fdivBits_toNat`); outside the range the function is `0`, which no statement looks at. -/
def fdivBits (W P : Nat) (a b : BitVec (W + P)) : BitVec (W + P) :=
if h : 2 ≤ W ∧ 2 ≤ P then
let f : Format := ⟨W, P, h.1, h.2⟩
have hk : f.k = W + P := k_eq W P (by omega)
(divide f .roundTiesToEven (a.cast hk.symm) (b.cast hk.symm)).cast hk
else 0#(W + P)divideIEEE754.leanThe trusted IEEE 754-2019 division on bit patterns, for any format and rounding mode: the special cases first, then the exact quotient rounded once.
/-- **IEEE 754-2019 division** `division(x, y)` (§5.4.1) of format `f` under rounding-direction
attribute `mode`, on bit patterns.
The special cases, in order:
* any NaN operand (quiet or signaling) → the canonical NaN (§6.2, NaN policy above);
* `division(∞, ∞)` and `division(0, 0)` are invalid operations (§7.2) → the canonical NaN;
* `division(∞, y)` for finite `y`, zero included → `∞`, exact (§6.1);
* `division(x, ∞)` for finite `x`, zero included → `0`, exact (§6.1);
* `division(x, 0)` for finite nonzero `x` → `∞`, the divideByZero exception (§7.3);
* `division(0, y)` for finite nonzero `y` → `0`, exact.
In all non-NaN cases the sign of the result is the exclusive OR of the operands' signs (§6.3).
Otherwise `x = (−1)^sx × 2^qx × cx` and `y = (−1)^sy × 2^qy × cy` are finite nonzero, and the
result is the exact quotient rounded (§4.3, §5.1: as if computed with unbounded range and
precision, then rounded): `|x| / |y| = (nx / dx) / (ny / dy) = (nx × dy) / (dx × ny)`
where `nx / dx` is `|x|` as a fraction (`Datum.value?`). -/
def divide (f : Format) (mode : RoundingMode) (a b : BitVec f.k) : BitVec f.k :=
match decode f a, decode f b with
| .nan _, _ | _, .nan _ => canonicalNaN f
| .inf _, .inf _ => canonicalNaN f
| .zero _, .zero _ => canonicalNaN f
| .inf sx, .zero sy | .inf sx, .finite sy _ _ => infinity f (sx ^^ sy)
| .zero sx, .inf sy | .finite sx _ _, .inf sy => zero f (sx ^^ sy)
| .finite sx _ _, .zero sy => infinity f (sx ^^ sy)
| .zero sx, .finite sy _ _ => zero f (sx ^^ sy)
| .finite sx qx cx, .finite sy qy cy =>
-- |x| = nx / dx and |y| = ny / dy exactly (Datum.value? without the sign)
let nx := cx * 2 ^ qx.toNat
let dx := 2 ^ (-qx).toNat
let ny := cy * 2 ^ qy.toNat
let dy := 2 ^ (-qy).toNat
round f mode (sx ^^ sy) (nx * dy) (dx * ny)FormatIEEE754.leanA binary interchange format: the exponent-field width w and the precision p, both at least 2; a pattern has 1 + w + (p − 1) = w + p bits.
/-- A **binary interchange format** (IEEE 754-2019 §3.3, §3.4 and Table 3.5), given by
* `w` — the width in bits of the biased-exponent field `E`, and
* `p` — the precision: the number of significand digits, *including* the implicit leading bit.
binary16 is `w = 5, p = 11`; binary32 is `w = 8, p = 24`; binary64 is `w = 11, p = 53`.
The side conditions `2 ≤ w`, `2 ≤ p` exclude degenerate parameter choices (Table 3.5's
formats all satisfy them); they are discharged automatically for literals. -/
structure Format where
/-- Width of the biased-exponent field `E` (§3.4). -/
w : Nat
/-- Precision `p`: significand digits including the implicit bit (§3.3). -/
p : Nat
hw : 2 ≤ w := by decide
hp : 2 ≤ p := by decideStatementSpec.leanThe trusted challenge statement that these properties restate, part by part.
/-- **The challenge statement** for the two-parameter design family
`Submission.design.sem : Nat → Nat → Design2`: at every `W, P ≥ 2` in range the design satisfies the
fixed-size task at that format. A submission proves
`SvGolf.Tasks.FdivP.Statement Submission.design.sem`. -/
abbrev Statement (sem : Nat → Nat → LeanModels.Sv.Design2) : Prop :=
∀ W P, inRange W P → (task W P).StatementFixed (sem W P)taskSpec.leanThe task as data: the parameter range, the ports at each parameter value, and the function the outputs must compute.
/-- The task at the format `⟨W, P⟩`, as a fixed-size `CombTask` (its own parameter is ignored and
taken at `0`, as in `CombTask.StatementFixed`): inputs `a b : BitVec (W + P)`, output
`q = fdivBits W P a b`. -/
def task (W P : Nat) : CombTask where
inRange K := K = 0
inputs _ := [("a", W + P), ("b", W + P)]
outputs _ := [("q", W + P)]
fn _ := fun (a, b, ()) => (fdivBits W P a b, ())The shared trusted base
CombTask.SatisfiedAtTask.leanThe trusted form of a combinational statement at one parameter value: the interface, then no clock and termination, then the function.
/-- The statement at one parameter value: interface; no clocked process, no
combinational loop and termination; function. Conjunct 2 is the triple
`Unclocked d ∧ LoopFree d ∧ Terminates2 d`. -/
def SatisfiedAt (N : Nat) (d : Design2) : Prop :=
t.Interface N d ∧ (Unclocked d ∧ LoopFree d ∧ Terminates2 d) ∧ t.Computes N dinputPortsTask.leanThe design's input ports, each with its declared width, in declaration order.
/-- The input ports of `d` with their declared widths, in declaration order.
`instantiate2` lists the ports first, in port-list order. A declaration is
an input port iff its `isInput` flag is set. -/
def inputPorts (d : Design2) : List Sig :=
d.decls.toList.filterMap fun dc => if dc.isInput then some (dc.name, dc.width) else noneoutputPortsTask.leanThe design's output ports, each with its declared width, in declaration order.
/-- The output ports of `d` with their declared widths, in declaration order.
A declaration is an output port iff its `isOutput` flag is set. -/
def outputPorts (d : Design2) : List Sig :=
d.decls.toList.filterMap fun dc => if dc.isOutput then some (dc.name, dc.width) else noneHoldAllTask.leanHoldAll st ports values: in the state st, every listed port holds its value as a known bit vector (no x, no z) of exactly the port's width.
/-- `HoldAll st sigs v`: in state `st`, every port `(n, w)` of `sigs` is bound
to the fully known `w`-bit vector that `v` assigns it. -/
def HoldAll (st : SvState) : (sigs : List Sig) → Vals (sigs.map Prod.snd) → Prop
| [], _ => True
| (n, _) :: sigs, v => SvState.lookup st n = some (LVec.ofBitVec v.1) ∧ HoldAll st sigs v.2⊨₂Spec2.leand ⊨₂ P: in every completed run of the design d, under every schedule and every stimulus, the stimulus and the trace satisfy P.
/-- `d ⊨₂ P` — for **every** legal schedule, every stimulus, and every
completed run (`Runs2`), the trace satisfies `P`. Introduce from a raw
∀-fuel fact with `Models2.of_run`; eliminate against a concrete run with
`Models2.run` / `Models2.runs`. Says nothing about whether runs complete —
pair it with `Terminates2`. -/
def Models2 (d : Design2) (P : TraceProp2) : Prop :=
∀ (σ : ScheduleOracle) (stim tr : List SvState), Runs2 d σ stim tr → P d stim tr
@[inherit_doc] scoped infix:50 " ⊨₂ " => Models2spec2Spec2.leanTurns a property of a stimulus (one input entry per cycle) and a trace (one snapshot of every signal per cycle) into the form ⊨₂ takes.
/-- Lift a design-agnostic stimulus/trace predicate into `⊨₂`
(`d ⊨₂ spec2 fun stim tr => …`). -/
def spec2 (P : List SvState → List SvState → Prop) : TraceProp2 := fun _ stim tr => P stim trRuns2Spec2.leanRuns2 d σ stim tr: simulating d under the schedule σ on the stimulus stim completes, with the trace tr.
/-- The fuel-abstracted Design2 run judgment: *some* fuel completes the run
of `d` under schedule `σ` and stimulus `stim` with trace `tr`. The only place
fuel appears in a Design2 spec. -/
def Runs2 (d : Design2) (σ : ScheduleOracle) (stim tr : List SvState) : Prop :=
∃ fuel, run2 d σ fuel stim = .ok trScheduleOracleSemantics.leanA legal schedule: the order in which the simulator runs the processes that are ready at the same moment. The statement quantifies over all of them.
/-- A legal schedule: at invocation `k`, orders the ready process list.
`choose_perm` is the legality proof — every invocation is a permutation of
the ready list — so `∀ σ : ScheduleOracle` ranges over exactly the legal
schedules. See the module docstring for the invocation-counter protocol. -/
structure ScheduleOracle where
/-- Invocation counter and ready process indices in, execution order out. -/
choose : Nat → List Nat → List Nat
/-- Every invocation yields a permutation of the ready list. -/
choose_perm : ∀ (k : Nat) (ready : List Nat), (choose k ready).Perm readyProcess2.isEdgePhaseSem2.leanTrue for the processes that run at the clock edge: always_ff, always @(posedge …) and asynchronous-reset blocks.
/-- Edge-phase processes: every posedge-clocked block, INCLUDING the
async-reset ones (the posedge fires with reset asserted too — the body's
reset branch is what holds the state, pin3 CYCLE 4). -/
def Process2.isEdgePhase : Process2 → Bool
| .alwaysFF _ _ | .alwaysPlain _ _ | .alwaysFFR _ _ _ _ => true
| _ => falseWhat does not count
Designs that try to score without meeting the statement (negatives), or that exploit a place where the proof's reading and the scored netlist could differ (attacks). The checker stops at the first stage that refuses; each design is listed with that stage.
- Refused before any proof is tried: 4 designs (by stage:
extract3,banlist1) - Rejected at the proof: 26 designs (by stage:
solution26)
Refused before any proof is tried
The checker's static stages read the text itself and refuse it: an operator the task bans, a construct that two tools read differently, an unknown (x or z) value that could arise, or a program the language forbids.
rm_pin.sv(negative, stopped atextract): Adds a rounding-mode input that is never read.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, input logic rtz, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulestatus_flag.sv(negative, stopped atextract): Adds aninexactoutput next toq.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q, output logic inexact ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate assign inexact = 1'b0; endmodulewide_q.sv(negative, stopped atextract): The reference withqone bit wider, its top bit always 0.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K] = 1'b0; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulediv_op.sv(negative, stopped atbanlist): The reference with its division steps replaced by the banned run-time/and%.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [2*P+1:0] num; logic [P+1:0] qq; logic rnz; assign nbx = {1'b0, nb_r[P-1]}; assign num = na_r[P-1] << (P + 1); assign qq = num / nb_r[P-1]; assign rnz = (num % nb_r[P-1]) != 0; logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodule
Rejected at the proof
These pass every static check. The proof that comes with each one does not compile, or does not prove the statement: a design that is wrong somewhere in the task's range (or has other ports) has no proof at all, and a proof that leaves a goal unproved is never accepted.
dsh_sticky_short.sv(attack, stopped atsolution): The reference with the denormalizer's sticky test two bits short: wrong on some subnormal results.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != {qm[P:2], 2'b00}) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmoduledsh_wrap64.sv(attack, stopped atsolution): The reference with the denormalizing shift taken modulo 64: right at the scoring format, wrong for exponent widths of 7 and more.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = ((~E[EW-1] & (|E)) ? 0 : (1 - E)) & 63; logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmoduleew_narrow.sv(attack, stopped atsolution): The reference with an exponent register that is too narrow when the precision is large: right at the scoring format, wrong elsewhere.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + 2; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmoduleftz.sv(attack, stopped atsolution): The reference flushing subnormal results to zero.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = (~E[EW-1] & (|E)) ? ({ef, qs[P-1:1]} + inc) : 0; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmoduleinc_tie_odd.sv(attack, stopped atsolution): The reference rounding exact ties to the odd neighbour.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | ~qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_f_minus2.sv(attack, stopped atsolution): The Newton reference with two fraction bits fewer in its working precision.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 2; localparam integer NI = $clog2((P + 9) / 8) + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd45, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + ge1 + ge2; assign rnz = (rm != mb) & (rm != {mb, 1'b0}) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_ge1_const.sv(attack, stopped atsolution): The Newton reference whose correction always adds 1.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 4; localparam integer NI = $clog2((P + 9) / 8) + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd45, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + 1'b1 + ge2; assign rnz = (rm != mb) & (rm != {mb, 1'b0}) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_ni_minus1.sv(attack, stopped atsolution): The Newton reference with one Newton step fewer: right at small precisions only.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 4; localparam integer NI = $clog2((P + 9) / 8) + 0; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd45, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + ge1 + ge2; assign rnz = (rm != mb) & (rm != {mb, 1'b0}) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_no_ge2.sv(attack, stopped atsolution): The Newton reference whose correction stops one short: wrong only where the estimate is two below the quotient, and right on every pair of binary16.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 4; localparam integer NI = $clog2((P + 9) / 8) + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd45, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + ge1; assign rnz = (rm != mb) & (rm != {mb, 1'b0}) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_r0_off.sv(attack, stopped atsolution): The Newton reference with a wrong constant in its initial reciprocal: right at some precisions only.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 4; localparam integer NI = $clog2((P + 9) / 8) + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd47, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + ge1 + ge2; assign rnz = (rm != mb) & (rm != {mb, 1'b0}) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_rnz_no2mb.sv(attack, stopped atsolution): The Newton reference whose sticky bit forgets one remainder: wrong only on rare exact quotients, and right on every pair of binary16.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 4; localparam integer NI = $clog2((P + 9) / 8) + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd45, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + ge1 + ge2; assign rnz = (rm != mb) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulenewton_rnz_nomb.sv(attack, stopped atsolution): The Newton reference whose sticky bit forgets the other remainder, taking some exact quotients for inexact ones.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer F = P + 4; localparam integer NI = $clog2((P + 9) / 8) + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P-1:0] ma, mb; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; logic [P:0] zr; assign zr = '0; logic [NI:0][F:0] r; assign r[0] = {6'd45, zr[P-2:0]} - {mb, 4'd0} + mb; logic [NI-1:0][P+F-1:0] dr; logic [NI-1:0][F:0] u; logic [NI-1:0][2*F:0] ru; genvar k; generate for (k = 0; k < NI; k = k + 1) begin : newton assign dr[k] = mb * r[k]; assign u[k] = ~dr[k][P+F-1:P-1]; assign ru[k] = r[k] * u[k]; assign r[k+1] = ru[k][2*F:F]; end endgenerate logic [P+F-1:0] qp; logic [P+1:0] qf; assign qp = ma * r[NI]; assign qf = qp[P+F-1:F-2]; logic [P+1:0] qb, rm, qq; logic ge1, ge2, rnz; logic [P+1:0] qe; assign qe = ((&a[K-2:T]) | (&b[K-2:T])) ? (qf - a[0] - b[0]) : qf; assign qb = qe * mb; assign rm = {ma[0], zr} - qb; assign ge1 = (rm >= mb); assign ge2 = (rm >= {mb, 1'b0}); assign qq = qe + ge1 + ge2; assign rnz = (rm != {mb, 1'b0}) & (|rm); logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmoduleovf_late.sv(attack, stopped atsolution): The reference testing for overflow one step too late, so the all-ones exponent keeps its fraction.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & (|E[EW-2:W]); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulerr_sticky_dropped.sv(attack, stopped atsolution): The reference with a sticky bit that ignores the division's last remainder.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_drop_carry.sv(attack, stopped atsolution): The SRT reference with one carry of its carry-save remainder dropped.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // one carry of the carry-save row dropped (cy[k][3] replaced by 0). Over W = 2, P = 2..12 exhaustive: wrong on every P (20 of 2^8 pairs at (2,2)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:4], 1'b0, g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_no_cin.sv(attack, stopped atsolution): The SRT reference that forgets the +1 of a negated divisor multiple.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // the +1 of -q * dv (q > 0, the two's complement of the multiple) dropped from the carry vector. Over W = 2, P = 2..12 exhaustive: wrong on every P (72 of 2^8 pairs at (2,2)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], 1'b0, 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_no_corr.sv(attack, stopped atsolution): The SRT reference without its final correction, so a negative remainder leaves the quotient one too high.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // the final correction is missing (qq = u[N], also when the residual is negative). Over W = 2, P = 2..12 exhaustive: right at P = 2, wrong from P = 3 (28 of 2^10 pairs at (2,3)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_otfc_digit.sv(attack, stopped atsolution): The SRT reference whose on-the-fly conversion appends the wrong bits for the digit -1.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // on-the-fly conversion: the digit pair appended to U for q = -1 is 10, not 11. Over W = 2, P = 2..12 exhaustive: wrong on every P (20 of 2^8 pairs at (2,2)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_otfc_um.sv(attack, stopped atsolution): The SRT reference whose on-the-fly conversion takes one digit's decremented quotient from the wrong register.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // on-the-fly conversion: UM' for the digit q = 0 is taken from U instead of UM (g0 for g1). Over W = 2, P = 2..12 exhaustive: right at P = 2, wrong from P = 3 (40 of 2^10 pairs at (2,3)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_qds_t1_d0.sv(attack, stopped atsolution): The SRT reference with another wrong selection constant: right below precision 5.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // a wrong selection constant: t1's leaf at da = 0 is 66 instead of 68 (Wally's mks1[0] 4 -> 2). Over W = 2, P = 2..12 exhaustive: right at P = 2..4 (the bad cells are not reached), wrong from P = 5 (24 of 2^14 pairs at (2,5)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd66)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_qds_t2_d0.sv(attack, stopped atsolution): The SRT reference with one wrong constant in its digit-selection table: right below precision 5, where the bad table cell is never reached.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // a wrong selection constant: t2's leaf at da = 0 is 75 instead of 76 (Wally's mks2[0] 12 -> 11). Over W = 2, P = 2..12 exhaustive: right at P = 2..4 (the bad cell is not reached), wrong from P = 5 (20 of 2^14 pairs at (2,5)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd75)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_qds_tm_d7.sv(attack, stopped atsolution): The SRT reference with a wrong selection constant for negative digits: right below precision 5.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // a wrong selection constant: tm's leaf at da = 7 is 38 instead of 41 (Wally's mksm1[7] -23 -> -26). Over W = 2, P = 2..12 exhaustive: right at P = 2..4 (the bad cells are not reached), wrong from P = 5 (20 of 2^14 pairs at (2,5)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd38 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_stages_m1.sv(attack, stopped atsolution): The SRT reference with one stage, two quotient bits, fewer.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // one stage fewer (N = H radix-4 digits). Over W = 2, P = 2..12 exhaustive: wrong on every P (84 of 2^8 pairs at (2,2)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = |rs; // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulesrt_sticky_sign.sv(attack, stopped atsolution): The SRT reference whose sticky bit takes every negative remainder for an exact quotient.the design, with its licence and provenance notices
// ATTACK for task fdivp: the SRT reference (tasks/fdivp/reference/fdivp_srt.sv) with ONE change. // the sticky bit reads the residual's sign (rnz = ~sign & (rs != 0)): a negative residual is taken for exact. Over W = 2, P = 2..12 exhaustive: right at P = 2, wrong from P = 3 (32 of 2^10 pairs at (2,3)). // // fdiv #(W, P), radix-4 SRT form: a third divider for task fdivp. It is the reference D3 // (tasks/fdivp/reference/fdivp.sv) with its P + 2 restoring steps replaced by an unrolled radix-4 SRT core: digits in // {-2, -1, 0, 1, 2}, a carry-save partial remainder, quotient-digit selection from 7 top bits of the remainder and 3 // bits of the divisor, and on-the-fly conversion. Unpack/classify, the normalizers, the exponent, the denormalizer, the // rounding and the output stage are D3's VERBATIM, so the core has the contract of D3's quotient `qq` and sticky // `|rr[P+2]` (the interface the Newton reference reference/fdivp_newton.sv plugs into as well): // // qq = floor(ma * 2^(P+1) / mb) (P + 2 bits) // rnz = (ma * 2^(P+1) mod mb) != 0 (the sticky of the division) // // for the normalized significands ma, mb in [2^(P-1), 2^P). // // Proved for every W, P >= 2 (reference/fdivp_srt.lean): the selection table is checked cell by cell by kernel // `decide`, and the invariant over the N stages gives the contract above (section SrCore there). // // ---- Provenance // The SRT core is adapted from CORE-V Wally (https://github.com/openhwgroup/cvw, commit // c1e386b5d1155e92e21593a7986999274f086729), src/fpu/fdivsqrt/: fdivsqrtiter.sv (the generate loop of stages), // fdivsqrtstage4.sv (one radix-4 step), fdivsqrtuslc4cmp.sv (the selection by comparison with divisor-dependent // constants), fdivsqrtuotfc4.sv (on-the-fly conversion), fdivsqrtpostproc.sv (the final correction and sticky), // src/generic/csa.sv and src/generic/mux.sv (mux2, written here as `?:`). Written by David Harris, Katherine Parry, // Cedar Turek; modified by Kevin Kim, Alessandro Maiuolo, James Stine. // Copyright (C) 2021-26 Harvey Mudd College & Oklahoma State University // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // (Apache License 2.0, https://www.apache.org/licenses/LICENSE-2.0, with the Solderpad Hardware License v2.1 // exception, https://solderpad.org/licenses/SHL-2.1/). The rest of this file (D3) is svGolf's. // The license texts ship with the reference: tasks/fdivp/reference/LICENSES/ (Apache-2.0.txt, SHL-2.1.txt). // The algorithm is the textbook one (M. Ercegovac, T. Lang, "Digital Arithmetic", 2004, ch. 5; D. Harris et al., // "RISC-V System-on-Chip Design", 2025, the Wally divider chapter). The unmodified Wally files were first run through // the svGolf source gate, extractor and banlist; what they refuse is recorded in tests/fdivp/results/srt_S0.md. // // Changes to the Wally code, each with its reason: // 1. Unrolled and combinational: Wally runs DIVCOPIES stages per clock between registers (fdivsqrtiter, with the // start muxes and flops); here all N = H + 1 stages are one generate loop and the initial values (Wally's X, 0, // initU = 0, initUM = -1) are wired into stage 0. Reason: fdivp is one combinational module. // 2. Division only: the square-root paths (SqrtE, fdivsqrtfgen4's F, Smsbs, the j0/j1 first-step specials, the sqrt // arms of the selection) are removed. Reason: the task divides. // 3. The struct parameter `cvw_t P` (DIVb, ...) and `import cvw::*` are replaced by integer localparams of the task's // W and P. Reason: the extractor refuses the struct parameter and its member accesses; the proof fragment reads // integer localparams (svgolf/PROVING.md section 4). // 4. Scaling: Wally's Q4.DIVb vectors with X, D in [1, 2) become RW = P + 6 bit integer vectors: the divisor's leading // one sits at bit P + 2 with 3 zero bits below it (so the selection window [P+5:P-2] exists for P = 2 and 3), and // the dividend is pre-shifted right by XS (0 for odd P, 1 for even P), so that the N-digit integer quotient is // floor(2^(P+1) ma / mb) exactly, at any parity of P. Reason: the interface above, with an affine stage count. // The pre-shift is a part-select of the zero-padded copy xw = 16 ma at the bounds [RW+XS:1+XS], not a shift by // XS. Reason: the proof fragment reads affine part-select bounds but not a shift by a parameter amount. // 5. The instances (csa, mux2, fdivsqrtuslc4cmp, fdivsqrtuotfc4) are inlined as continuous assigns. // Reason: the proof fragment has no instances. // 6. Selection: the $signed comparisons of the 7-bit estimate with the constants become unsigned comparisons of the // estimate with its sign bit flipped against the constants + 64 (the same order). The constant arrays mks2/mks1/ // mks0/mksm1 indexed by the divisor bits (a dynamic index) become four 3-level `?:` trees on those 3 bits, // continuous assigns computed once (they depend on the divisor only). The constants are Wally's, unchanged. // Reason: signed declarations and arithmetic and dynamic indices are outside the proof fragment, and a procedural // `case` table would take the design off the combinational route the proofs of D3 and Newton use. // 7. The divisor-multiple mux: Wally's `case (udigit)` with `default: Dsel = 'x` becomes a priority `?:` chain on the // four comparison results (uslc4cmp's own if-else order), so no one-hot digit vector is formed. Reason: the // source gate refuses x literals. // 8. The negative multiples -D and -2D: Wally adds ~D (all bits) with the +1 carried in at bit 0; here the multiples // keep the 3 low bits zero ({111, ~mb, 000} and {11, ~mb, 1000}) and the +1 enters the carry vector at bit 3, // so the residual's pad bits stay constant zero. Reason: area (a constant column costs no gates). // 9. On-the-fly conversion: Wally's positional form (U | K, UM | K with K from a per-cycle thermometer register C) // becomes the shift-append form of the same five cases (Ercegovac-Lang): U' = 4U + q, UM' = 4U + q - 1, modulo // 2^(P+2); C and K are gone. Reason: in an unrolled loop the digit position is the stage index, and an append is // a concatenation of part-selects with affine bounds. // 10. Final correction and sticky (fdivsqrtpostproc): kept, as qq = (the sign of WS + WC) ? UM : U and // rnz = (WS + WC != 0), the zero test made on the sum the sign needs anyway (Wally's aplusbeq0 tests WS + WC == 0 // without the carry chain; it is not used). Reason: one adder for both. // // ---- The core, in numbers (dv = mb * 8, the divisor; ws[0] = ma * 2^(3-XS), the dividend) // H = (P + 2) / 2, XS = 2H - P - 1, N = H + 1 digits, RW = P + 6. // Stage k: the estimate y = (ws[k][P+5:P-2] + wc[k][P+5:P-2]) >> 1 (Q4.3 in units of the divisor's leading one) and // the 3 divisor bits A = dv[P+1:P-1] select q in {-2..2} (Wally's constants); the remainder R = ws + wc becomes // 4 * (R - q * dv) by one carry-save row; the digits accumulate on the fly in U (= the digits so far) and UM = U - 1. // The selection keeps |R| <= 8/3 dv (checked exactly over every table cell, tests/fdivp/results/srt_S0.md), so after // N steps 2^(P+1) ma / mb = U + R / (4 dv) with |R / (4 dv)| <= 2/3: qq = R < 0 ? UM : U, rnz = R != 0. module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; localparam integer H = (P + 2) / 2; // 2H >= P + 1 quotient bits after the first digit localparam integer XS = 2 * H - P - 1; // dividend pre-shift: 0 for odd P, 1 for even P (2H - XS = P + 1) localparam integer N = H + 1; // radix-4 digits localparam integer RW = P + 6; // remainder width: 4 integer bits over the divisor's P + 2 // ---- unpack and classify (D3) logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0]) & ~eb_nz & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); // ---- normalizers (D3): P - 1 one-bit stages; the EW-bit register counts the shifts down logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate // the normalized significands (top bit set for finite nonzero operands; 0 for a zero, whose quotient is unused) logic [P-1:0] ma, mb, mbn; assign ma = na_r[P-1]; assign mb = nb_r[P-1]; assign mbn = ~mb; // ---- divisor multiples (Wally's D, D2, and -D, -2D less the +1 that the carry vector takes at bit 3) logic [RW-1:0] dv, d2, nd1, nd2, zw; logic [RW+1:0] xw; // 16 ma: ws[0] = xw[RW+XS:1+XS] = ma * 2^(3-XS) assign dv = {3'b000, mb, 3'b000}; assign d2 = {2'b00, mb, 4'b0000}; assign nd1 = {3'b111, mbn, 3'b000}; assign nd2 = {2'b11, mbn, 4'b1000}; assign zw = '0; assign xw = {4'b0000, ma, 4'b0000}; // ---- selection constants (Wally fdivsqrtuslc4cmp's mks2/mks1/mks0/mksm1 + 64), by the 3 divisor bits after the // leading one: each a 3-level ?: tree on da[2], da[1], da[0]. By da = 0..7: // t2 76 78 80 81 82 84 86 87 t1 68 68 70 70 70 72 72 72 // t0 60 60 58 58 58 56 56 56 tm 51 50 48 47 46 44 42 41 logic [2:0] da; logic [6:0] t2, t1, t0, tm; assign da = dv[P+1:P-1]; assign t2 = da[2] ? (da[1] ? (da[0] ? 7'd87 : 7'd86) : (da[0] ? 7'd84 : 7'd82)) : (da[1] ? (da[0] ? 7'd81 : 7'd80) : (da[0] ? 7'd78 : 7'd76)); assign t1 = da[2] ? (da[1] ? (da[0] ? 7'd72 : 7'd72) : (da[0] ? 7'd72 : 7'd70)) : (da[1] ? (da[0] ? 7'd70 : 7'd70) : (da[0] ? 7'd68 : 7'd68)); assign t0 = da[2] ? (da[1] ? (da[0] ? 7'd56 : 7'd56) : (da[0] ? 7'd56 : 7'd58)) : (da[1] ? (da[0] ? 7'd58 : 7'd58) : (da[0] ? 7'd60 : 7'd60)); assign tm = da[2] ? (da[1] ? (da[0] ? 7'd41 : 7'd42) : (da[0] ? 7'd44 : 7'd46)) : (da[1] ? (da[0] ? 7'd47 : 7'd48) : (da[0] ? 7'd50 : 7'd51)); // ---- N radix-4 SRT stages logic [N:0][RW-1:0] ws, wc; // carry-save remainder (Wally WS, WC) logic [N:0][P+1:0] u, um; // on-the-fly quotient U and U - 1 (Wally U, UM), mod 2^(P+2) logic [N-1:0][7:0] es; // top 8 bits of ws + wc (Wally PreWmsbs, Q4.4) logic [N-1:0][6:0] yb; // the Q4.3 estimate with its sign bit flipped (Wally Wmsbs + 64) logic [N-1:0] g2, g1, g0, gm; // estimate >= each constant: q = 2, >= 1, >= 0, >= -1 logic [N-1:0][RW-1:0] mm, sm, cy; // the multiple -q * dv, carry-save sum and carry logic [N-1:0] uq1, uq0, um1, um0; // the appended digit pairs: q mod 4 and (q - 1) mod 4 logic [N-1:0][P-1:0] us, ums; // the prefix each appends to: U or UM assign ws[0] = xw[RW+XS:1+XS]; assign wc[0] = '0; assign u[0] = '0; assign um[0] = '1; genvar k; generate for (k = 0; k < N; k = k + 1) begin : srt // selection (Wally fdivsqrtuslc4cmp, division) assign es[k] = ws[k][P+5:P-2] + wc[k][P+5:P-2]; assign yb[k] = es[k][7:1] ^ 7'b1000000; assign g2[k] = (yb[k] >= t2); assign g1[k] = (yb[k] >= t1); assign g0[k] = (yb[k] >= t0); assign gm[k] = (yb[k] >= tm); // one carry-save step 4 * (R - q * dv) (Wally fdivsqrtstage4 + csa; the +1 of -q * dv, q > 0, enters at bit 3) assign mm[k] = g2[k] ? nd2 : (g1[k] ? nd1 : (g0[k] ? zw : (gm[k] ? dv : d2))); assign sm[k] = ws[k] ^ wc[k] ^ mm[k]; assign cy[k] = (ws[k] & wc[k]) | (ws[k] & mm[k]) | (wc[k] & mm[k]); assign ws[k+1] = {sm[k][RW-3:0], 2'b00}; assign wc[k+1] = {cy[k][RW-4:3], g1[k], 5'b00000}; // on-the-fly conversion (Wally fdivsqrtuotfc4, shift-append form): // q: 2 1 0 -1 -2 // U' {U,10} {U,01} {U,00} {UM,11} {UM,10} // UM' {U,01} {U,00} {UM,11} {UM,10} {UM,01} assign uq1[k] = g2[k] | ~g0[k]; assign uq0[k] = (g1[k] & ~g2[k]) | (gm[k] & ~g0[k]); assign um1[k] = ~g1[k] & gm[k]; assign um0[k] = g2[k] | (g0[k] & ~g1[k]) | ~gm[k]; assign us[k] = g0[k] ? u[k][P-1:0] : um[k][P-1:0]; assign ums[k] = g1[k] ? u[k][P-1:0] : um[k][P-1:0]; assign u[k+1] = {us[k], uq1[k], uq0[k]}; assign um[k+1] = {ums[k], um1[k], um0[k]}; end endgenerate // ---- final correction and sticky (Wally fdivsqrtpostproc): a negative remainder takes U - 1 logic [RW-1:0] rs; logic [P+1:0] qq; logic rnz; assign rs = ws[N] + wc[N]; assign qq = rs[RW-1] ? um[N] : u[N]; assign rnz = ~rs[RW-1] & (|rs); // ---- quotient normalization (D3): P significand bits and the round bit; st0 = (qq[P+1] & qq[0]) | rnz inline logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; // ---- exponent (D3; two's complement, EW bits): E = ya - yb + emax - adj; emax = 011..1 (W bits) logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); // ---- denormalize, round to nearest even (D3, with the SRT core's sticky rnz) logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | rnz | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; // ---- output (D3): fields by case (nan > inf > zero > overflow > finite) assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmodulezero_by_zero_inf.sv(attack, stopped atsolution): The reference returning infinity for ±0 / ±0 instead of NaN.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); localparam integer K = W + P; localparam integer T = P - 1; localparam integer EW = W + P + 1; logic s, ea_nz, eb_nz, c_nan, c_inf, c_zero; assign s = a[K-1] ^ b[K-1]; assign ea_nz = |a[K-2:T]; assign eb_nz = |b[K-2:T]; assign c_nan = ((&a[K-2:T]) & (|a[T-1:0])) | ((&b[K-2:T]) & (|b[T-1:0])) | ((&a[K-2:T]) & ~(|a[T-1:0]) & (&b[K-2:T]) & ~(|b[T-1:0])); assign c_inf = ((&a[K-2:T]) & ~(|a[T-1:0])) | (~eb_nz & ~(|b[T-1:0])); assign c_zero = ((&b[K-2:T]) & ~(|b[T-1:0])) | (~ea_nz & ~(|a[T-1:0])); logic [P-1:0][P-1:0] na_r, nb_r; logic [P-1:0][EW-1:0] ya_r, yb_r; assign na_r[0] = {ea_nz, a[T-1:0]}; assign nb_r[0] = {eb_nz, b[T-1:0]}; assign ya_r[0] = ea_nz ? a[K-2:T] : 1; assign yb_r[0] = eb_nz ? b[K-2:T] : 1; genvar i; generate for (i = 0; i < P - 1; i = i + 1) begin : norm assign na_r[i+1] = na_r[i][P-1] ? na_r[i] : (na_r[i] << 1); assign nb_r[i+1] = nb_r[i][P-1] ? nb_r[i] : (nb_r[i] << 1); assign ya_r[i+1] = na_r[i][P-1] ? ya_r[i] : (ya_r[i] - 1); assign yb_r[i+1] = nb_r[i][P-1] ? yb_r[i] : (yb_r[i] - 1); end endgenerate logic [P:0] nbx; logic [P+2:0][P:0] rr; logic [P+1:0][P:0] dd; logic [P+1:0] qq; assign nbx = {1'b0, nb_r[P-1]}; assign rr[0] = {1'b0, na_r[P-1]}; genvar k; generate for (k = 0; k < P + 2; k = k + 1) begin : div assign qq[P+1-k] = (rr[k] >= nbx); assign dd[k] = rr[k] - nbx; assign rr[k+1] = qq[P+1-k] ? (dd[k] << 1) : (rr[k] << 1); end endgenerate logic adj; logic [P:0] qm; assign adj = ~qq[P+1]; assign qm = qq[P+1] ? qq[P+1:1] : qq[P:0]; logic [W-1:0] onesW, emw; logic [EW-1:0] E, dsh; logic ovf; assign onesW = '1; assign emw = onesW >> 1; assign E = ya_r[P-1] - yb_r[P-1] + emw - adj; assign ovf = ~E[EW-1] & ((|E[EW-2:W]) | (&E[W-1:0])); assign dsh = (~E[EW-1] & (|E)) ? 0 : (1 - E); logic [P:0] qs; logic inc; logic [W-1:0] ef; logic [K-2:0] mag; assign qs = qm >> dsh; assign inc = qs[0] & ((qq[P+1] & qq[0]) | (|rr[P+2]) | ((qs << dsh) != qm) | qs[1]); assign ef = (~E[EW-1] & (|E)) ? E[W-1:0] : 0; assign mag = {ef, qs[P-1:1]} + inc; assign q[K-1] = ~c_nan & s; assign q[K-2:T] = (c_nan | c_inf | (~c_zero & ovf)) ? onesW : (c_zero ? 0 : mag[K-2:T]); assign q[T-1] = c_nan | (~(c_nan | c_inf | c_zero | ovf) & mag[T-1]); genvar n; generate for (n = 0; n < T - 1; n = n + 1) begin : lo assign q[n] = ~(c_nan | c_inf | c_zero | ovf) & mag[n]; end endgenerate endmoduleconst_nan.sv(negative, stopped atsolution): Always outputs the canonical quiet NaN.the design, with its comments left out
module fdiv #( parameter int W = 5, parameter int P = 11 ) ( input logic [W+P-1:0] a, input logic [W+P-1:0] b, output logic [W+P-1:0] q ); logic [W-1:0] ones; logic [P-2:0] top; assign ones = '1; assign top = (1 << (P - 2)); assign q = {1'b0, ones, top}; endmodule
Spec.lean, verbatim (109 lines)
import SvGolf.Task
import tasks.fdivp.IEEE754
/-!
# Task `fdivp` (trusted statement): IEEE 754 division, PARAMETRIC in the format
The variant of the statement that needs NO change to `SvGolf/Task.lean` (`design/fdiv-param/TASK.md`
explains the choice of this form, "Option C", and `design/fdiv-param/Task.lean.patch` is the unapplied
`CombTask2` alternative): the two-parameter family is a family of fixed-size `CombTask`s, one per `(W, P)`,
and the statement quantifies over the pairs with `CombTask.StatementFixed` at each.
Module (two parameters, in this order; port order as written):
```systemverilog
module fdiv #(parameter int W = 5, parameter int P = 11) (
input logic [W+P-1:0] a,
input logic [W+P-1:0] b,
output logic [W+P-1:0] q
);
```
`W` is the width of the biased-exponent field and `P` the precision (the significand digits
including the implicit leading bit), so the trailing significand has `P - 1` bits and a pattern
has `1 + W + (P - 1) = W + P` bits: binary16 is `W = 5, P = 11`, bfloat16 `W = 8, P = 8`,
binary32 `W = 8, P = 24`, binary64 `W = 11, P = 53`.
Statement: for every `W ≥ 2` and `P ≥ 2` (the spec's own well-formedness `Format.hw`, `Format.hp`)
with `W + P + 1 < 2^31` (so that the widths `W + P` and `W + P + 1`, `int` expressions of the module,
stay below `2^31`, the values an `int` holds), the design has exactly the ports `a`, `b`
(inputs, `W + P` bits) and `q` (output, `W + P` bits), no process is clocked, there is no
combinational loop, every run terminates, and in every cycle whose stimulus drives `a` and
`b` with known values the snapshot's `q` is `SvGolf.IEEE754.divide ⟨W, P⟩ .roundTiesToEven a b`,
the trusted spec of `svgolf/tasks/fdivp/IEEE754.lean` at that format. `REVIEW.md` lists the modelling choices.
-/
namespace SvGolf.Tasks.FdivP
open SvGolf SvGolf.IEEE754
/-- The storage width of the format `⟨W, P⟩`: `1 + W + (P - 1) = W + P`. -/
theorem k_eq (W P : Nat) (hP : 1 ≤ P) : 1 + W + (P - 1) = W + P := by omega
/-- **The function of the task**: `divide ⟨W, P⟩ .roundTiesToEven` on `(W + P)`-bit patterns,
for `2 ≤ W` and `2 ≤ P` (the spec's `Format` requires both). The `BitVec.cast`s only transport a
pattern along the equation `Format.k = W + P` (they leave `toNat` unchanged:
`fdivBits_toNat`); outside the range the function is `0`, which no statement looks at. -/
def fdivBits (W P : Nat) (a b : BitVec (W + P)) : BitVec (W + P) :=
if h : 2 ≤ W ∧ 2 ≤ P then
let f : Format := ⟨W, P, h.1, h.2⟩
have hk : f.k = W + P := k_eq W P (by omega)
(divide f .roundTiesToEven (a.cast hk.symm) (b.cast hk.symm)).cast hk
else 0#(W + P)
/-- The task at the format `⟨W, P⟩`, as a fixed-size `CombTask` (its own parameter is ignored and
taken at `0`, as in `CombTask.StatementFixed`): inputs `a b : BitVec (W + P)`, output
`q = fdivBits W P a b`. -/
def task (W P : Nat) : CombTask where
inRange K := K = 0
inputs _ := [("a", W + P), ("b", W + P)]
outputs _ := [("q", W + P)]
fn _ := fun (a, b, ()) => (fdivBits W P a b, ())
/-- Which parameter pairs the statement covers: the spec's own `Format` well-formedness, and
`W + P + 1 < 2^31`, so that the port width `W + P` and the exponent width `W + P + 1` a design computes
in (the ports' `[W+P-1:0]` and a `localparam integer EW = W + P + 1`, evaluated as `int`s) stay below
`2^31`, the values an `int` holds. -/
def inRange (W P : Nat) : Prop := 2 ≤ W ∧ 2 ≤ P ∧ W + P + 1 < 2 ^ 31
/-- **The challenge statement** for the two-parameter design family
`Submission.design.sem : Nat → Nat → Design2`: at every `W, P ≥ 2` in range the design satisfies the
fixed-size task at that format. A submission proves
`SvGolf.Tasks.FdivP.Statement Submission.design.sem`. -/
abbrev Statement (sem : Nat → Nat → LeanModels.Sv.Design2) : Prop :=
∀ W P, inRange W P → (task W P).StatementFixed (sem W P)
/-! Sanity checks on the statement's data (closed, by `decide`/`rfl`). -/
/-- binary16, bfloat16-like and binary32 are in range. -/
example : inRange 5 11 ∧ inRange 8 8 ∧ inRange 8 24 := by
simp [inRange]
/-- The range ends where `W + P + 1` reaches `2^31`, the first value an `int` does not hold. -/
example : inRange (2 ^ 31 - 4) 2 ∧ ¬ inRange (2 ^ 31 - 3) 2 ∧ inRange 2 (2 ^ 31 - 4) ∧
¬ inRange 2 (2 ^ 31 - 3) := by
simp [inRange]
/-- The input names are distinct (the non-vacuity theorem `CombTask.SatisfiedAt.exists_run`
needs it), at every parameter pair. -/
example (W P : Nat) : (((task W P).inputs 0).map Prod.fst).Nodup := by
simp [task]
/-- The casts do not change values. -/
theorem fdivBits_toNat (W P : Nat) (h : 2 ≤ W ∧ 2 ≤ P) (a b : BitVec (W + P)) :
(fdivBits W P a b).toNat =
(divide ⟨W, P, h.1, h.2⟩ .roundTiesToEven
(a.cast (k_eq W P (by omega)).symm) (b.cast (k_eq W P (by omega)).symm)).toNat := by
simp [fdivBits, h]
/-- Golden vectors of the spec through the task's function: `1 / 3 = 0x3555` in binary16,
`1 / 3 = 0x3EAAAAAB` in binary32, and bfloat16-like `(8, 8)`: `1 / 3 = 0x3EAB`. -/
example : ((task 5 11).fn 0 (0x3C00#16, 0x4200#16, ())).1 = 0x3555#16 := by decide
example : ((task 8 24).fn 0 (0x3F800000#32, 0x40400000#32, ())).1 = 0x3EAAAAAB#32 := by decide
example : ((task 8 8).fn 0 (0x3F80#16, 0x4040#16, ())).1 = 0x3EAB#16 := by decide
/-- `0 / 0` is the canonical NaN of the format (`0x7E00` in binary16). -/
example : ((task 5 11).fn 0 (0x0000#16, 0x0000#16, ())).1 = 0x7E00#16 := by decide
/-- The smallest formats are in range: `W = 2, P = 2` is 4 bits. -/
example : ((task 2 2).fn 0 (0b0011#4, 0b0100#4, ())).1 = fdivBits 2 2 0b0011#4 0b0100#4 := rfl
end SvGolf.Tasks.FdivP
Its trusted text
The modules specific to this task. Like every task, it also rests on the shared trusted base (the ls-sv semantics of SystemVerilog and svGolf's statement helpers), and a proof may import any module of the ls-sv library. Nothing else is trusted: proof helpers are kernel-checked like any submission.
| module | role | lines | sha256 |
|---|---|---|---|
tasks.fdivp.Spec | task statement | 109 | 71e46a4ce975 |
tasks.fdivp.IEEE754 | task statement | 518 | ea783e2a80d8 |
How to participate #
- Write a circuit with the task's exact interface.
- Prove in Lean 4 that it meets the trusted statement; Start a new design, below, gives the route, and the proving guide shows how.
- Check and record it (how to submit): the checker accepts the pair or says which stage refused it, as it does for each design under what does not count.
- Beat par: an accepted design whose score (area × time) is below that of the best proved reference. The leaderboard ranks by it.