基于SAT的电路综合方法
SAT-Based Methods for Circuit Synthesis
摘要：
反应式合成通过从声明性规范自动构造正确的硬件来支持设计人员。综合算法通常计算一个策略，然后构造一个实现它的电路。在这项工作中，我们研究了第二步，即基于SAT和QBF的方法，从策略中计算电路。这包括基于QBF认证、插值和计算学习的方法。我们提出了优化，高效的实现，并从安全规范，我们优于BDD的执行时间和电路大小的合成实验结果。这是[2]的扩展版本，带有附加附录。
英文摘要：
Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size. This is an extended version of [2], with an additional appendix.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
