US 2020/0026813 A1Published application

Providing guidance to an equivalence checker when a design contains retimed registers

AssigneeSynopsys, Inc.

InventorsMuzaffer Hiraoglu, Darren Charles Cronquist, Peter Wilhelm Joseph Zepter, Navneet Kakkar, Sridhar Keladi

Life of this patent

Estimating the term…

Loading patent…

Abstract

Systems and techniques are described for providing guidance to an equivalence checker when a design contains retimed registers. Some embodiments can perform at least a register retiming optimization on a first design to obtain a second design. Next, the embodiments can determine one or more codes to provide guidance for connecting the set/clear inputs of the retimed registers. The first design, the second design, and the one or more codes can then be provided to an equivalence checker, wherein providing the one or more codes to the equivalence checker reduces an amount of computation required by the equivalence checker to determine functional equivalence between the first design and the second design.

Claims15

Dependent claims

A non-transitory computer-readable storage medium storing instructions that, when executed by a computer, cause the computer to perform a method for providing guidance to an equivalence checker, the method comprising:

performing at least a register retiming optimization on a first design to obtain a second design;
defining a register in the first design to be a representative register;
for at least one retimed register in a set of retimed registers in the second design,
determining a first code that corresponds to a first logical relationship between (1) the retimed register's asynchronous set input and asynchronous clear input, and (2) the representative register's asynchronous set input and asynchronous clear input, and
determining a second code that corresponds to a second logical relationship between (1) the retimed register's synchronous set input and synchronous clear input, and (2) the representative register's synchronous set input and synchronous clear input;
and
providing the first design, the second design, the first code, and the second code to the equivalence checker, wherein providing the first and second codes to the equivalence checker reduces an amount of computation required by the equivalence checker to determine functional equivalence between the first design and the second design.

4 more elements

An apparatus, comprising:

a processor;
and
a memory storing instructions that, when executed by the processor, cause the processor to perform a method for providing guidance to an equivalence checker, the method comprising:
performing at least a register retiming optimization on a first design to obtain a second design;
defining a register in the first design to be a representative register;
for at least one retimed register in a set of retimed registers in the second design,
determining a first code that corresponds to a first logical relationship between (1) the retimed register's asynchronous set input and asynchronous clear input, and (2) the representative register's asynchronous set input and asynchronous clear input, and
determining a second code that corresponds to a second logical relationship between (1) the retimed register's synchronous set input and synchronous clear input, and (2) the representative register's synchronous set input and synchronous clear input;
and
providing the first design, the second design, the first code, and the second code to the equivalence checker, wherein providing the first and second codes to the equivalence checker reduces an amount of computation required by the equivalence checker to determine functional equivalence between the first design and the second design.

7 more elements

A method for providing guidance to an equivalence checker, the method comprising:

performing at least a register retiming optimization on a first design to obtain a second design;
defining a register in the first design to be a representative register;
for at least one retimed register in a set of retimed registers in the second design,
determining a first code that corresponds to a first logical relationship between (1) the retimed register's asynchronous set input and asynchronous clear input, and (2) the representative register's asynchronous set input and asynchronous clear input, and
determining a second code that corresponds to a second logical relationship between (1) the retimed register's synchronous set input and synchronous clear input, and (2) the representative register's synchronous set input and synchronous clear input;
and
providing the first design, the second design, the first code, and the second code to the equivalence checker, wherein providing the first and second codes to the equivalence checker reduces an amount of computation required by the equivalence checker to determine functional equivalence between the first design and the second design.

4 more elements

Dependencies are inferred from the claim text.

Facts

Application: 16/037,936Filed 17 Jul 2018
Published: 23 Jan 2020
Term ends: Not estimatedThe source records don’t support an estimate.

Classification6 codes

G06F 30/3323
Design verification, e.g. functional simulation or model checking: using formal methods, e.g. equivalence checking or property checking
G06F 30/35
Circuit design: delay-insensitive circuit design, e.g. asynchronous or self-timed
G06F 30/327
Circuit design at the digital level: logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist
G06F 30/3312
Using simulation: timing analysis