Verification of hardware design for component that evaluates an algebraic expression using decomposition and recombination

A system for verifying a hardware design for a component that evaluates a main algebraic expression comprising at least two variables, the main algebraic expression being representable as a lossless combination of a plurality of sub-algebraic expressions, and one or more of the at least two variables can be constrained to cause an instantiation of the hardware design to evaluate each of the sub-algebraic expressions, the system comprising:

• memory configured to store:
• the hardware design;
• and
• one or more verification tools comprising one or more formal verification tools;
• and
• one or more processors configured to:
• for each of the plurality of sub-algebraic expressions, verify, using the one or more verification tools, that an instantiation of the hardware design generates a correct output to that sub-algebraic expression for valid values of each variable in that sub-algebraic expression;
• and
• for each of one of more combinations of sub-algebraic expressions, formally verify, using the one or more formal verification tools, that an instantiation of the hardware design generates a correct output to that combination of sub-algebraic expressions by comparing an output of an instantiation of the hardware design under a first set of constraints to an output of an instantiation of the hardware design under a second set of constraints;
• wherein the one or more combinations comprises a combination that is equivalent to the main algebraic expression.