PolyVer: Polynomial Verification of Electronic Circuits

PolyVer：电子电路的多项式验证

• 批准号: 431649366
• 负责人: Professor Dr. Rolf Drechsler
• 金额: --
• 依托单位: Arbeitsgruppe Rechnerarchitektur und Zuverlässige Eingebettete Systeme
• 依托单位国家: 德国
• 项目类别: Reinhart Koselleck Projects
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/431649366?language=en
• 关键词: PolyVer; Polynomial; Verification; Electronic; Circuits

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.

数字革命极大地改变了我们的生活。在个人计算机，互联网和现代移动设备之后，我们可以观察到传统行业的数字化。这场革命的基础是数字逻辑电路。为了履行其重要角色，电路必须没有错误。Polyver项目的目的是使正式验证技术在极其有用的情况下比目前更有用，即它们将成为验证现实世界数字电路的“瑞士军刀”。 Polyver将从根本上将当今以设计为中心的电路的发展过程从乍看之下完全不可能：在多项式时间和空间中进行正式验证。借助多佛，正式保证，即从数学意义上的证据，在可预测的时间内成为今天的现实和未来的电子系统。为了实现这一目标，Polyver将通过对可拖动电路类的细粒度理解来创建理论基础。然后，将研究每个类别（包括其组成性）的有效（即多项式）决策程序。该项目的主要可交付成果除了理论结果外，还针对电路类的有效实施的验证算法，它们在以验证为中心的流中进行连续集成以及一系列案例研究，以证明多项式验证性的实际好处。