OpenROAD-SYN status: asap7 Bazel syn_test suite, QoR/runtime/clock-period graphs, opt-in LEC

[oharboe]

Status report for OpenROAD-SYN (SYNTH_USE_SYN=1) across the asap7 design suite, now wired into Bazel via the config.mk DSL.

What this adds

• SYNTH_USE_SYN is first-class in the Bazel DSL: both synthesis engines are supported, and a design's config.mk value selects its regular flow's engine (gcd's local_arguments workaround is gone). Carried as four git_override patches on the pinned bazel-orfs commit (patches/bazel-orfs/), to be upstreamed when churn settles.
• bazelisk test //flow/designs/asap7:syn_test — synthesis-only OpenROAD-SYN QoR gates for 14 designs, failing designs included by design: this is a status suite. The gate checks the synthesis-stage subset of the design's regular rules-base.json (checkMetadata.py --only-prefix), so no per-variant rules files are committed; the generated synthesis rules snapshot (<name>_syn_update_rules) feeds the clock-period plot instead.
• Status graphs as plain bazelisk build targets (matplotlib from the pip hub, no host deps), checked into flow/docs/images/:
  • //flow/designs/asap7:syn_qor_png — QoR deltas + runtime A/B, failed designs rendered as hatched columns via best-effort _qor targets
  • //flow/designs/asap7:clock_period_png — effective clock period across stages from the checked-in rules-*.json alone
• Opt-in RTL-vs-netlist LEC (SYNTH_LEC_CHECK=1, make-side): kepler-formal compares the input RTL (experimental slang frontend) against the new always-written 1_synth.v.
• Fixes surfaced along the way: the Bazel synth stage never declared logs/1_synth.json, so metadata-check could not see any synth__* metrics (broke every Bazel <design>_test with synth rules); bazelisk run <design>_update was broken by a two-source cp; genMetrics.py now tolerates synthesis-only trees.

Where OpenROAD-SYN stands on asap7

design	OpenROAD-SYN synthesis	notes
gcd, gcd-ccs	✅ pass	1.7% less area, 12% fewer instances than yosys
uart	✅ pass	yosys baseline itself is broken in Bazel today (read_slang plugin fails to load; pre-existing)
aes, aes_lvt, aes-mbff	✅ pass	~9% less area, ~22% fewer instances; up to 68% faster synthesis
jpeg, jpeg_lvt	✅ pass	slightly more area (+3–5%), fewer instances, positive WS
ethmac, ethmac_lvt	✅ pass	area parity, ~90% slower than yosys
aes-block	❌ QoR gate fail	hierarchical BLOCKS; synthesizes, but +157% area blows past the yosys-derived rules-base gate
mock-alu	❌ fail	SDC references yosys-style register names (*io_out_REG*) absent from the SYN netlist
riscv32i	❌ fail	slang rejects procedural assignment to nets (dmem.v)
mock-cpu	❌ fail	slang rejects endianness-mismatched part-select (wptr_full.v)
ibex	⏱ excluded	synthesis completes in seconds; report_metrics STA spins >2h on 48 threads
cva6	⏱ excluded	synthesize takes 73s but repair_design -pre_placement still running after 10+ min when cut off
swerv_wrapper, riscv32i-mock-sram	⏱ excluded	large/hierarchical; not yet run to completion

Excluded designs are documented in SYN_SLOW_DESIGNS (flow/designs/asap7/BUILD); their manual per-design targets remain for reproduction.

LEC status (kepler-formal)

The wiring works end-to-end (flist generation, YAML config, verdict grep), but kepler-formal's experimental SystemVerilog frontend cannot yet lower even gcd's RegEn sequential block ("fallback currently supports only multi-LHS reset branches"), so SYNTH_LEC_CHECK is a separate opt-in from LEC_CHECK — otherwise installing kepler-formal would break make synth for every SYN design. Hermetic Bazel-built kepler-formal was investigated and parked: its naja cmake superbuild needs system Boost/CapnProto/TBB and -lstdc++, which cannot work under the zero-sysroot hermetic toolchain (the deps.bzl @@// → Label() fix and a BCR onetbb dependency get kepler's own sources compiling and are worth upstreaming to keplertech/kepler-formal).

Refreshing the graphs

bazelisk build //flow/designs/asap7:syn_qor_png //flow/designs/asap7:clock_period_png
cp -f bazel-bin/flow/designs/asap7/openroad-syn-*.png flow/docs/images/

🤖 Generated with Claude Code

[oharboe]

@povik @maliberty I took OpenROAD SYN for a spin.

[gemini-code-assist]

Code Review

This pull request integrates OpenROAD-SYN support into the design flow, enabling a synthesis-only variant and a best-effort synthesis QoR reporting suite for asap7 designs. Key changes include adding Bazel patches for bazel-orfs, implementing new QoR reporting targets and plotting utilities, and integrating formal equivalence checking (LEC) for synthesis. The build configuration was updated to support these status targets, and a minor improvement was suggested to refactor a dictionary comprehension in design.bzl for better readability and efficiency.

[oharboe]

@povik It is enormously much further along than the first time I tried it. 🤠

[oharboe]

Closing this in favor of a narrower follow-up PR that carries only the immediate concern: a local Bazel counterpart of the Jenkins QoR signal (https://dashboard.precisioninno.com/), so OpenROAD-SYN can be iterated on locally with fast, targeted feedback — on any design, including designs not yet officially switched to SYN, with a forced-yosys comparison still available after a switch.

The rest of this PR is parked, not abandoned:

• SYNTH_LEC_CHECK (opt-in RTL-vs-netlist LEC) waits for kepler-formal's experimental SystemVerilog frontend to become more capable (today it cannot lower even gcd's RegEn block).
• Hermetic Bazel deployment of kepler-formal needs upstream work in its naja cmake superbuild (system Boost/CapnProto/TBB).
• The QoR/runtime/clock-period status graphs are superseded by the dashboard.

Everything here remains in this closed PR / the openroad-syn-status branch and can be revived when those pieces mature.

[oharboe]

The narrower follow-up PR is #4365 (bazel-orfs side merged as The-OpenROAD-Project/bazel-orfs#771).