Expand description
§rhdl-gen
rhdl-gen is the reproducible boundary between the Rust/RHDL source and
generated Verilog artifacts. It does not synthesize, place, route, or execute a
design on hardware.
§Operational boundary
listreads the target registry and does not generate or validate RTL.generatelowers one registered target and writes generated Verilog plus a provenance manifest; it does not invoke synthesis.checkinvokes Icarus for the small smoke targets.check --fullalso uses Verilator for standalone complete-lane and three-lane equivalence traces.check --signer-fullis an opt-in, multi-gigabyte lowering and Verilator gate for the modular production signer. Run it serially in a dedicated evidence directory and coordinate ownership of shared build memory first.signer-throughputdoes not lower RHDL. It revalidates a preserved signer bundle and runs a separate always-ready Verilator trace against that exact immutable source.benchmark-kernelsequentially lowers the canonical SHA lane and modular Rust/RHDL AXI-Lite benchmark, then emits an immutable bundle, a metadata- derived wire-only named Vitis wrapper, and packaging Tcl. Generation is not a card build or hardware run.u280-link-graphrevalidates one current generated HBM kernel, its canonical schema-2 generation manifest, and a complete successful full-signer evidence directory before creating a new read-only provenance record.u280-verify-link-graphperforms the same live source/evidence validation against an existing canonical record and writes nothing.u280-hbm-rtl-checkrevalidates that live graph, stages the exact kernel and signer sources in order, and runs a self-checking external simulation through the actual packaged top, AXI4-Lite, and deterministic HBM models. Typed RHDL offsets expose the signer final-beat handshake to an independent observer; payload-B handshakes are observed independently as well. Their spans must equal the shell summary/diagnostics before the external spans can satisfy the source-only thresholds. One canonical Verilator executable is resolved and hashed before use, invoked by exact path, revalidated through evidence sealing, and recorded by canonical path, digest, and byte length. The built simulator receives the same pre-execution identity retention and sealing checks, so a replaced post-run binary cannot become the recorded artifact.
The kept-evidence examples use a caller-selected absolute directory rather than a user-specific home path. Choose a new path outside the source workspace and set it before running either opt-in command:
export EVIDENCE_ROOT=/absolute/path/to/hashsigs-evidence
mkdir -p "$EVIDENCE_ROOT"§Evidence boundary
Every artifact produced here remains at the generated-verilog evidence tier.
An elaboration or simulation PASS applies only to the named generated source,
toolchain, and exercised trace recorded by its manifest. It is not formal
proof, synthesis, mapped-resource, timing-closure, placement, route, shell,
card-execution, or deployment evidence. Those claims require their own higher-
tier flows and reports.
rhdl-gen list
rhdl-gen generate <TARGET> --output <DIRECTORY> [--force]
rhdl-gen check [--full] [--signer-full] [--temp-root <DIRECTORY>] [--keep]
rhdl-gen signer-throughput --source-evidence <DIRECTORY> --output <NEW_DIRECTORY>
rhdl-gen benchmark-kernel --output <NEW_DIRECTORY>
rhdl-gen u280-link-graph --kernel <VERILOG> --kernel-manifest <JSON> --signer-evidence <DIRECTORY> --output <NEW_JSON>
rhdl-gen u280-verify-link-graph --kernel <VERILOG> --kernel-manifest <JSON> --signer-evidence <DIRECTORY> --record <JSON>
rhdl-gen u280-hbm-rtl-check --kernel <VERILOG> --kernel-manifest <JSON> --signer-evidence <DIRECTORY> --record <JSON> --output <NEW_DIRECTORY>benchmark-kernel requires a clean source worktree and a path that does not
exist. Its two memory-heavy graphs are lowered in separate child processes.
The output manifest checksum-binds the lane, unresolved benchmark skeleton,
wire-only wrapper, exact concatenated bundle, packaging Tcl, child logs, packed
port widths, ABI version, clean source provenance, and the validated complete
module graph. Generation rejects duplicate or unreachable definitions unless
the named Vitis top reaches exactly one benchmark, one canonical three-cluster
signer, exactly three cluster-prototype instances, and one canonical external
lane site.
The emitted packaging Tcl is intentionally non-overwriting. It requires a new
XO path, atomically acquires a new per-XO .package-work path, rejects
source/output aliasing,
hashes the source, packages a read-only checked copy, embeds the source digest
and byte count in the IP description, verifies the copy imported into the
packaged IP, and rehashes the original, staged, and imported copies before a
non-overwriting publication rename. Both IP metadata and
package_xo explicitly select user_managed, matching the xrt::ip host
contract. The canonical runtime identity is
hashsigs_wots_sha256_benchmark_kernel:{hashsigs_wots_sha256_benchmark_kernel_1};
the exact 250/300 MHz v++ link configs live under fpga/u280/phase_a/.
The register contract and one-time-key persistence boundary are summarized in
the U280 evidence workflow and maintained alongside
the implementation in fpga/u280/BENCHMARK_ABI.md.
list prints the profile and top module for every registered target. generate
writes a deterministic .v file and adjacent .manifest.json; it refuses to
replace either filename unless --force is explicit. The manifest records the
source commit and dirty state, pinned RHDL and HashSigsRS revisions, profile,
target, exact Verilog SHA-256 digest, validation boundary, and the evidence tier
generated-verilog.
The target registry keeps LEGACY_KECCAK and
HASHSIGS_SHA256_GENERIC_V1 explicit. The SHA profile exports an isolated
round, a full combinational compression oracle, a checked two-stage registered
pipeline, the complete 64-stage round pipeline, the complete BRAM-backed
compression lane, and the exact three-lane compression farm. The three complete
structural targets are explicitly named *-unchecked because their RHDL export
bypasses Icarus’s final scan; standalone generation is not a validation claim.
The profiles are separate build targets; generating one does not introduce a
runtime profile mux or make its keys and signatures compatible with the other.
The default check creates a unique temporary child directory and asks Icarus
Verilog to parse and elaborate these declared tops:
legacy-keccak-roundlegacy-keccak-iterativesha256-roundsha256-pipeline-2
It fails clearly when iverilog is unavailable. The child directory is removed
by default; --keep preserves it for inspection. Tool temporary files are
directed into the same selected child directory.
check --full first performs the default check. It then renders
sha256-compression-lane-64-unchecked and
sha256-compression-farm-3x64-unchecked. For each declared top it asks
Verilator to parse and elaborate the generated hierarchy, then builds a
deterministic SystemVerilog testbench. Expected digests are calculated by the
independent Rust compress_block model. The simulations exercise the published
SHA-256 abc block, non-IV feed-forward cases, adjacent tokens, bubbles,
asymmetric full-width tags, exact 64-cycle latency, reset flushing, and
post-reset recovery. The farm test additionally checks independent activity on
all three lanes.
The report includes the Verilator version, lint/build/run times, success
markers, a deterministic warning-code inventory, and captured diagnostic-log
paths. Those paths are preserved when --keep is supplied and are explicitly
labeled ephemeral otherwise. A successful -Wno-fatal lint result with listed
warnings is accepted elaboration, not a warning-clean claim.
check --signer-full is the separate, resource-intensive production-signer
gate. It requires a clean source worktree. It first lowers the exact
FullCompressionLane as sha256_compression_lane, writes and marks that source
read-only, and exits that dedicated child process. Only after the operating
system has reclaimed that entire address space does a second child lower the
unresolved ModularSha256SignerTop skeleton. The two memory-heavy RHDL graphs
therefore cannot overlap. It persists these files in the unique check directory:
sha256_compression_lane.source.vwots_sha256_signer_top.skeleton.vwots_sha256_signer_top.bundle.vwots_sha256_signer_top.bundle.manifest.jsonwots_sha256_signer_top_tb.svsigner-lower-lane.logsigner-lower-skeleton.log
The manifest records the clean source commit, pinned RHDL and HashSigsRS
revisions, explicit HASHSIGS_SHA256_GENERIC_V1 profile, generator version,
independent SHA-256 digest and byte length for every source, the self-checking
testbench, and both child-process logs, plus packed signer and lane port widths
and the validated module graph. The linker fails unless the
skeleton contains no lane definition, its shared cluster prototype contains
one reachable canonical lane site, and graph traversal from the signer top
finds exactly one reachable parent containing prototype instances c0, c1,
and c2 with no extras or duplicates. Intermediate RHDL-generated wrapper
modules are permitted; unreachable lookalike hierarchies do not satisfy the
gate. The bundle must contain exactly one canonical lane definition, and every
module name must have one definition. The driver rechecks the read-only files,
provenance, checksums, widths, and graph immediately before each external build
or simulation phase.
The immutable SystemVerilog testbench embeds twelve expected WOTS results
calculated with the independent Sha256GenericWots software oracle. Packed
testbench field ranges come from RHDL Digital::static_kind,
bit_range, and path!; they are not handwritten Verilog offsets. The finite
trace resets a live sacrificial job, fills all twelve contexts, rejects a
thirteenth offer, applies deterministic randomized backpressure, holds the
first final beat for five cycles, and compares all 420 accepted output beats by
job identity. It requires twelve finals and releases, no faults or errors, and
post-completion quiescence. The opt-in integration test is ignored by ordinary
test runs because full-lane and signer-skeleton lowering have multi-gigabyte
host-memory footprints.
After a successful run, the Verilator lint, build, and simulation logs are
marked read-only and recorded by filename, byte length, and SHA-256 digest in
wots_sha256_signer_top.check-evidence.json. That final manifest also binds the
exact success marker, source commit, bundle manifest, testbench, and lowering
logs. It records only this finite generated-RTL gate; it does not raise the
evidence tier.
Use --keep when the immutable sources, manifest, testbench, and diagnostic
logs need to survive the command:
cargo run --release --locked -j1 -p rhdl-gen -- check --signer-full \
--temp-root "$EVIDENCE_ROOT/signer-rtl" --keepChoose a filesystem with enough free space for the generated Verilator object
tree. The driver also sets TMPDIR, TMP, and TEMP to the selected kept
workspace for every lowering and external-tool phase.
Lint proves that Verilator accepted and elaborated each unchecked rendering. The simulations are generated-RTL equivalence evidence for only the exercised deterministic vectors and control sequences; they are not formal proofs. The production signer trace is a finite saturated batch, not a sustained-throughput measurement. Verilator is a two-state simulator, so this gate is also not a four-state unknown-propagation proof. Neither operation constitutes synthesis, timing, resource, route, or hardware evidence.
§Sustained signer generated-RTL gate
signer-throughput is deliberately separate from check --signer-full. It
does not lower or relink any RHDL. Instead, --source-evidence must name a
preserved successful signer directory produced by check --signer-full --keep.
The command revalidates the complete immutable chain before the build, before
simulation, and after simulation: regular non-symlink/read-only files, exact
manifest schemas, target, HASHSIGS_SHA256_GENERIC_V1 profile, pinned source
revisions, packed port widths, module graph and top, lane-plus-skeleton bundle
bytes, every recorded checksum/length, successful lowering/lint/build/run
statuses, and the exact prior finite-equivalence PASS marker. The new output
must not already exist and must be outside both the source evidence directory
and the source workspace.
The separately generated immutable testbench derives every packed field offset
from RHDL Digital metadata and embeds 72 distinct fused private-seed results
from the independent Sha256GenericWots oracle. It continuously holds the next
job valid until admission, keeps output ready high, and compares all 2,520
accepted beats, job identities, admission/return clusters, 72 finals, and 72
credit releases. Each local release must remain the sole pending release and
match the cluster of the next delivered final. Results 1 through 12 warm the
pipeline. The exact interval
from completion boundary 12 to completion boundary 60 covers 48 result
intervals and must be at most 24,000 cycles, or 500 cycles/result normalized at
250 MHz. Results 61 through 72 are a mandatory tail, followed by 160 cycles of
quiescence. Any fault, error, malformed frame, interleaving, missing/duplicate
job, release mismatch, or output-ready drop fails the run.
On success, the testbench, built simulator, build log, simulation log, and
final evidence manifest are read-only. The manifest binds the source bundle,
both source evidence manifests and prior PASS marker, the current clean flow
commit and exact rhdl-gen executable digest, Verilator version, fixed
benchmark constants, and every new output checksum. Verilator receives only
the validated bundle and this new testbench as HDL sources, with --threads 1
and -j 1.
cargo run --release --locked -j1 -p rhdl-gen -- signer-throughput \
--source-evidence "$EVIDENCE_ROOT/signer-rtl/rhdl-gen-check-EXAMPLE" \
--output "$EVIDENCE_ROOT/signer-throughput/run-EXAMPLE"This is sustained generated-RTL completion evidence for the exact always-ready trace, not synthesis, timing closure, mapped resources, route, shell, card, or arbitrarily backpressured throughput evidence. Verilator remains a two-state simulator.
§U280 HBM provenance link
The HBM package boundary never accepts a loose signer .v file. The creator
requires the exact generated kernel, its adjacent generation manifest, and a
preserved directory that still passes the complete check --signer-full
evidence validator. The current rhdl-gen source worktree must be clean. Its
commit must equal the kernel manifest commit, the manifest must be the exact
canonical schema-2 encoding for target sha256-u280-hbm-kernel, and every
profile, validation-scope, filename, source digest, pinned revision, and
generator-version field must equal the current build. The supplied kernel bytes
must also equal a fresh in-memory rendering from the current Rust/RHDL source.
The signer validator rechecks the full finite-equivalence evidence chain. The link record binds the exact kernel, kernel manifest, signer bundle, signer bundle manifest, and signer check-evidence manifest by canonical filename, byte length, and SHA-256. It also records both clean source commits, both pinned revisions, the exact top/shell/signer module and instance identities, and the strictly sorted complete reachable module inventory. The adapter must remain wire-only and its top must have exactly the two expected direct children.
Schema 2 uses typed deny_unknown_fields records and one canonical pretty-JSON
encoding with a trailing newline. Missing, duplicate, unknown, nested-in-place-
of-scalar, reordered, or otherwise non-canonical JSON is rejected. Record
fields are descriptive only: the verifier reconstructs the expected record
from current kernel generation and independently validated signer evidence,
then requires exact equality. It never trusts a success boolean or digest from
the record to authorize the corresponding input.
Create the record once, then use the read-only verifier immediately before any consumer packages the sources:
rhdl-gen u280-link-graph \
--kernel "$HBM_GENERATION/hashsigs_sha256_hbm_kernel.v" \
--kernel-manifest "$HBM_GENERATION/hashsigs_sha256_hbm_kernel.manifest.json" \
--signer-evidence "$SIGNER_EVIDENCE" \
--output "$LINK_EVIDENCE/combined-link-graph.json"
rhdl-gen u280-verify-link-graph \
--kernel "$HBM_GENERATION/hashsigs_sha256_hbm_kernel.v" \
--kernel-manifest "$HBM_GENERATION/hashsigs_sha256_hbm_kernel.manifest.json" \
--signer-evidence "$SIGNER_EVIDENCE" \
--record "$LINK_EVIDENCE/combined-link-graph.json"Both commands establish source provenance and structural generated-RTL identity only. They do not establish synthesis, timing, resource, route, XRT, card-output, or on-card performance evidence.
The complete Keccak permutation and SHA-256 compression targets are exportable combinational correctness oracles. They are intentionally excluded from the quick Icarus check because they are not the area-oriented implementations; the SHA compression oracle is also excluded from default unit generation because lowering it is slow. All complete unchecked SHA structural targets are likewise excluded from default unit generation and quick Icarus checks.
None of these operations constitutes synthesis, timing closure, resource measurement, routing, or card evidence.
Structs§
- Artifact
Manifest - Deterministic checksum and provenance record accompanying generated RTL.
- Generated
Artifact - Files produced by one generation operation.
- Source
Provenance - Source-tree identity captured before an artifact is written.
- Target
Spec - Metadata and generator for one extensible RTL target.
Enums§
- Command
- Parsed command-line operation.
Constants§
- GENERATED_
VERILOG_ EVIDENCE_ TIER - Evidence tier written to every generated artifact manifest.
- HASHSIGS_
REVISION HashSigsRSrevision used by the compatibility profile.- RHDL_
REVISION - RHDL revision used to lower these Rust kernels to Verilog.
- USAGE
- Command-line usage text.
Statics§
- TARGETS
- Registered RHDL Verilog generation targets.
Functions§
- execute
- Execute one parsed command and return its human-readable output.
- find_
target - Look up a target by its stable registry name.
- generate_
target - Generate one target and its deterministic provenance manifest.
- parse_
args - Parse arguments excluding the executable name.
- run_
from_ args - Parse and execute arguments excluding the executable name.