Skip to main content

Crate rhdl_gen

Crate rhdl_gen 

Source
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

  • list reads the target registry and does not generate or validate RTL.
  • generate lowers one registered target and writes generated Verilog plus a provenance manifest; it does not invoke synthesis.
  • check invokes Icarus for the small smoke targets. check --full also uses Verilator for standalone complete-lane and three-lane equivalence traces.
  • check --signer-full is 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-throughput does not lower RHDL. It revalidates a preserved signer bundle and runs a separate always-ready Verilator trace against that exact immutable source.
  • benchmark-kernel sequentially 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-graph revalidates 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-graph performs the same live source/evidence validation against an existing canonical record and writes nothing.
  • u280-hbm-rtl-check revalidates 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-round
  • legacy-keccak-iterative
  • sha256-round
  • sha256-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.v
  • wots_sha256_signer_top.skeleton.v
  • wots_sha256_signer_top.bundle.v
  • wots_sha256_signer_top.bundle.manifest.json
  • wots_sha256_signer_top_tb.sv
  • signer-lower-lane.log
  • signer-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" --keep

Choose 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.

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§

ArtifactManifest
Deterministic checksum and provenance record accompanying generated RTL.
GeneratedArtifact
Files produced by one generation operation.
SourceProvenance
Source-tree identity captured before an artifact is written.
TargetSpec
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
HashSigsRS revision 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.