原创：ACM 计算机学会

2024年07月18日 11:30 北京

SAT 求解器的快速发展使得将精确合成编码为 SAT 问题求解成为可能。本文首次提出了一种基于增量 SAT 的精确合成流 IncSyn 。通过定义辅助函数和相应的启发式算法， IncSyn 可以利用之前计算的最优实现的拓扑信息和最优子电路。实验表明，IncSyn 在限定时间内实现了12个输入函数的规模提升目标，并且在测试基准上达到了15倍的加速。它还在库构建和动态重写的实际应用中显示了有效性，而且执行时间要少得多。这篇来自北京大学研究团队的研究荣获GLSVLSI 2024最佳论文奖，收录在GLSVLSI '24: Proceedings of the Great Lakes Symposium on VLSI 2024。下面，让我们来进一步了解下这篇研究。

GLSVLSI2024

最佳论文奖

基于增量式SAT的精确综合

Incremental SAT-based Exact Synthesis

作者：Sunan Zou, Jiaxi Zhang，Guojie Luo（北京大学）

精确综合是逻辑综合中根据给定布尔函数生成最优电路的一项关键技术。SAT 求解器的最新进展使基于 SAT 的方法变得可行。然而，难以控制和不可预测的执行时间以及潜在的降质和运行时开销限制了它的应用。为了缓解此类限制，作者们提出了一种基于增量式 SAT的精确综合方法（IncSyn）。该方法利用先前的知识来加速寻找新的最优电路。IncSyn 可揭示函数之间的关系，并相应地修改编码和综合流程。作者们将精确综合的速度提高了15倍，并实现了规模上的进步，在容许时间内解决了多达12个输入的布尔函数的大量案例。该方法将最优库构建和动态重写的平均运行时间分别缩短了6%和64%。

作者评论：

数字逻辑电路的面积最小化问题在逻辑综合中有广泛的应用，以往基于可满足性求解器（SAT）精确综合方法指数增长的运行时间限制了其大规模使用。本文提出利用已生成的最优电路作为辅助，增量式地求解更大规模电路的新方法，并给出了经验性的已生成电路选择规则。基于已生成电路，本文构造了基于最优子结构和基于拓扑结构的增量求解方法，极大地缩小了搜索空间。相较于此前的方法，该增量求解法扩大了可求解的问题规模，并实现了数十倍的加速。

查看原文：

https://doi.org/10.1145/3649476.3658739

查看GLSVLSI '24: Proceedings of the Great Lakes Symposium on VLSI 2024 完整论文录：

https://dl.acm.org/doi/proceedings/10.1145/3649476

本文转载自《最佳论文奖丨北京大学罗国杰教授团队提出基于增量式SAT的精确综合新方法》 by ACM 计算机学会

原文链接https://mp.weixin.qq.com/s/PfHjd462AGqeymyeLqUTnQ