BNSynth: Bounded Boolean Functional Synthesis
This addresses the problem of synthesizing smaller Boolean functions for resource-constrained areas like circuit design, representing an incremental advance with a novel bounded approach.
The paper tackles the Boolean Functional Synthesis (BFS) problem by introducing BNSynth, a tool that synthesizes correct-by-construction Boolean functions under a bound on the solution space, resulting in at least 3.2X and up to 24X improvement in solution size reduction compared to state-of-the-art tools.
The automated synthesis of correct-by-construction Boolean functions from logical specifications is known as the Boolean Functional Synthesis (BFS) problem. BFS has many application areas that range from software engineering to circuit design. In this paper, we introduce a tool BNSynth, that is the first to solve the BFS problem under a given bound on the solution space. Bounding the solution space induces the synthesis of smaller functions that benefit resource constrained areas such as circuit design. BNSynth uses a counter-example guided, neural approach to solve the bounded BFS problem. Initial results show promise in synthesizing smaller solutions; we observe at least \textbf{3.2X} (and up to \textbf{24X}) improvement in the reduction of solution size on average, as compared to state of the art tools on our benchmarks. BNSynth is available on GitHub under an open source license.