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.