SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning

Yiting Wang (University of Maryland, College Park) · Wanghao Ye (University of Maryland, College Park) · Ping Guo (ByteDance) · Yexiao He (University of Maryland, College Park) · Ziyao Wang (University of Maryland, College Park) · Bowei Tian (University of Maryland, College Park) · Shwai He (University of Maryland, College Park) · Guoheng Sun (University of Maryland, College Park) · Zheyu Shen (Peking University) · Sihan Chen (CMU, Carnegie Mellon University) · Ankur Srivastava (University of Maryland, College Park) · Qingfu Zhang (City University of Hong Kong) · Gang Qu (University of Maryland, College Park) · Ang Li (Austrian Academy of Sciences)
abstract syntax treecompiler-based approachesdigital circuitsfinite state machineformal equivalence checkslarge language modelneuron-symbolic frameworkpower performance arearegister transfer levelretrieval-augmented optimizationstate mergingsymbolic reasoningsyntactic correctnesssynthesis feedbacktest-driven validation

Optimizing Register Transfer Level (RTL) code is crucial for improving the efficiency and performance of digital circuits in the early stages of synthesis. Manual rewriting, guided by synthesis feedback, can yield high-quality results but is time-consuming and error-prone. Most existing compiler-based approaches have difficulty handling complex design constraints. Large Language Model (LLM)-based methods have emerged as a promising alternative to address these challenges. However, LLM-based approaches often face difficulties in ensuring alignment between the generated code and the provided prompts. This paper introduces SymRTLO, a neuron-symbolic framework that integrates LLMs with symbolic reasoning for the efficient and effective optimization of RTL code. Our method incorporates a retrieval-augmented system of optimization rules and Abstract Syntax Tree (AST)-based templates, enabling LLM-based rewriting that maintains syntactic correctness while minimizing undesired circuit behaviors. A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic, allowing fine-grained state merging and partial specification handling beyond the scope of pattern-based compilers. Furthermore, a fast verification pipeline, combining formal equivalence checks with test-driven validation, further reduces the complexity of verification. Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively, compared to the state-of-the-art methods. We will release the code as open source upon the paper's acceptance.