大规模RTL设计中基于SAT的时态安全属性归纳验证

"这篇论文探讨了在大型RTL(寄存器传输级)设计中验证时态安全属性的有效方法，特别是基于SAT（满足性问题求解）的显式归纳验证技术。作者提出了一种名为‘显式归纳’的新方法，旨在处理时间属性的验证，这是以往方法中未涉及的。他们介绍了ForSpec语言在这一过程中的应用，以及如何在Thunder有界模型检查器中实现这一概念。通过这种方法，他们成功地验证了复杂的大型电路，如奔腾TM4处理器的控制电路，这些电路的规模远超传统模型检查方法能够处理的范围。该研究强调了显式归纳在处理具有广泛反馈的时序安全属性验证中的优势。" 在详细介绍中，文章首先指出形式验证对于确保系统正确性的重要性，特别是在模型检查中，通过检查状态转换图来验证系统是否符合时序逻辑公式。然而，对于大型RTL设计，传统的有界模型检查方法往往因状态空间的爆炸性增长而受限，无法有效处理复杂的时态安全属性。 Shepherd、Singh和Stalmarck提出的“窗口归纳”是一种增强有界模型检验的技术，用于安全属性的无界验证。然而，这种方法并不直接适用于时间属性。为了解决这个问题，Armoni等人提出了“显式归纳”，这是一种新的归纳计划，专门针对时间属性。显式归纳的独特之处在于将归纳方案作为规范的一部分，使其易于控制和调整。这使得使用像ForSpec这样高度表达性的语言来表达和操作归纳证明成为可能。 在实践中，作者展示了如何在ForSpec编译器和Thunder模型检查器中实现显式归纳，并通过实际案例——验证奔腾TM4处理器的控制电路，证明了这种方法的有效性。这些控制电路具有广泛的反馈路径，传统方法难以处理，但通过显式归纳，能够成功验证比传统方法能处理的电路大几个数量级的设计。 此外，这项工作还讨论了如何实施显式归纳并评估其在实际验证任务中的性能。研究得到了NSF、BSF和英特尔公司的资助，并在开放获取许可下发表，可供进一步研究和应用。 关键词涵盖了SAT求解、归纳验证、窗口归纳和安全性，显示了该研究在计算机科学领域，尤其是硬件验证和形式验证方向的重要贡献。通过这种基于SAT的显式归纳方法，研究人员和工程师可以更有效地验证复杂的时态安全属性，从而提高大型电子设计的可靠性和质量。