RustSys¶
RustSys turns RTL into mapped netlists with bounded synthesis, technology mapping and independently checked equivalence.
Development update · 2026-11-01¶
Opaque SRAM interfaces are now preserved through elaboration, mapping and netlist export. Port widths, bus indices and instance/pin identities are checked; unsupported or inconsistent interfaces produce diagnostics. The macro's behavior continues to come from its original vendor model for independent checking.
Source, evidence and remaining limits
Development status · 2026-10-28¶
The RustEDA integration combines bounded synthesis, BLIF/AIGER and mapped-netlist inputs, revision-bound timing optimization and a shared RustEDA foundation. The earlier Ibex three-library synthesis campaign proves all six RustSys/Yosys netlists equivalent with arbitrary initial state. Real-SRAM preservation for IHP Ibex remains experimental; physical closure is a separate open gate.
Progress, source revisions and verification limits →
Benchmark¶
The published benchmark is the Ibex RV32 core with two real IHP SRAMs on IHP SG13G2 with the ETH EZ130 8T library, run end to end through the native RustEDA flow and compared with LibreLane. RustSys synthesizes the Ibex + SRAM design in that flow; the flow's synthesis and final CEC gates prove the synthesized and final netlists equivalent to the original RTL.
RustEDA benchmarks · RustSys in the whole-flow benchmark
A CLI you can compose¶
-
Start with files. Finish with files.
Read RTL and Liberty. Export gate-level Verilog and a JSON report. Run in a shell, a CI job, or an agent loop.
-
Give agents a contract.
Keep results on standard output and diagnostics on standard error. Use structured errors, bounded tables, revision guards, and explicit exit statuses.
-
Keep the evidence.
Record resolved commands, input hashes, events, and reports. Check the exported netlist with a separate RTL interpreter and SAT solver.
-
Follow the benchmark.
RustSys synthesizes the Ibex + SRAM design in the RustEDA whole-flow benchmark on IHP SG13G2. The flow proves its netlists equivalent to the RTL.
Choose your path¶
| I want to… | Start here |
|---|---|
| Install the CLI and try a small checked design | Installation → quickstart |
| Synthesize my own RTL against a cell library | Synthesis → language support |
| Drive the tools from an agent or CI system | Agent workflow → commands → reports |
| Understand what a proof establishes | Equivalence checking → verification scope |
| Find the published benchmark or assess a performance claim | Benchmarks |
| Scale CPU synthesis and compare area or setup-Fmax | CPU performance and scaling |
| Extend RustSys or another RustEDA tool | Architecture → contributing |
A small first run¶
From the repository root, after building RustSys:
FIX=verification/fixtures/synthetic/synth
rustsys synth --top counter --lib "$FIX/lib/wt_rich.lib" \
--out .work/counter_mapped.v --report .work/counter.json \
"$FIX/rtl/counter/counter.sv"
rustsys check synth --top counter --lib "$FIX/lib/wt_rich.lib" \
--netlist .work/counter_mapped.v "$FIX/rtl/counter/counter.sv"
The bundled library is a small verification fixture. Use a characterized technology library for your own standard-cell targets. The quickstart explains the generated files and verdicts; the agent guide adds recorded runs and machine-readable output.
Preview status
RustSys 0.1.0 is built from source and is not published to crates.io. Supported constructs and analysis limits are documented explicitly. A synthesis success, a timing estimate, and an equivalence proof are separate results.