Hardware validation through binary decision diagrams including functions and equalities

A computer program product in a computer-readable medium for validating a hardware design, comprising functional descriptive material that when executed by a computer, enables the computer to perform acts including:

• applying one of a plurality of transformation rules to simplify a binary decision diagram containing function symbols and variables which represent a hardware design to be validated;
• repeating the application of the plurality of transformation rules to the binary decision diagram until no more of the plurality of transformation rules may be applied to the binary decision diagram;
• and
• in response to no more of the plurality of the transformation rules being applicable to the binary decision diagram, determining whether the binary decision diagram has been reduced to a single true value.

A data processing system for validating a hardware design, comprising:

• a processing unit including at least on processor;
• memory;
• and
• a set of instructions in the memory,
• wherein the processing unit executes the set of instructions to perform acts including:
• applying one of a plurality of transformation rules to simplify a binary decision diagram containing function symbols and variables which represent a hardware design to be validated;
• repeating the application of the plurality of transformation rules to the binary decision diagram until no more of the plurality of transformation rules may be applied to the binary decision diagram;
• and
• in response to no more of the plurality of the transformation rules being applicable to the binary decision diagram, determining whether the binary decision diagram has been reduced to a single true value.