Polynomial Formal Verification of Arithmetic Circuits
By Alireza Mahzoon, University of Bremen, Germany, mahzoon@uni-bremen.de | Rolf Drechsler, University of Bremen, Germany and DFKI GmbH, Germany, drechsler@uni-bremen.de
Abstract
In recent years, significant effort has been put into developing formal verification approaches by both academic and industrial research. In practice, these techniques often give satisfying results for some types of circuits, while they fail for others. A major challenge in this domain is that the verification techniques suffer from unpredictability in their performance. The only way to overcome this challenge is the calculation of bounds for the space and time complexities. If a verification method has polynomial space and time complexities, scalability can be guaranteed.
In this monograph, we propose Polynomial Formal Verification (PFV) of arithmetic circuits. We discuss the importance and advantages of PFV. Subsequently, we prove that PFV of different types of arithmetic circuits, including adders, multipliers, and Arithmetic Logic Units (ALUs) is possible. Furthermore, we calculate the exact upper-bound space and time complexities of verifying these circuits.
Polynomial Formal Verification of Arithmetic Circuits
In recent years, significant effort has been put into developing formal verification approaches in both academic and industrial research. In practice, these techniques often give satisfying results for some types of circuits, while they fail for others. A major challenge in this domain is that the verification techniques suffer from unpredictability in their performance. The only way to overcome this challenge is the calculation of bounds for the space and time complexities. If a verification method has polynomial space and time complexities, scalability can be guaranteed.
In this monograph, Polynomial Formal Verification (PFV) of arithmetic circuits is evaluated. The importance and advantages of PFV are discussed, and subsequently it is proved that PFV of different types of arithmetic circuits, including adders, multipliers, and Arithmetic Logic Units (ALUs), is possible. Furthermore, the exact upper-bound space and time complexities of verifying these circuits are calculated.
