用于晶体管级集成电路形式化验证的建模技术：性能与精度之间的权衡

《IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems》：Modeling Techniques for the Formal Verification of Integrated Circuits at Transistor-Level: Performance Versus Precision Tradeoffs

本文提出基于形式方法的新电路验证框架，通过改进和新增晶体管级语义模型，结合SMT求解器有效探索电路状态空间，解决传统方法无法覆盖的电过载（EOS）检测问题，并通过实验验证了新语义的有效性。

　　

摘要：

任何电子系统的行为都可以追溯到其组成部件之间的物理相互作用方式。这些低级别的相互作用解释了特定电路状态在物理上是如何实现的。某些电路状态可能是错误的，例如，施加的电压应力超过了某个器件的承受范围。了解这种错误是否可能发生在给定的电路上非常重要，以便可以采取必要的纠正措施。识别错误需要某种电路建模技术以及一种探索电路模型状态空间的方法（如果状态空间是有限的，那么这个空间可能会非常庞大）。在这项工作中，我们展示了传统验证技术的局限性，并提出了一种基于形式化方法的新方法来克服这些局限性。我们为晶体管级别的描述提出了新的电路语义，方法包括：1）回顾和改进现有的语义；2）引入新的替代语义。然后，我们在验证框架中展示了这些新语义的使用情况，该框架利用了满足性模理论（SMT）求解器来验证电路的特定电气特性。具体来说，我们解决了寻找受到电气过应力（EOS）影响的电路晶体管的问题。通过形式化比较和实验基准测试，我们得出了有趣的结论。

引言

验证是集成电路设计流程中的一个关键阶段，它占据了整个项目时间的50%到60%[1]。尽管现有的验证技术很多，但新的专用集成电路（ASIC）设计仍然可能存在逻辑和功能上的缺陷，其中60%的缺陷是由设计错误引起的[2]。理想的验证流程应该是既可靠（即从不遗漏任何实际错误）又可扩展的。然而，在实践中，同时实现这两个特性非常困难，这导致许多设计错误直到产品制造完成后才被发现。验证工具的不可靠性通常是由于：1）对电路行为的错误假设，导致某些电路状态在电路的抽象建模中被忽略[3]；或者2）没有考虑电路的完整状态空间（如果考虑连续的电压区间，状态空间可能会非常庞大甚至无限）。实际上，一个复杂的电路的具体状态空间无法通过枚举方式完全覆盖，但具体的电路执行可以覆盖其一个具有代表性的子集。另一方面，形式化方法可以更全面地探索状态空间的抽象。为了确保验证的可靠性，需要对电路行为做出保守的假设。然而，验证工具中使用的建模越粗糙，工具报告误报的概率就越高。只有通过提高精度才能避免误报。然而，精确的技术（例如仿真）无法很好地扩展到大型设计中。因此，找到一个良好的性能/精度平衡点非常困难。