Understand the benchmarks

The published benchmark is the Ibex RV32 core with two real IHP SRAMs on IHP SG13G2 with the ETH EZ130 8T standard-cell library, run end to end through the native RustEDA flow and compared with LibreLane. Its result is on the RustEDA benchmarks page. This page describes how RustSys synthesis is run, measured and checked inside that benchmark.

Synthesis inside the flow

RustSys runs as an ordinary workspace step of the native flow. rusteda init and rusteda import load the RTL with the EZ130 and SRAM Liberty libraries into a fresh workspace, rustsys synth --base-rev maps the design, and rusteda export writes the mapped netlist that the later repair, placement, routing and signoff stages consume. The two SRAMs are opaque macros during synthesis. The agent workflow describes the same commands.

Measurement boundary

The synthesis step runs under the flow's step time limit and resource guard. Its time is part of the flow's end-to-end wall clock: following the RustEDA benchmark method, the clock starts from prepared RTL and ends only when GDS and the required verification results are complete. The benchmark reports that whole-flow time. This documentation publishes no separate synthesis-only time.

Equivalence

The flow's synthesis equivalence gate proves the synthesized netlist equivalent to the original RTL; its final equivalence gate does the same for the final netlist. Each gate binds the hashes of the RTL and of the netlist it checks, and a gate that is not proven fails the run. A successful synthesis exit status is not evidence of equivalence.

The proof uses two-valued RTL event semantics: ordinary X/Z data is completed to zero, original and implementation initial states stay arbitrary, and no reset or input assumption is added. It does not establish four-state refinement or the equivalence of the SRAM macro internals; the flow exercises both SRAMs separately in simulation against the vendor models. The checking guide explains this semantic model.

Earlier synthesis-only campaigns

Earlier synthesis-only campaigns on other designs and libraries are no longer published as benchmark results. Their dated archives of raw timing, quality and proof receipts remain under verification/benchmarks/open-hardware/results/; the reproduction guide lists their pinned inputs and commands. Verification evidence describes their proof scopes and the proof invalidation registry, and CPU performance and scaling describes the harness method.