Polynomial Verification of 2-Affine Spaces

Polynomial Formal Verification (PFV) ensures that a class of circuits can be verified efficiently by calculating polynomial upper bounds for the resource demands of the verification process. In this paper, we address the PFV of Boolean affine spaces represented by a 2-XOR sum of products. We show that time and space resources remain quadratic in the number of input variables during the entire verification process. Specifically, we prove that the dimensions of ROBDDs and QRBDDs representing a 2-affine space are linear. Furthermore, we prove that all ROBDDs generated during the symbolic simulation of the circuit can be computed in linear time. Finally, we provide an overall quadratic upper bound for the formal verification of QRBDD-based circuits. The experimental results confirm the given bounds.