[Auto] CIRCT PR #10493: [Synth] Add SAT-based exact synthesis pass

[github-actions]

Automatically triggered benchmark for CIRCT PR #10493.

PR Title: [Synth] Add SAT-based exact synthesis pass
Author: uenoku
Created: 2026-05-18T05:52:49Z

Synth files modified:

• include/circt/Dialect/Synth/Transforms/SynthPasses.td
• integration_test/circt-synth/exact-synthesis.mlir
• lib/Dialect/Synth/Transforms/CMakeLists.txt
• lib/Dialect/Synth/Transforms/ExactSynthesis.cpp
• test/Dialect/Synth/exact-synthesis-error.mlir

Datapath files modified:

---

🤖 Benchmarks have been automatically triggered. Combinatorial benchmark results will be posted here when done.

[github-actions]

🤖 Benchmarks triggered for CIRCT PR #10493!

• 🔍 Combinatorial benchmark (with translation validation and equivalence check) — results will be posted here when done
• 🧪 Pass benchmark (AIG/pass track) — results at GitHub Pages when done

Building CIRCT from source before and after the PR; this takes a while.

View combinatorial workflow runs | View pass benchmark runs

[github-actions]

Benchmark results for CIRCT PR #10493

📊 View report | 📦 Artifacts

[Synth] Add SAT-based exact synthesis pass

	Before	After
Commit	c970c420	cf9f53a5
Version	CIRCT c970c42	CIRCT c970c42

Tools: base CIRCT c970c42, pr CIRCT c970c42 | Benchmarks: 158 | Generated: 2026-05-18T06:20:36.525484

Summary (Geometric Mean)

Category	Metric	base	pr
Overall (198 benchmarks)	Gates	720.97	720.97 (0.0%)
	Depth	17.83	17.83 (0.0%)
	Area (ASAP7)	40.18	40.18 (0.0%)
	Delay (ASAP7)	294.47	294.47 (0.0%)
	Area (Sky130)	3555.85	3555.85 (0.0%)
	Delay (Sky130)	1717.5	1717.50 (0.0%)
DatapathBench	Gates	5410.23	5410.23 (0.0%)
	Depth	41	41.00 (0.0%)
	Area (ASAP7)	246.24	246.24 (0.0%)
	Delay (ASAP7)	652	652.00 (0.0%)
	Area (Sky130)	28458.7	28458.74 (0.0%)
	Delay (Sky130)	3771.07	3771.07 (0.0%)
ELAU	Gates	308.41	308.41 (0.0%)
	Depth	12.7	12.70 (0.0%)
	Area (ASAP7)	18.47	18.47 (0.0%)
	Delay (ASAP7)	213.65	213.65 (0.0%)
	Area (Sky130)	1482.74	1482.74 (0.0%)
	Delay (Sky130)	1250.13	1250.13 (0.0%)
microbenchmarks	Gates	484.34	484.34 (0.0%)
	Depth	14.19	14.19 (0.0%)
	Area (ASAP7)	23.31	23.31 (0.0%)
	Delay (ASAP7)	233.57	233.57 (0.0%)
	Area (Sky130)	2338.69	2338.69 (0.0%)
	Delay (Sky130)	1366.59	1366.59 (0.0%)

SMT Translation Validation (bitwuzla)

✔ Pass: 206 | ✘ Fail: 0 | ⚠ Error: 110

Equivalence Check (CEC)

✔ Equivalent: 158 | ✘ Non-equiv: 0 | ⏱ Timeout: 0 | ⚠ Error: 0 | — Skipped: 40

Per-benchmark details

DatapathBench

AddMop_16 (CEC: ✔)

Tool	Gates	Depth	Area (ASAP7)	Delay (ASAP7)	Area (Sky130)	Delay (Sky130)	SMT TV (bitwuzla)
base	369	19	17	329	2107	1861	✔
pr	369 (0.0%)	19 (0.0%)	17 (0.0%)	329 (0.0%)	2107 (0.0%)	1861 (0.0%)	✔

SMT Translation Validation (base)

	From	To
✔	tmpz1aaazekAddMop.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_convert-datapath-to-comb.mlir
✔	0_1_convert-datapath-to-comb.mlir	0_2_canonicalize.mlir
✔	0_2_canonicalize.mlir	0_3_convert-comb-to-synth.mlir
✔	0_3_convert-comb-to-synth.mlir	0_4_cse.mlir
✔	0_4_cse.mlir	0_5_canonicalize.mlir
✔	0_5_canonicalize.mlir	0_6_synth-lower-variadic.mlir
✔	0_6_synth-lower-variadic.mlir	0_7_convert-comb-to-synth.mlir
✔	0_7_convert-comb-to-synth.mlir	0_8_cse.mlir
✔	0_8_cse.mlir	0_9_canonicalize.mlir
✔	0_9_canonicalize.mlir	0_10_synth-lower-variadic.mlir
✔	0_10_synth-lower-variadic.mlir	0_11_synth-structural-hash.mlir
✔	0_11_synth-structural-hash.mlir	0_12_synth-maximum-and-cover.mlir
✔	0_12_synth-maximum-and-cover.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	tmpfwoyspet.synth.mlir

SMT Translation Validation (pr)

	From	To
✔	tmpb20pcp35AddMop.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_convert-datapath-to-comb.mlir
✔	0_1_convert-datapath-to-comb.mlir	0_2_canonicalize.mlir
✔	0_2_canonicalize.mlir	0_3_convert-comb-to-synth.mlir
✔	0_3_convert-comb-to-synth.mlir	0_4_cse.mlir
✔	0_4_cse.mlir	0_5_canonicalize.mlir
✔	0_5_canonicalize.mlir	0_6_synth-lower-variadic.mlir
✔	0_6_synth-lower-variadic.mlir	0_7_convert-comb-to-synth.mlir
✔	0_7_convert-comb-to-synth.mlir	0_8_cse.mlir
✔	0_8_cse.mlir	0_9_canonicalize.mlir
✔	0_9_canonicalize.mlir	0_10_synth-lower-variadic.mlir
✔	0_10_synth-lower-variadic.mlir	0_11_synth-structural-hash.mlir
✔	0_11_synth-structural-hash.mlir	0_12_synth-maximum-and-cover.mlir
✔	0_12_synth-maximum-and-cover.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	tmpw_c_a4ft.synth.mlir

AddMop_48 (CEC: ✔)

Tool	Gates	Depth	Area (ASAP7)	Delay (ASAP7)	Area (Sky130)	Delay (Sky130)	SMT TV (bitwuzla)
base	1545	22	78	373	8726	2188	✔
pr	1545 (0.0%)	22 (0.0%)	78 (0.0%)	373 (0.0%)	8726 (0.0%)	2188 (0.0%)	✔

SMT Translation Validation (base)

	From	To
✔	tmp8gbpxmydAddMop.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_convert-datapath-to-comb.mlir
✔	0_1_convert-datapath-to-comb.mlir	0_2_canonicalize.mlir
✔	0_2_canonicalize.mlir	0_3_convert-comb-to-synth.mlir
✔	0_3_convert-comb-to-synth.mlir	0_4_cse.mlir
✔	0_4_cse.mlir	0_5_canonicalize.mlir
✔	0_5_canonicalize.mlir	0_6_synth-lower-variadic.mlir
✔	0_6_synth-lower-variadic.mlir	0_7_convert-comb-to-synth.mlir
✔	0_7_convert-comb-to-synth.mlir	0_8_cse.mlir
✔	0_8_cse.mlir	0_9_canonicalize.mlir
✔	0_9_canonicalize.mlir	0_10_synth-lower-variadic.mlir
✔	0_10_synth-lower-variadic.mlir	0_11_synth-structural-hash.mlir
✔	0_11_synth-structural-hash.mlir	0_12_synth-maximum-and-cover.mlir
✔	0_12_synth-maximum-and-cover.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	tmpnyawuy3o.synth.mlir

SMT Translation Validation (pr)

	From	To
✔	tmpx8eibhj4AddMop.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_convert-datapath-to-comb.mlir
✔	0_1_convert-datapath-to-comb.mlir	0_2_canonicalize.mlir
✔	0_2_canonicalize.mlir	0_3_convert-comb-to-synth.mlir
✔	0_3_convert-comb-to-synth.mlir	0_4_cse.mlir
✔	0_4_cse.mlir	0_5_canonicalize.mlir
✔	0_5_canonicalize.mlir	0_6_synth-lower-variadic.mlir
✔	0_6_synth-lower-variadic.mlir	0_7_convert-comb-to-synth.mlir
✔	0_7_convert-comb-to-synth.mlir	0_8_cse.mlir
✔	0_8_cse.mlir	0_9_canonicalize.mlir
✔	0_9_canonicalize.mlir	0_10_synth-lower-variadic.mlir
✔	0_10_synth-lower-variadic.mlir	0_11_synth-structural-hash.mlir
✔	0_11_synth-structural-hash.mlir	0_12_synth-maximum-and-cover.mlir
✔	0_12_synth-maximum-and-cover.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	tmpkqdwdwj4.synth.mlir

AddMulSgn_16 (CEC: ✔)

Tool	Gates	Depth	Area (ASAP7)	Delay (ASAP7)	Area (Sky130)	Delay (Sky130)	SMT TV (bitwuzla)
base	3804	44	156	673	19732	4088	⚠
pr	3804 (0.0%)	44 (0.0%)	156 (0.0%)	673 (0.0%)	19732 (0.0%)	4088 (0.0%)	⚠

SMT Translation Validation (base)

	From	To
✔	tmp0g7x9jtlAddMulSgn.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_canonicalize.mlir
⏱	0_1_canonicalize.mlir	0_2_convert-datapath-to-comb.mlir
✔	0_2_convert-datapath-to-comb.mlir	0_3_canonicalize.mlir
✔	0_3_canonicalize.mlir	0_4_convert-comb-to-synth.mlir
✔	0_4_convert-comb-to-synth.mlir	0_5_cse.mlir
✔	0_5_cse.mlir	0_6_canonicalize.mlir
✔	0_6_canonicalize.mlir	0_7_synth-lower-variadic.mlir
⏱	0_7_synth-lower-variadic.mlir	0_8_convert-comb-to-synth.mlir
✔	0_8_convert-comb-to-synth.mlir	0_9_cse.mlir
✔	0_9_cse.mlir	0_10_canonicalize.mlir
✔	0_10_canonicalize.mlir	0_11_synth-lower-word-to-bits.mlir
✔	0_11_synth-lower-word-to-bits.mlir	0_12_cse.mlir
✔	0_12_cse.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	0_15_canonicalize.mlir
✔	0_15_canonicalize.mlir	0_16_synth-maximum-and-cover.mlir
✔	0_16_synth-maximum-and-cover.mlir	0_17_synth-lower-variadic.mlir
✔	0_17_synth-lower-variadic.mlir	0_18_synth-structural-hash.mlir
✔	0_18_synth-structural-hash.mlir	tmprgteeue6.synth.mlir

SMT Translation Validation (pr)

	From	To
✔	tmp26i5q99fAddMulSgn.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_canonicalize.mlir
⏱	0_1_canonicalize.mlir	0_2_convert-datapath-to-comb.mlir
✔	0_2_convert-datapath-to-comb.mlir	0_3_canonicalize.mlir
✔	0_3_canonicalize.mlir	0_4_convert-comb-to-synth.mlir
✔	0_4_convert-comb-to-synth.mlir	0_5_cse.mlir
✔	0_5_cse.mlir	0_6_canonicalize.mlir
✔	0_6_canonicalize.mlir	0_7_synth-lower-variadic.mlir
⏱	0_7_synth-lower-variadic.mlir	0_8_convert-comb-to-synth.mlir
✔	0_8_convert-comb-to-synth.mlir	0_9_cse.mlir
✔	0_9_cse.mlir	0_10_canonicalize.mlir
✔	0_10_canonicalize.mlir	0_11_synth-lower-word-to-bits.mlir
✔	0_11_synth-lower-word-to-bits.mlir	0_12_cse.mlir
✔	0_12_cse.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	0_15_canonicalize.mlir
✔	0_15_canonicalize.mlir	0_16_synth-maximum-and-cover.mlir
✔	0_16_synth-maximum-and-cover.mlir	0_17_synth-lower-variadic.mlir
✔	0_17_synth-lower-variadic.mlir	0_18_synth-structural-hash.mlir
✔	0_18_synth-structural-hash.mlir	tmp0bys0ecv.synth.mlir

AddMulSgn_48 (CEC: ✔)

Tool	Gates	Depth	Area (ASAP7)	Delay (ASAP7)	Area (Sky130)	Delay (Sky130)	SMT TV (bitwuzla)
base	34900	58	1417	909	180592	5554	⚠
pr	34900 (0.0%)	58 (0.0%)	1417 (0.0%)	909 (0.0%)	180592 (0.0%)	5554 (0.0%)	⚠

SMT Translation Validation (base)

	From	To
✔	tmp1zmvlz_kAddMulSgn.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_canonicalize.mlir
⏱	0_1_canonicalize.mlir	0_2_convert-datapath-to-comb.mlir
⏱	0_2_convert-datapath-to-comb.mlir	0_3_canonicalize.mlir
✔	0_3_canonicalize.mlir	0_4_convert-comb-to-synth.mlir
✔	0_4_convert-comb-to-synth.mlir	0_5_cse.mlir
⏱	0_5_cse.mlir	0_6_canonicalize.mlir
⏱	0_6_canonicalize.mlir	0_7_synth-lower-variadic.mlir
⏱	0_7_synth-lower-variadic.mlir	0_8_convert-comb-to-synth.mlir
✔	0_8_convert-comb-to-synth.mlir	0_9_cse.mlir
✔	0_9_cse.mlir	0_10_canonicalize.mlir
✔	0_10_canonicalize.mlir	0_11_synth-lower-word-to-bits.mlir
✔	0_11_synth-lower-word-to-bits.mlir	0_12_cse.mlir
✔	0_12_cse.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	0_15_canonicalize.mlir
✔	0_15_canonicalize.mlir	0_16_synth-maximum-and-cover.mlir
✔	0_16_synth-maximum-and-cover.mlir	0_17_synth-lower-variadic.mlir
✔	0_17_synth-lower-variadic.mlir	0_18_synth-structural-hash.mlir
✔	0_18_synth-structural-hash.mlir	tmpesutp3le.synth.mlir

SMT Translation Validation (pr)

	From	To
✔	tmpd8ob6l8pAddMulSgn.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_canonicalize.mlir
⏱	0_1_canonicalize.mlir	0_2_convert-datapath-to-comb.mlir
⏱	0_2_convert-datapath-to-comb.mlir	0_3_canonicalize.mlir
⏱	0_3_canonicalize.mlir	0_4_convert-comb-to-synth.mlir
✔	0_4_convert-comb-to-synth.mlir	0_5_cse.mlir
⏱	0_5_cse.mlir	0_6_canonicalize.mlir
⏱	0_6_canonicalize.mlir	0_7_synth-lower-variadic.mlir
⏱	0_7_synth-lower-variadic.mlir	0_8_convert-comb-to-synth.mlir
✔	0_8_convert-comb-to-synth.mlir	0_9_cse.mlir
✔	0_9_cse.mlir	0_10_canonicalize.mlir
✔	0_10_canonicalize.mlir	0_11_synth-lower-word-to-bits.mlir
✔	0_11_synth-lower-word-to-bits.mlir	0_12_cse.mlir
✔	0_12_cse.mlir	0_13_synth-lower-variadic.mlir
✔	0_13_synth-lower-variadic.mlir	0_14_synth-structural-hash.mlir
✔	0_14_synth-structural-hash.mlir	0_15_canonicalize.mlir
✔	0_15_canonicalize.mlir	0_16_synth-maximum-and-cover.mlir
✔	0_16_synth-maximum-and-cover.mlir	0_17_synth-lower-variadic.mlir
✔	0_17_synth-lower-variadic.mlir	0_18_synth-structural-hash.mlir
✔	0_18_synth-structural-hash.mlir	tmp63k7ewqk.synth.mlir

AddMulUns_16 (CEC: ✔)

Tool	Gates	Depth	Area (ASAP7)	Delay (ASAP7)	Area (Sky130)	Delay (Sky130)	SMT TV (bitwuzla)
base	2712	40	117	629	13811	3807	⚠
pr	2712 (0.0%)	40 (0.0%)	117 (0.0%)	629 (0.0%)	13811 (0.0%)	3807 (0.0%)	⚠

SMT Translation Validation (base)

	From	To
✔	tmpeoea57r6AddMulUns.mlir	0_0_convert-comb-to-datapath.mlir
✔	0_0_convert-comb-to-datapath.mlir	0_1_canonicalize.mlir
⏱	0_1_canonicalize.mlir	0_2_convert-datapath-to-comb.mlir
✔	0_2_convert-datapath-to-comb.mlir	0_3_canonicalize.mlir
✔	0_3_canonicalize.mlir	0_4_convert-comb-to-synth.mlir
✔	0_4_convert-comb-to-synth.mlir	0_5_cse.mlir
✔	0_5_cse.mlir	0_6_canonicalize.mlir
✔	0_6_canonicalize.mlir	0_7_synth-lower-variadic.mlir
⏱	0_7_synth-lower-variadic.mlir	0_8_convert-comb-to-synth.mlir
✔	0_8_convert-comb-to-synth.mlir	0_9_cse.mlir
✔	0_9_cse.mlir	0_10_canonicalize.mlir
✔	0_10_canonicalize.mlir	0_11_synth-lower-word-to-bits.mlir
✔	0_11_synth-lower-word-to-bits.mlir	0_1

... (truncated, see full report in artifacts)