用于降低电路复杂度的先进逆变器图分解技术

《ACM Transactions on Design Automation of Electronic Systems》：Advanced And-Inverter Graph Decomposition Technique for Reducing Circuit Complexity

本文首次将TreeWidth分解技术引入电子设计自动化领域，提出结合CutWidth和TreeWidth的新分解方法，显著降低电路复杂度。实验表明，该方法在ISCAS'85和EPFL基准电路上的复杂度上界较传统方法分别提升90.16倍和1986.37倍，并成功应用于形式验证流程优化。

　　

摘要

在电子设计自动化（EDA）领域，管理电路复杂性是实现高效电路验证、测试和优化的重要任务。随着设计复杂性的增加，形式化验证、故障检测和电路优化等任务面临诸多挑战。因此，降低电路复杂性对于提高这些任务的效率和可扩展性至关重要。这些电路通常被表示为图结构。在参数化复杂性研究领域，CutWidth（CW）和TreeWidth（TW）是两种被广泛研究的分解技术，常用于图算法的分析。本文首次将TW分解技术引入EDA领域，并展示了其在降低电路复杂性方面的效果。此外，我们提出了一种新的分解方法，结合了这两种技术，进一步降低了电路复杂性。我们还通过实验结果对比了不同分解方法得出的复杂性上界，以证明该方法在ISCAS’85和EPFL基准电路上的有效性。实验结果显示，对于ISCAS’85基准电路，我们的分解技术比CW方法的复杂性上界降低了90.16倍；对于EPFL基准电路，该技术比CW方法的复杂性上界降低了94.13倍。最后，为了展示这些分解技术在解决各种EDA问题中的适用性，我们提出了一种新的形式化验证（FV）方法，该方法利用这些技术为验证过程提供复杂性上界。我们对ITC’99、MCNC’91、VHDL算术单元库（ELAU）基准电路、不同长度的加法器电路（最长3072位）以及不同规模的乘法器电路（最大10×10）进行了实验评估，以验证该方法的可扩展性。

最后，为了进一步证明这些分解技术的实用性，我们提出了一种新的形式化验证方法，该方法利用这些技术为验证过程确定复杂性上界。我们还对ITC’99、MCNC’91、VHDL算术单元库（ELAU）基准电路、不同长度的加法器电路（最长3072位）以及不同规模的乘法器电路（最大10×10）进行了实验验证，以验证该方法的可扩展性。