VerA: Fully Automatic Formal Verification of Arithmetic Circuits

VerA：算术电路的全自动形式验证

• 批准号: 436285168
• 负责人: Professor Dr. Rolf Drechsler
• 金额: --
• 依托单位: Institut für Informatik (IIF)
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/436285168?language=en
• 关键词: VerA; Fully; Automatic; Formal; Verification

Today arithmetic circuits play a crucial role in many computationally intensive applications (like signal processing and cryptography) as well as in upcoming AI architectures (e.g. for machine learning and deep learning).The diversity of arithmetic circuits is huge and covers a wide range of different operations from trigonometric functions to floating point square root. Despite this diversity, almost all intricate operations can be performed using four basic operations: addition, subtraction, multiplication, and division.In order to satisfy the demands for high speed, low power, and low area designs, a large variety of architectures have been proposed for arithmetic units. These architectures take advantage of sophisticated algorithms to optimize different implementation aspects. As a result, they are usually extensively parallel and structurally complex which makes it extremely challenging to ensure the correctness of such arithmetic circuit implementations.In the project VerA, we envision a fully automatic formal verification methodology that goes beyond incomplete simulation-based approaches and semi-automatic approaches based on theorem proving which are still the state-of-the-art for arithmetic circuit verification in industrial practice.Only *formal* verification is able to provide rigorous guarantees concerning the correctness of arithmetic circuits. *Full automation* is needed, since thedesign of circuits containing arithmetic is nowadays not only confinedto the major processor vendors, but is also done by many different suppliers of special-purpose embedded hardware who cannot afford to employ large teams of specialized verification engineers being able to provide human-assisted theorem proofs. Thus, the need for an automated formal verification of arithmetic circuits has substantially increased during the last years.In this project, we focus on the most challenging task in arithmetic circuitverification, the verification of circuits containing complex and highly optimized industrial multipliers and dividers at the gate level. Whereas the question has been open for a long time, encouraged by recent advances in verification based on Symbolic Computer Algebra, we strongly believe that it is the ideal time to attack this problem.

如今，算术电路在许多计算密集型应用(如信号处理和密码学)以及即将到来的人工智能体系结构(如机器学习和深度学习)中扮演着至关重要的角色。算术电路的多样性是巨大的，涵盖了从三角函数到浮点平方根的各种不同的运算。尽管存在这种多样性，但几乎所有复杂的运算都可以使用加法、减法、乘法和除法这四种基本运算来执行。为了满足高速、低功耗和低面积设计的要求，已经提出了各种不同的算术单元结构。这些架构利用复杂的算法来优化不同的实现方面。在VERA项目中，我们设想了一种全自动的形式验证方法，它超越了基于不完全模拟的方法和基于定理证明的半自动方法，这两种方法仍然是工业实践中算术电路验证的最新技术，只有*形式*验证才能提供关于算术电路正确性的严格保证。由于如今包含算术的电路的设计不仅限于主要的处理器供应商，而且还由许多不同的专用嵌入式硬件供应商完成，他们负担不起雇用大量专门的验证工程师团队来提供人工辅助定理证明的费用，因此需要*完全自动化*。因此，在过去的几年里，对算术电路的自动化形式验证的需求大大增加。在这个项目中，我们专注于算术电路验证中最具挑战性的任务，即在门级对包含复杂且高度优化的工业乘法器和除法器的电路进行验证。虽然这个问题已经悬而未决很长一段时间了，受到基于符号计算机代数的验证的最新进展的鼓舞，我们坚信现在是解决这个问题的理想时机。