Verification evidence and limits¶
The published benchmark is the RustEDA whole-flow Ibex run with two real IHP SRAMs on IHP SG13G2 / EZ130 8T, on the RustEDA benchmarks page. Its synthesis and final CEC gates prove the synthesized and final netlists equivalent to the original RTL; the benchmark page describes RustSys's part and the proof scope.
The retained synthesis-only common campaign, whose archive is mainly historical timing and quality receipts, binds each measured implementation to its original RTL, Liberty library and exact exported Verilog bytes. Performance sampling, logical equivalence and timing analysis are separate operations with separate receipts.
Common campaign proof method¶
The common campaign checks RustSys and Yosys netlists on Sky130 HD and GF180 7T. Each tool's 1/16-core netlists must be byte-identical, so one proof covers both allocations.
Functional validation uses the independent RTL event model and external ABC CEC. Inferred multiplication/addition uses exact observed-operand components checked by Arisca, with complete ABC checks of extraction, context reconstruction, the Boolean context and transport to the actual measured netlist. Observations add obligations; they do not assume internal signals equivalent. The model completes ordinary X/Z data and undriven values to zero while keeping arbitrary register initial states. It adds no reset pulse, reachability restriction or new input assumption. Wildcards retain their language matching semantics.
The event export quantifies the original inputs and RTL states, retains every original output, and covers every implementation state element's data, clock/enable and asynchronous controls under a checked one-to-one correspondence. Names supply bindings first; when mapping removes them, a bounded search can propose bindings without fixing any initial value or sharing state. Restricting proposal candidates leaves every original RTL state free. The relation ledger must cover all implementation state. A successful export remains undecided until every external comparison completes.
Each certificate checks the input, library, gate implementation and obligation hashes. A previously completed certificate can be reused only for those exact bytes and the same scope. Changed measured netlists require a new proof. Data and clock corruption controls are included on both baseline PDKs.
The native interpreter shares format readers and core types with synthesis, while its RTL interpretation, cell evaluation and proof implementation are separate. External tool calibration and independently specified controls address common-error risk; this is not a claim of a fully independent frontend or four-state simulation equivalence.
Timing evidence¶
An independent OpenSTA executable analyzes the exact mapped netlist under a common TT, ideal-clock, zero-wire model. Its setup-Fmax estimate is separate from functional equivalence and from routed timing closure. Read the timing assumptions, excluded path classes and raw constraint-check output before using the number.
No timing result implies physical DRC, placement/routing, clock-tree correctness or hold closure. Missing results remain missing; they are never printed as zero violations.
Historical proof scopes¶
The earlier four-core campaign, whose archive also tabulates historical timing and area results, used EQY/SBY, ABC CEC and undef-aware Yosys SAT with checked arithmetic compositions. It established defined-bit refinement under its documented state correspondence. The two historical native VexRiscv SAT checks stayed unverified under their budgets, despite completed external proofs in that campaign.
The corrected single-run OpenC910 campaign, whose archive is mainly a historical stress-run timing record, calibrated the independent two-valued RTL model against actual Yosys netlists and checked complete projected obligations with ABC. Its producer and source snapshots are retained. It is a different measurement profile from the common default-mapping campaign.
Invalidations remain part of the record¶
A concatenated/replicated wildcard-label bug affected both synthesis and its native checker. The correction was checked against an independently captured simulation truth table, exhaustive small controls, external formal comparisons and negative old-netlist controls. Earlier certificates were explicitly invalidated in the registry.
A historical equivalent report does not override a later invalidation. Use each campaign's dated archive and declared semantic model; do not relabel an old certificate as proof of a changed netlist.
Regression coverage¶
The repository includes synthetic known-answer fixtures, generated and metamorphic designs, deliberately faulty netlists, resource-budget controls, and both Sky130 and GF180 coverage. Requirement identifiers connect behavior to implementations and tests.