I am working on the formal verification of gate-level circuits, specifically of approximate circuits. Here, I prove that the formal verification of specific approximate circuits is feasible in polynomial time and space, by giving polynomial upper bounds for the verification complexity.
Polynomial Formal Verification of Approximate Functions
Automated polynomial formal verification using generalized binary decision diagram patterns