  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.
