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.

如今，算术电路在许多计算密集型应用（如信号处理和密码学）以及即将到来的人工智能架构（如机器学习和深度学习）中发挥着至关重要的作用。算术电路的多样性非常巨大，涵盖了从三角函数到浮点平方根的各种不同运算。尽管如此，几乎所有复杂的运算都可以使用四种基本运算来执行：加、减、乘和除。为了满足高速、低功耗和小面积设计的要求，已经提出了各种各样的算术单元结构。这些架构利用复杂的算法来优化不同的实现方面。因此，它们通常是广泛并行的并且结构复杂，这使得确保这种算术电路实现的正确性极具挑战性。我们设想了一种全自动的形式化验证方法，它超越了基于不完全模拟的方法和基于定理证明的半自动方法，这些方法仍然是目前的状态，在工业实践中，算术电路验证的一种技术。只有形式验证才能对算术电路的正确性提供严格的保证。* 完全自动化 * 是必要的，因为电路的设计包含算术现在不仅局限于主要的处理器供应商，但也是由许多不同的供应商的专用嵌入式硬件谁不能聘请大型团队的专业验证工程师能够提供人工辅助定理证明。因此，在过去的几年里，对算术电路的自动化形式验证的需求大幅增加。在这个项目中，我们专注于算术电路验证中最具挑战性的任务，即在门级验证包含复杂和高度优化的工业乘法器和除法器的电路。鉴于这个问题已经开放了很长一段时间，最近的进展基于符号计算机代数的验证鼓励，我们坚信，这是理想的时间来解决这个问题。