VerA: Fully Automatic Formal Verification of Arithmetic Circuits

点击翻译按钮获取中文摘要

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.