Polynomial Formal Verification of Approximate Functions

During the development of digital circuits, their functional correctness has to be ensured, for which formal verification methods have been established. Here, upper bounds for the BDD size and the time and space complexity are provided for the verification of general approximate functions and several state-of-the-art approximate adders.