基于电路割宽特性的布尔可满足性多项式形式验证方法研究

为解决集成电路设计复杂度增加导致的验证难题，研究人员开展基于电路割宽(Cutwidth)特性的布尔可满足性(SAT)验证方法研究。通过提出两种SAT验证方法——电路CNF割宽分解验证和电路AIG割宽分解验证，证明了验证时间复杂度可由电路割宽参数化界定。实验证明该方法能线性时间验证加法器等具有恒定割宽的电路类，为多项式形式验证(PFV)领域提供了新的高效解决方案。

　　

随着摩尔定律的持续演进，集成电路设计复杂度呈指数级增长，硬件设计过程中的错误风险显著增加。传统仿真验证方法无法保证100%覆盖率，而形式验证方法虽然能确保完全正确性，但其普遍存在的指数级时间复杂度成为制约实际应用的瓶颈。在这个背景下，多项式形式验证(Polynomial Formal Verification, PFV)作为一个新兴研究领域应运而生，旨在开发具有可预测多项式时间和空间复杂度的验证方法。

在众多形式验证技术中，布尔可满足性(Boolean Satisfiability, SAT)因其灵活性和高效性成为主流选择，但其NP完全性本质导致最坏情况下仍面临指数级复杂度。此前研究多集中于使用二元决策图(Binary Decision Diagrams, BDD)实现PFV，而对SAT在PFV中的应用潜力缺乏系统探索。Luca Müller和Rolf Drechsler的这项研究填补了这一空白，相关成果发表在《Microprocessors and Microsystems》上。

研究团队采用了两种创新性技术路线：首先是基于电路CNF(Circuit-CNF)的割宽分解验证，通过开发具有确定性行为的缓存式SAT求解器(CacheSAT)，利用电路隐含子句特性约束搜索空间；其次是基于电路AIG(And-Inverter Graph)的割宽分解验证，通过将电路分解为多个子图并建立输出表传递验证信息。实验采用三种典型加法器架构（波纹进位加法器RCA、进位跳跃加法器CSKA和先行进位加法器CLA）作为案例研究，输入规模从32位扩展至10240位。

在电路CNF割宽分解验证方面，研究证明验证时间复杂度可参数化为电路CNF的割宽。通过精心设计的变量排序，研究人员展示了三种加法器架构的恒定割宽特性：RCA为4，CSKA和CLA均为8。实验数据表明，当输入规模从32位增至1024位时，所需验证的独特一致子公式(Distinct Consistent Sub-Formulas, DCSF)数量呈线性增长，验证时间从0.2秒增至243.2秒（RCA），完全符合理论预期。

在电路AIG割宽分解验证方面，研究建立了更精细的复杂度分析框架。通过将电路分解为多个简化子图(Reduced Subgraphs)，证明每个子图的SAT实例变量数受常数限制。关键发现包括：RCA的AIG割宽为2，CSKA为4，CLA为8。实验采用并行计算策略，在32线程环境下，10240位CLA验证时间仅需265.7秒，显著优于此前ASP(Answer Set Programming)方法的500.3秒。

这项研究的理论突破体现在多个方面：首次严格证明了SAT验证时间复杂度可由电路割宽参数化界定；明确了具有恒定割宽的电路类可实现线性时间验证；为加法器类电路建立了完整的复杂度分析框架。在实践层面，研究提出的验证方法可直接应用于工业级EDA工具链，其并行计算架构特别适合现代多核处理器环境。

讨论部分指出，相比传统BDD方法，SAT验证具有更好的可扩展性和灵活性；而与ASP方法相比，SAT在并行计算方面展现出明显优势。研究人员特别强调，虽然两种验证方法都适用于PFV，但电路AIG分解在实际运行效率上更具优势，这主要得益于其对现代SAT求解器的良好兼容性。

这项研究为集成电路形式验证领域开辟了新方向，其理论框架可扩展至更广泛的电路类型验证。未来工作将聚焦于三个方向：优化分解算法自动化程度、探索近似电路验证应用、以及开发专用SAT求解器加速技术。这些进展将进一步提升该方法在工业级芯片验证中的实用价值。