PolyVer: Polynomial Verification of Electronic Circuits

• Applicant: Professor Dr. Rolf Drechsler
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: since 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 431649366

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.

• DFG Programme: Reinhart Koselleck Projects