Evidence ladder
Current completion boundary: generated RTL is the highest passed signer-performance tier. The U280 250 MHz and 300 MHz synthesis and route records, plus programmed-card execution, are pending. Until those exact artifact chains pass, do not describe the project as synthesized, routed, timed at either target clock, card-validated, or hardware-complete.
| Tier | What it can establish | What remains outside the tier |
|---|---|---|
| 0. Model | Dependency arithmetic, bounds, or a software oracle | RHDL behavior and all implementation claims |
| 1. Source simulation | Rust/RHDL behavior and modeled cycle events | Emitted RTL, mapped resources, timing, route, hardware |
| 2. Generated RTL | Lowering equivalence for an executed trace | Formal proof, synthesis, clock, mapping, route, card |
| 3. U280 synthesis | Mapping and estimated timing for an exact top and constraint | Placement, route, shell, physical clock, card rate |
| 4. U280 route | Resource and timing of a completely routed exact design | Shell/card behavior unless included and executed |
| 5. Card execution | Validated runtime behavior and throughput for the tested setup | Untested workloads, clocks, shells, or revisions |
Promotion moves one exact source and artifact chain upward. It cannot combine a cycle interval from one commit with timing from another, or a routed core from one top with a shell from another.
Negative results
A failed synthesis, placement, or route attempt remains useful when it names the exact source, tool, constraint, failure, and reports. Retaining it prevents future readers from treating “Vivado exited” as “timing closed.”
Dirty source
Dirty-source evidence is permitted only when every differing source file and checksum is recorded. A clean source commit is preferred for promotion and deployment. The manifest displays dirty state rather than hiding it.
Four-state and formal boundaries
Verilator’s ordinary two-state simulation does not prove unknown propagation. A deterministic testbench is not a formal proof. These limitations remain nonclaims even when every expected output in that trace matches.