Equivalence checking between two or more circuit designs that include square root circuits
AssigneeSynopsys, Inc.
InventorsHimanshu Jain, Carl P. Pixley
Life of this patent
Estimating the term…
Abstract
Methods and apparatuses are described for proving equivalence between two or more circuit designs that include one or more division circuits and/or one or more square-root circuits. Some embodiments analyze the circuit designs to determine an input relationship between the inputs of two division (or square-root) circuits. Next, the embodiments determine an output relationship between the outputs of two division (or square-root) circuits based on the input relationship. The embodiments then prove equivalence between the circuit designs by using the input and output relationships.
Claims14
In an electronic design automation (EDA) tool in a computer, a method for proving equivalence between a first circuit design and a second circuit design, wherein the first circuit design includes a first square-root circuit and the second circuit design includes a second square-root circuit, the method comprising:
- the EDA tool in the computer analyzing the first and second circuit designs to determine an input relationship between the square-root operand of the first square-root circuit and the square-root operand of the second square-root circuit, wherein the square-root operand of the first square-root circuit is not equal to the square-root operand of the second square-root circuit, and wherein the input relationship is of the form c=a·m2, where a is the square-root operand of the first square-root circuit, c is the square-root operand of the second square-root circuit, and m is an integer;
- the EDA tool in the computer determining an output relationship between a set of outputs of the first square-root circuit and a set of outputs of the second square-root circuit based on the input relationship;
- and
- the EDA tool in the computer proving equivalence between the first and second circuit designs by using the input and output relationships, wherein using the input and output relationships to prove equivalence improves performance of the EDA tool in the computer.
A non-transitory computer-readable storage medium storing instructions of an electronic design automation (EDA) tool that, when executed by a computer, cause the computer to perform a method for proving equivalence between a first circuit design and a second circuit design, wherein the first circuit design includes a first square-root circuit and the second circuit design includes a second square-root circuit, the method comprising:
- analyzing the first and second circuit designs to determine an input relationship between the square-root operand of the first square-root circuit and the square-root operand of the second square-root circuit, wherein the square-root operand of the first square-root circuit is not equal to the square-root operand of the second square-root circuit, and wherein the input relationship is of the form c=a·m2, where a is the square-root operand of the first square-root circuit, c is the square-root operand of the second square-root circuit, and m is an integer;
- determining an output relationship between a set of outputs of the first square-root circuit and a set of outputs of the second square-root circuit based on the input relationship;
- and
- proving equivalence between the first and second circuit designs by using the input and output relationships, wherein using the input and output relationship to prove equivalence improves performance of the EDA tool in the computer.
An apparatus, comprising:
- a processor;
- and
- a non-transitory computer-readable storage medium storing instructions for formal equivalence checking that, when executed by the processor, cause the processor to perform a method for proving equivalence between a first circuit design and a second circuit design, wherein the first circuit design includes a first square-root circuit and the second circuit design includes a second square-root circuit, the method comprising:
- proving correctness of the first and second square-root circuits;
- analyzing the first and second circuit designs to determine an input relationship between the square-root operand of the first square-root circuit and the square-root operand of the second square-root circuit, wherein the input relationship is of the form c=a·m2, where a is the square-root operand of the first square-root circuit, c is the square-root operand of the second square-root circuit, and m is an integer;
- determining an output relationship between a set of outputs of the first square-root circuit and a set of outputs of the second square-root circuit based on the input relationship;
- and
- proving equivalence between the first and second circuit designs by using the input and output relationships, wherein using the input and output relationship to prove equivalence improves performance of the EDA tool in the computer.
Dependencies are inferred from the claim text.