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.