Self-referential verification for gate-level implementations of arithmetic circuits

Verification of gate-level implementations of arithmetic circuits is challenging for a number of reasons: the existence of some hard-to-verify arithmetic operators, the use of different operand ordering, the incorporation of merged arithmetic with cross-operator implementations, and the employment of circuit transformations based on arithmetic relations. It is hence a peculiar problem that does not fit well within the existing register-transfer-level-to-gate equivalence-checking methodology. We propose a self-referential functional verification approach which uses the gate-level implementation of the arithmetic circuit under verification to verify itself. The verification task is decomposed into a sequence of equivalence-checking subproblems, each of which compares structurally similar circuit pairs derived from the implementation under verification. These equivalence-checking subproblems represent the functional equations that uniquely define the intended arithmetic function. Based on these self-referential functional equations, a decomposition heuristic using structural information is employed to guide the verification process for better efficiency. Experimental results on a number of implementations of the multipliers, the multiply-add units, and the inner product units with different architectures demonstrate the versatility of this approach.