Module verification 

Verification and evidence

Hardware correctness has several layers. Passing a later layer does not excuse skipping an earlier one.

1. Pure model tests

[rhdl_ed25519_model] wraps the pinned Dalek implementation. Use it for:

• RFC 8032 vectors;
• public-key derivation;
• signing and strict verification;
• multipart semantics;
• deterministic randomized vectors;
• malformed key/signature expectations.

The model and hardware must not share the implementation under test for the lowest arithmetic oracle. Field/scalar RTL tests should also use independent big-integer calculations.

2. Kernel compilation and unit tests

Every #[kernel] and synchronous engine should compile through RHDL. Narrow tests should cover state transitions, arithmetic boundaries, carry behavior, BRAM latency, and ready/valid stalls.

Use single-job and back-to-back tests. A pipeline that passes with a bubble between every request has not demonstrated initiation interval one.

3. RHDL end-to-end simulation

The simulation harness drives real commands and message words into [rhdl_ed25519_top::Ed25519Core]. It compares public keys and signatures with Dalek, verifies results, records counters, and emits compact traces.

The checked-in simulation summary currently records passing cases for:

• three RFC 8032 vectors and deterministic messages;
• hardware SHA-512;
• constant-pattern scalar multiplication;
• end-to-end RFC signing and strict verification;
• 1, 64, 128, 4096, and 16384-byte signing;
• multipart 4097-byte signing/verification;
• non-canonical S rejection.

The recorded 64-byte compatibility signing result is 90,928 core cycles.

4. Emitted RTL simulation

Generated Verilog must be tested with Icarus and/or Verilator. This catches lowering and black-box integration errors that an RHDL behavioral model can miss. Fast-field tests drive hundreds of consecutive no-bubble requests and compare every response.

For any manually maintained SystemVerilog black box:

• lint it with Verilator;
• simulate it with an independent oracle;
• test reset in the middle of activity;
• test valid gaps and continuous valid;
• assert exact result latency and ordering.

5. Synthesis

Yosys is useful for generic structural statistics. Vivado is authoritative for U280 primitive inference, device utilization, and timing. Record:

• exact part and clock constraint;
• Vivado version;
• source/RTL checksum;
• LUT, register, DSP, BRAM, and URAM use;
• WNS/TNS and whether constraints were met;
• OOC versus full implementation.

An OOC module report omits the Vitis shell, SLR crossings, AXI movers, and whole-design congestion.

6. Hardware validation

Final evidence requires a U280 xclbin and XRT execution. Every hardware result must be checked by Dalek outside the timed interval. Run enough work to measure sustained throughput, not launch overhead.

For the fixed-64 objective, the acceptance run should include at least one million cold signatures, deterministic distinct seeds/messages, no mismatches, five warmups, and thirty measured runs. Report p50 and p95 throughput and latency.

Evidence labels

Use these words consistently:

• tested: a named test passed in the current source tree;
• simulated: a cycle/RTL simulation produced the result;
• synthesized: a named tool/part/constraint produced a utilization report;
• implemented: place-and-route completed and met DRC/timing conditions;
• measured on U280: a physical-board run produced the result;
• modeled/estimated/target: not hardware evidence.

Do not call a negative-WNS design “300 MHz.” Say it was constrained to 300 MHz and report the miss.