HKU Open-Sources AI Chip Design Agent with Lean 4 Theorem Proving

Overview

A research team from Hong Kong University has open-sourced a chip design agent infrastructure comprising two layers: CKTLean , a typed hardware description language embedded in Lean 4 with a compiler and interactive REPL, and CktFormalizer , an agent framework that orchestrates large language models and tools to generate, repair, optimize, and formally verify circuits. The system takes natural language specifications and produces physical layouts (GDSII) while providing machine-checked equivalence proofs at the source-code level.

System Architecture

The workflow consists of five stages:

Input Specification : Natural language description, reference designs, and Lean example code.

Code Generation (purple): The LLM writes Lean code and iteratively fixes errors via a "modify–compile–diagnose" loop (up to 100 interaction rounds, 40 for initial generation).

Formal Verification (cyan): The agent constructs a Lean theorem stating equivalence between the formal specification and the compiled circuit, using the REPL to obtain proof goals and diagnostics.

Synthesis & Physical Design (orange): CKTLean exports SystemVerilog, which passes through functional simulation, logic synthesis, and place-and-route using the SkyWater 130 nm PDK and OpenROAD.

PPA Optimization (pink): Area, timing, and power metrics are fed back to the agent, which modifies the Lean code, re-verifies equivalence, and keeps the best version; failed optimizations are rolled back.

All tools run in a Docker environment. Final artifacts include Lean source, equivalence proofs, SystemVerilog, GDSII layout, and PPA metrics.

Motivation: Beyond Simulation-Based Verification

Current LLM-based RTL generation typically emits Verilog directly and relies on simulation for validation. The authors identify two shortcomings:

Syntax checking and RTL simulation cannot guarantee full correctness: syntax checks only ensure grammatical validity, while simulation covers limited test trajectories and cannot prove equivalence to the original spec or guarantee physical implementability.

PPA optimization amplifies the problem because each design change must preserve functionality and still pass synthesis and physical implementation.

Raising the abstraction level (e.g., Chisel, Bluespec, Clash) helps manage complexity but still requires correctness guarantees. The team chose to combine hardware description with machine-checkable reasoning in Lean 4.

CKTLean: Typed Hardware IR and Verification Foundation

CKTLean extends the open-source Sparkle HDL . Using 17 representative hardware tasks from CVDP, the team identified five limitations in Sparkle: stateful parameterized designs, memories, bit manipulations, signed arithmetic, and multi-clock designs. CKTLean extends the typed intermediate representation and compilation flow to cover these scenarios and provides a persistent Lean REPL for interactive type checking and theorem proving.

In this representation, bit-widths are part of types, pattern matching must be exhaustive, and mismatches are caught at type-check time—giving the model precise, location-specific diagnostics before simulation.

CktFormalizer: Agent Loop for Generation and Evaluation

On top of CKTLean, CktFormalizer schedules the LLM, compiler, and backend tools. The basic evaluation pipeline has four steps:

Generation : Agent writes Lean, repairs via compiler feedback (100-round budget).

Export : Automatic SystemVerilog generation after successful compilation.

Functional Verification : Simulation with the benchmark's testbench (results not fed back to the agent in this evaluation).

Physical Implementation : Synthesis, place-and-route, DRC, LVS, and gate-level simulation using SkyWater 130 nm and OpenROAD.

Benchmark Evaluation: Four Suites, 430 Tasks

The paper evaluates on four public benchmarks, notably CVDP (168 tasks) which closely mirrors real RTL design and verification, covering state machines, arithmetic datapaths, interconnects, and memories.

Full-System Comparison vs. Direct Verilog Generation

Two baselines use the same LLM and interaction budget to generate SystemVerilog directly. On ResBench , synthesis pass rates for the Verilog baselines were 60.5% and 57.4%, while CktFormalizer + CKTLean achieved 100% . Post-route gate-level simulation pass rates were 88.2% (RTLLM) and 100% (ResBench), both higher than the baselines.

Ablation: CKTLean vs. Original Sparkle

Keeping the CktFormalizer agent fixed and swapping only the backend:

On CVDP: compilation pass rate rose from 77.4% to 91.1%; synthesis pass rate from 67.4% to 100%; fully clean designs (synthesis, PNR, DRC, LVS all pass) from 67.4% to 97.1%.

On ResBench: fully clean designs from 95.3% to 100%.

However, CVDP post-route gate-level simulation remains a challenge for all methods (~27–33% pass rate).

Further Explorations

Microarchitecture Exploration

On 63 complex VerilogEval tasks, the model generated 4 distinct microarchitectures per design. 27 designs yielded multiple synthesizable candidates; 10 achieved >5% area reduction. Six case studies showed area reductions of 9.9%–35.2% and post-route power reductions of 2.0%–30.3% (largest on a state machine).

Agentic Loop for Equivalence Proofs

The agent formulates equivalence as a Lean theorem and iteratively builds the proof: propose step → query REPL for goals/diagnostics → revise. On 30 VerilogEval tasks, this loop raised proof completion from 53.3% (16/30) to 63.3% (19/30) and compilation pass rate from 77% to 100%. The proof establishes source-level equivalence under given assumptions; it does not guarantee the formal spec matches natural language intent nor cover the Lean-to-SystemVerilog compilation.

Closed-Loop PPA Optimization

Starting from existing designs, the agent modifies Lean code based on synthesis area and cell-count feedback, recompiles, resimulates, and resynthesizes. Accepted candidates are kept; others are rolled back. Over 5 iterations, 54 designs entered the loop, 31 reduced area, 28 by >5%. The best case shrank from 196 μm² to 81 μm² ( 58.6% reduction ). Adding post-route timing feedback improved setup slack from −0.37 ns to +0.35 ns on a tight-clock design, achieving timing closure where area-only feedback failed.

Open-Source Release

The project is under Apache-2.0. The repository contains three main parts:

CKTLean ( Sparkle/): typed hardware language, compiler frontend, SystemVerilog backend.

CktFormalizer ( cktarchon/ and agent/): agent loop for Lean generation, compilation checks, sandboxed file I/O, benchmark adapters and scoring.

Experiment Scripts ( experiments/): launch scripts, backend evaluation pipelines, and direct-Verilog baselines.

Requirements: Lean 4 (via elan), Python 3.13, Icarus Verilog. Dependency management uses uv.

git clone <repo-url> cktlean
cd cktlean
lake build
uv sync

Run VerilogEval benchmark:

uv run python -m cktarchon.run --dataset verilogeval \
  --results-dir results/verilogeval --workers 4

Add --synth --pnr --drc --lvs to continue through physical implementation. Use cktarchon.run_verilog for the direct-Verilog baseline.