Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification.

翻译：设计验证是一项复杂且成本高昂的任务，尤其对于大型和复杂的处理器项目而言。形式化验证技术通过全面检查设计行为提供了优势，但需要大量人力和在属性制定方面的专业知识。近期研究聚焦于使用自一致性通用属性对设计进行验证，由于其与设计无关性，降低了验证难度。然而，单一的自一致性属性面临误报以及由于指数级状态空间增长导致的可扩展性问题。为应对这些挑战，本文提出TIUP，一种使用重言式作为通用属性的技术。我们展示了TIUP如何有效利用重言式作为抽象规约，覆盖处理器数据路径和控制路径。TIUP简化并优化了工程师的验证流程，实现了高效的形式化处理器验证。