Neural Circuit Synthesis from Specification Patterns
This addresses the challenge of limited training data for machine learning approaches in LTL synthesis, an incremental improvement for hardware design automation.
The paper tackles the problem of synthesizing hardware circuits from high-level logical specifications in linear-time temporal logic (LTL) by training hierarchical Transformers on synthetic data generated from common patterns mined from competition specifications, resulting in solving a significant portion of competition problems and out-of-distribution examples.
We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic (LTL). The LTL synthesis problem is a well-known algorithmic challenge with a long history and an annual competition is organized to track the improvement of algorithms and tooling over time. New approaches using machine learning might open a lot of possibilities in this area, but suffer from the lack of sufficient amounts of training data. In this paper, we consider a method to generate large amounts of additional training data, i.e., pairs of specifications and circuits implementing them. We ensure that this synthetic data is sufficiently close to human-written specifications by mining common patterns from the specifications used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve a significant portion of problems from the synthesis competitions, and even out-of-distribution examples from a recent case study.