Publikation
Polynomial Formal Verification of Approximate Functions
Martha Schnieber; Saman Fröhlich; Rolf Drechsler
In: IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE Computer Society Annual Symposium on VLSI (ISVLSI-2022), July 4-6, Pafos, Cyprus, 2022.
Zusammenfassung
During the development of digital circuits, their functional correctness has to be ensured, for which formal verification methods have been developed. However, the verification process using formal methods can have an exponential time and space complexity, potentially leading to a failure due to time or space constraints. Thus, in the past years, it has been shown that multiple circuits are guaranteed to be verifiable efficiently in polynomial time and space using specific formal methods. However, the polynomial verifiability of approximate functions, which are beneficial for applications with hardware or time constraints, has not been focused by research yet.
In this paper, we present two methods for generating polynomially verifiable circuits for an approximate function g, if g approximates another function f such that they differ for a polynomial amount of input assignments and a polynomially verifiable circuit for f exists. Using BDDs, we prove the polynomial verifiability of both circuits for g with respect to the number of inputs. Furthermore, for several error metrics, we explore the correlation between the BDD sizes during the verification process of both circuits and the error between f and g. Finally, we experimentally evaluate the given upper bounds for the BDD sizes during the verification process of both circuit architectures for several approximate functions.