Module validation 

Evidence ledger separating simulation, mapping, timing, and hardware claims.

Validation Record

This file records what has been demonstrated for the current all-RHDL source. It intentionally does not inherit results from the removed handwritten SystemVerilog implementation.

Documentation Refresh, 2026-10-08

The visual guide adds a beginner-level signature recipe, parallel-path resource diagram, register-stage overlay, conceptual FPGA map, and optimization roadmap. The architecture guide and this evidence ledger are now available directly in Rustdoc. Diagram resource estimates are explicitly separated from measured leaf counts; the FPGA drawing is not actual placement.

This refresh changes documentation and doc-only module wiring, not hardware behavior. Rebuild with the bounded warning-denied command in the crate’s developer workflow. The offline SVG render check does not establish browser/mobile layout or any new hardware result. Native, RTL, synthesis, routing, and board tests are not rerun for this docs-only change.

Current evidence

2026-10-03 optimization update: the default topology now has eight signing SHA lanes, two signing multi-comb engines, and two pair compressors, plus the unchanged strict-verification arithmetic. The 64-context widened signer passed 192 distinct, exact-Dalek signatures in 498.52 seconds of host simulation. Its original short-window rate was burst-biased; the logged completion-64/128 window gives 149.75 cycles/sign (1.369M/s at an assumed 205 MHz). The following revision uses 128 signing contexts and a six-tile field multiplier; its validation is recorded separately below. Long native tests use a no-waveform driver with constant history memory. No native simulation establishes physical fit or achieved clock. The older mapping reports below refer to representative leaves and the compact topology.

The six-tile cell passed 548 integer differential cases at exactly six stages, plus generated RTL and netlist equivalence in Icarus. Field multiply/add/subtract, all 128 encoded-point addresses, synchronous reads, and point-pair read-after-write regressions passed. The new signing scheduler and encoded-R controller compile through the RHDL frontend. The 384-signature sustained rerun passed all outputs. Conservative reanalysis with 128 warmup/drain completions gives 90.984375 cycles/sign, or 2.253M/s at an assumed 205 MHz. See reports/bench/README.md: the raw run’s shorter-window 2.499M/s printout is superseded and must not be used.

Fresh Yosys 0.62 xcup leaf mapping: 6 DSP48E2, 155 LUT2, 928 FDRE. With -nodsp: 0 DSP, 7,642 LUT primitives, 928 FDRE, plus carry/wide-mux primitives. DSP internal pipeline registers were not packed by this Yosys flow. Naive replication exceeds the FF cap, so these counts explicitly do not prove full-core fit. See reports/mapping/mul51-xcup-{dsp,lut}.json and the mapping discussion in the Optimization Lab. Vivado mapping remains required.

Warning-denied Clippy and Rustdoc passed for the hardware revision used by the 384-vector binary. After that gate, only the benchmark-window accounting and documentation were corrected; the new window was independently recomputed and negative-tested with tools/analyze_throughput.jq. The source documentation includes that correction; rebuild Rustdoc with the bounded command to refresh the rendered copy. A fresh full-workspace/whole-top RTL run was not performed during this resource-limited optimization window.

Native RHDL simulation has demonstrated:

• SHA-512 compression and padding-boundary behavior against sha2;
• radix-2^51 field multiplication, addition, subtraction, and normalization;
• scalar reduction and scalar multiply-add against Dalek scalar arithmetic;
• fixed-base multi-comb multiplication against Dalek points;
• projective point compression and compressed Edwards-Y decoding;
• rejection of noncanonical and low-order point encodings;
• variable-base multiplication for interleaved and arbitrary decoded points;
• the projective verification equation;
• cached public-key derivation and exact 64-byte signatures against ed25519-dalek;
• acceptance of a valid Dalek signature and rejection of a modified message;
• retention of simultaneous sign and verify completions by the result arbiter;
• compilation of individual pipelines through the RHDL frontend and Rust type-checking of the public Fast64Core composition.

The repository gate also checks formatting, warning-denied Clippy, warning-denied Rustdoc, the one-package invariant, generated-netlist origin, and absence of handwritten .sv/.v files outside vendor/, target/, and reports/generated/.

Claims matrix

Property	Status	Required evidence
One authored Rust crate	Proven	Cargo metadata
No handwritten HDL in crate	Proven by source-tree gate	File inventory
Hardware SHA-512	Proven in RHDL simulation	SHA differential tests
Cached signing correctness	Proven in RHDL simulation	Exact Dalek signature
Strict verification correctness	Partially proven	Valid/modified and malformed tests; broader vectors still desirable
Zero cryptographic DRAM/HBM scratch	Proven architecturally	No external-memory port
Generated top-level Verilog	Pending final export gate	reports/generated/fast64_core_rhdl.v
U280 resource fit	Not yet proven for current netlist	Fresh Vivado utilization report
U280 routed timing	Not yet proven for current netlist	Fresh post-route timing report
At least 2M signs/s	Optimization target, not yet proven	Sustained cycles plus achieved clock and resource fit
At least 200k verifies/s	Not yet proven on current netlist	On-card counters at routed clock

The prior handwritten implementation’s 1.014M signatures/s and 214.6k verifications/s are the regression targets. They are not reported as results for the all-RHDL implementation.

Bounded mapping and speed estimate

The current handoff includes a bounded representative mapping pass. Generated RHDL leaves passed Icarus 13.0 and Yosys 0.62 process/memory lowering:

Leaf	Generic cells	Multiplier cells
Field multiplier	519	226
Scalar reducer	3,477	576
SHA-512 compression lane	132	0

Those historical leaves used nine tiles per limb product. The current six-tile compact structural full-core estimate is 5,690 arithmetic multipliers: 3,450 in 23 field multipliers, 1,728 in three scalar reducers, and 512 in the signing scalar-wide multiplier. The widened topology adds five field multipliers for a structural estimate of 6,440. Both estimates are below 9,000; neither proves DSP mapping, the 260k LUT cap, or the 520k FF cap.

The older short fixed-base sample reported 121.077 cycles; it is not a full end-to-end sustained measurement. Four SHA lanes give an ideal hash-only 181.5-cycle service interval, or a 1.129M/s ceiling at 205 MHz. Eight lanes give a 2.259M/s hash-only ceiling. Context capacity and compression may impose stricter limits. Parallel point decoding is the estimated verification bottleneck at roughly 516 cycles/request, or about 397k verifies/s at 205 MHz. These are architecture-level estimates, not hardware claims. See reports/mapping/SUMMARY.md for calculations and checksums.

The final end-to-end signing rerun after packaging was manually stopped after approximately twelve minutes to protect interactive resources; it did not report a failure. The exact signing and strict-verification Dalek differentials had passed earlier during implementation. The short final gate re-confirmed the multi-comb interval, four-lane SHA routing, and back-to-back scalar reduction.

Reproduction

Run all local gates serially to keep compiler memory bounded:

./tools/test_all.sh

The functional simulations for complete signing and verification are much slower than hardware because RHDL evaluates large exact-width networks in software. A complete run can take several minutes. The gate uses one Cargo job and one test thread so multiple large simulations never compete for memory.

Generate bounded representative leaves with:

RUST_MIN_STACK=536870912 \
  cargo run --locked -j1 --bin export_fast_core_rhdl -- --leaves

Generate the complete top-level implementation netlist explicitly with:

RUST_MIN_STACK=536870912 \
  cargo run --locked -j1 --bin export_fast_core_rhdl

The output is generated evidence. Its SHA-256 digest is written to reports/generated/SHA256SUMS by the full gate.

U280 acceptance procedure

A physical-performance claim requires all of the following from the same generated-netlist checksum:

1. Vivado synthesis for xcu280-fsvh2892-2L-e with no critical warnings that alter memory or DSP inference.
2. Utilization below 260,000 LUTs, 520,000 registers, and 9,000 DSPs.
3. Successful placement and routing with nonnegative setup WNS.
4. A hardware run using monotonically increasing accepted/completed counters.
5. At least 192 interleaved operations after warm-up, with cycles measured from first accepted request to last completed request.
6. Dalek validation of every returned signature and verification decision outside the timed region.
7. Reported sign and verify rates derived from the achieved hardware clock, not a requested constraint.

The report must include generated-netlist checksum, bitstream checksum, device, tool version, achieved frequency, request count, cycle count, LUT/FF/BRAM/URAM/ DSP usage, WNS, and transport bytes. A timeout or unfinished route is not a passing hardware result.

Memory accounting

Fast64Core has no AXI master and no DRAM/HBM scratch interface. The fixed 64-byte message is transported once per request. The multi-comb table and all request contexts are local RHDL memories. This establishes zero external cryptographic scratch accesses, but a shell benchmark must separately report host-to-card and card-to-host bytes.