BNSynth: Bounded Boolean Functional Synthesis

TL;DR

BNSynth introduces a neural-guided, bounded approach to Boolean functional synthesis, producing smaller solutions with significant size reductions, applicable in resource-constrained design scenarios.

Contribution

First tool to solve Boolean Functional Synthesis with a solution space bound, enabling smaller, resource-efficient Boolean functions.

Findings

Achieves 3.2X to 24X reduction in solution size compared to existing tools.

Uses counter-example guided neural approach for bounded BFS.

Demonstrates promising results on benchmark problems.

Abstract

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.