Automatically designing fast and space-efficient digital circuits is challenging because circuits are discrete, must exactly implement the desired logic, and are costly to simulate. We address these challenges with CircuitVAE, a search algorithm that embeds computation graphs in a continuous space and optimizes a learned surrogate of physical simulation by gradient descent. By carefully controlling overfitting of the simulation surrogate and ensuring diverse exploration, our algorithm is highly sample-efficient, yet gracefully scales to large problem instances and high sample budgets. We test CircuitVAE by designing binary adders across a large range of sizes, IO timing constraints, and sample budgets. Our method excels at designing large circuits, where other algorithms struggle: compared to reinforcement learning and genetic algorithms, CircuitVAE typically finds 64-bit adders which are smaller and faster using less than half the sample budget. We also find CircuitVAE can design state-of-the-art adders in a real-world chip, demonstrating that our method can outperform commercial tools in a realistic setting.

In this work, we introduce GraPhSyM, a Graph Attention Network (GATv2) model for fast and accurate estimation of post-physical synthesis circuit delay and area metrics from pre-physical synthesis circuit netlists. Once trained, GraPhSyM provides accurate visibility of final design metrics to early EDA stages, such as logic synthesis, without running the slow physical synthesis flow, enabling global co-optimization across stages. Additionally, the swift and precise feedback provided by GraPhSym is instrumental for machine-learning-based EDA optimization frameworks. Given a gate-level netlist of a circuit represented as a graph, GraPhSyM utilizes graph structure, connectivity, and electrical property features to predict the impact of physical synthesis transformations such as buffer insertion and gate sizing. When trained on a dataset of 6000 prefix adder designs synthesized at an aggressive delay target, GraPhSyM can accurately predict the post-synthesis delay (98.3%) and area (96.1%) metrics of unseen adders with a fast 0.22s inference time. Furthermore, we illustrate the compositionality of GraPhSyM by employing the model trained on a fixed delay target to accurately anticipate post-synthesis metrics at a variety of unseen delay targets. Lastly, we report promising generalization capabilities of the GraPhSyM model when it is evaluated on circuits different from the adders it was exclusively trained on. The results show the potential for GraPhSyM to serve as a powerful tool for advanced optimization techniques and as an oracle for EDA machine learning frameworks.

Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection—a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): an LLM-based prover augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 98,734 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.

In this work, we present a reinforcement learning (RL) based approach to designing parallel prefix circuits such as adders or priority encoders that are fundamental to high-performance digital design. Unlike prior methods, our approach designs solutions tabula rasa purely through learning with synthesis in the loop. We design a grid-based state-action representation and an RL environment for constructing legal prefix circuits. Deep Convolutional RL agents trained on this environment produce prefix adder circuits that Pareto-dominate existing baselines with up to 16.0% and 30.2% lower area for the same delay in the 32b and 64b settings respectively. We observe that agents trained with open-source synthesis tools and cell library can design adder circuits that achieve lower area and delay than commercial tool adders in an industrial cell library.

Reinforcement learning (RL) has gained attention recently as an optimization algorithm for chip design. This method treats many chip design problems as Markov decision problems (MDPs), where design optimization objectives are converted into rewards given by the environment and design variables are converted into actions provided to the environment. Some recent examples include applications of RL to macro placement and standard cell layout routing. We believe RL can be applied to nearly all aspects of VLSI implementation flows, since many VLSI implementation problems are often NP-complete and state-of-art algorithms cannot be guaranteed to be optimal. With enough training data, it is possible to achieve better results with RL. In this paper we review recent advances in applying RL to VLSI implementation problems such as cell layout, synthesis, placement, routing and parameter tuning. We discuss the challenges of applying RL to VLSI implementation flows and propose future research directions for overcoming these challenges.

In recent times, stalling data-paths and virtual channels is becoming increasingly more important for uncovering corner case timing critical bugs in complex hardware design. Generating stimulus to achieve congestion at various virtual channels across numerous interfaces is a hard problem. Hence verification engineers typically mimic such congestion by artificially stalling the interfaces. Artificial stalling often exposes deadlock bugs, violations in ordering rules and credit overflow/underflow issues which escape traditional random simulation. To this end, random First-In First-Out (FIFO) and pipe stalling has played a critical role in Nvidia's simulation environment. While random stalling is useful, it is still not good enough to hit certain coverage metrics in the ever-decreasing time window for verification closure. In this paper, we demonstrate the application of a Genetic Algorithm (GA) framework to improve the efficacy of random stalling as measured by a set of coverage metrics. The GA based framework learns from existing stalling regressions and makes intelligent decisions regarding the Stall Parameters (SP) for achieving better coverage. Finally, we introduce DeepStall - an accelerated GA framework which uses a Deep Learning based model (of the relation function of SP and coverage metric) to tune SPs for better coverage.

We present Graph-Q-SAT, a branching heuristic for a Boolean SAT solver trained with value-based reinforcement learning (RL) using Graph Neural Networks for function approximation. Solvers using Graph-Q-SAT are complete SAT solvers that either provide a satisfying assignment or proof of unsatisfiability, which is required for many SAT applications. The branching heuristics commonly used in SAT solvers make poor decisions during their warm-up period, whereas Graph-Q-SAT is trained to examine the structure of the particular problem instance to make better decisions early in the search. Training Graph-Q-SAT is data efficient and does not require elaborate dataset preparation or feature engineering. We train Graph-Q-SAT using RL interfacing with MiniSat solver and show that Graph-Q-SAT can reduce the number of iterations required to solve SAT problems by 2-3X. Furthermore, it generalizes to unsatisfiable SAT instances, as well as to problems with 5X more variables than it was trained on. We show that for larger problems, reductions in the number of iterations lead to wall clock time reductions, the ultimate goal when designing heuristics. We also show positive zero-shot transfer behavior when testing Graph-Q-SAT on a task family different from that used for training. While more work is needed to apply Graph-Q-SAT to reduce wall clock time in modern SAT solving settings, it is a compelling proof-of-concept showing that RL equipped with Graph Neural Networks can learn a generalizable branching heuristic for SAT search.

As feature size shrinks, routing constraints become a more significant limiting factor to the manufacturability of VLSI designs. Routing congestion significantly impacts quality metrics such as area and timing performance, but congestion is not known accurately until late in the design cycle, after placement and routing. This can lead to unpleasant surprises during the design process. Accordingly, early prediction of routing requirements would enable design engineers to iterate faster, with more confidence that their designs were routable and high quality. Additionally, routability estimates can inform placement itself, preemptively eliminating routing problems. In this work, we present a graph-based deep learning method for quickly predicting logic-induced routing congestion hotspots from a gate-level netlist before placement. This model can provide early feedback to designers and EDA tools, indicating logic that may be difficult to route. Compared to using previous congestion prediction metrics to predict congestion hotspots without placement information, our solution provides a 29% increase in the Kendall ranking correlation score. Because our focus is on predicting congestion due to local logic structure, which manifests itself on lower metal layers, we also report accuracy for predicting lower metal layer congestion. When predicting congestion for the lower metal layers, the benefit of our solution over previous metrics increases to 75%. Additionally, our approach is fast. On a circuit with 1.3 million cells, our approach takes 19 seconds to predict congestion, compared with 10-60 minutes for other methods.