PolyVer: Polynomial Verification of Electronic Circuits

数字革命极大地改变了我们的生活。在个人电脑、互联网和现代移动设备之后，我们可以看到传统行业的数字化正在发生。这场革命的基础是数字逻辑电路。为了发挥它们的重要作用，电路必须没有错误。PolyVer项目的目标是使正式验证技术比目前更有用，即它们将成为验证现实世界数字电路的“瑞士军刀”。PolyVer将从根本上改变当今以设计为中心的电路开发过程，使其严格以验证为中心，这是通过关键的使能器来实现的，乍一看似乎是不可能的：多项式时间和空间的正式验证。使用PolyVer，形式保证，即数学意义上的证明，在可预测的时间内成为今天和未来电子系统的现实。为了实现这一目标，PolyVer将通过获得对可处理电路类的细粒度理解来创建理论基础。然后，将研究每个类的有效（即多项式）决策过程，包括它们的组合性。除了理论结果外，该项目的主要交付成果是一组有效实现的电路类验证算法，它们在以验证为中心的流程中持续集成，以及一系列案例研究，以展示多项式可验证性的实际优势。

The digital revolution changed our lives dramatically. After personal computers, internet and modern mobile devices, we can observe the digitalization of traditional industries taking place. The foundation of this revolution are digital logic circuits. To fulfill their important roles, the circuits have to be free of errors.The goal of the PolyVer project is to make formal verification techniques drastically more useful than they currently are, i.e. they will become the "swiss army knife" for verifying real-world digital circuits. PolyVer will radically change today's design-centric development process of circuits to be strictly verification-centric via the key enabler that seems to be impossible at the first glance: formal verification in polynomial time and space. With PolyVer, formal guarantees, i.e. proofs in a mathematical sense, become reality for todays and future electronic systems in predictable time. To reach this goal, PolyVer will create the theoretical foundations by obtaining a fine-grained understanding of tractable circuit classes. Then, efficient (i.e. polynomial) decision procedures for each class including their compositionality will be investigated. The key deliverables of the project are, in addition to the theoretical results, a set of efficiently implemented verification algorithms for the circuit classes, their continuous integration in a verification-centric flow, as well as a series of case studies to demonstrate the practical benefits of polynomial verifiability.