VerA: Fully Automatic Formal Verification of Arithmetic Circuits

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

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.