论文标题
BNSYNTH：有限的布尔功能合成
BNSynth: Bounded Boolean Functional Synthesis
论文作者
论文摘要
从逻辑规格中正确构建布尔函数的自动合成称为布尔功能合成（BFS）问题。 BFS有许多应用领域，从软件工程到电路设计范围。在本文中，我们介绍了一个工具BNSYNTH，这是第一个在解决方案空间上的给定绑定下解决BFS问题的问题。界限解决方案空间会导致较小功能的合成，从而使资源约束区域（例如电路设计）受益。 BNSYNTH使用反示例的神经方法来解决有限的BFS问题。最初的结果显示了合成较小溶液的希望；与我们的基准测试中的最先进的工具相比，我们至少观察到\ textbf {3.2x}（以及最多\ textbf {24x}）平均减小解决方案大小的改进。 BNSYNTH可在GitHub上获得开源许可证。
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.
