Method and apparatus for performing formal verification of polynomial datapath

An apparatus for synthesising an integrated circuit design comprising:

• a receiver for receiving a plurality of equivalent designs for synthesis in RTL;
• a data flow graph derivation unit configured for deriving a data flow graph representation of each design, each data flow graph representation having at least one input with an input bit width, at least one internal signal with an internal bit width, and at least one output with an output bit width;
• a data flow graph modification unit configured for deriving first modified versions of each data flow graph representation by restricting bit width for each said at least one internal signal to be equal to a largest output bit width of all the outputs, when said at least one internal signal is polynomial;
• a comparator configured for comparing each first modified design against the respective design from which it was derived to determine whether it is equivalent to the respective design for which it was derived;
• an input bit width restricting unit configured to restrict the bit widths of said at least one input to derive second modified versions of each respective first modified version of a design determined to be functionally equivalent to the design for which it was derived;
• a second comparator configured for comparing said second modified designs against each other to determine which second modified designs are functionally equivalent;
• and
• an output configured for providing any designs determined to be functionally equivalent to an RTL synthesis unit.

A non-transitory computer readable storage medium storing instructions which when executed by a computer causes the computer to perform a method for use in synthesis of an integrated circuit design, the method comprising:

• receiving a plurality of designs for synthesis in RTL;
• determining a data flow graph representation of each design, each data flow graph representation having at least one input with an input bit width, at least one internal signal with an internal bit width, and at a least one output with an output bit width;
• deriving first modified versions of each data flow graph representation by restricting bit width for each said at least one internal signal to be equal to a largest output bit width of all the outputs, when said at least one internal signal is polynomial;
• comparing each first modified design against the respective design from which it was derived to determine whether it is equivalent to the respective design from which it was derived;
• restricting the input bit widths of said at least one input to derive second modified versions of each respective first modified version of a design determined to be functionally equivalent to the design from which it was derived;
• comparing said second modified designs against each other to determine which second modified designs are functionally equivalent;
• and
• providing any one or more of the designs determined to be functionally equivalent to an RTL synthesis unit.