Adaptive bug-search depth for simple and deep counterexamples

Patent metadata

Field	Value
Publication number	US-10210296-B2
Application number	US-201715791620-A
Country	US
Kind code	B2
Filing date	Oct 24, 2017
Priority date	Mar 21, 2017
Publication date	Feb 19, 2019
Grant date	Feb 19, 2019

Abstract

Aspects of the present invention include methods, systems and computer program products. The method includes a processor providing a netlist indicative of connectivity and functional states of components of an integrated circuit design; iteratively searching through the netlist at a selected depth to locate errors within the netlist by a plurality of trials, each of the plurality of trials having a plurality of iterations; adaptively adjusting the selected depth depending on any errors within the netlist being located, the selected depth increasing over time from an initial value as between the plurality of iterations; and adaptively adjusting an amount of coverage of the netlist depending on any errors within the netlist being located, the amount of coverage of the netlist decreasing over time from an initial amount as between the plurality of iterations.

First claim

What is claimed is:

1. A computer-implemented method of designing an integrated circuit comprising:
providing, by a processor, a netlist indicative of connectivity and functional states of components of an integrated circuit design;
iteratively searching, by the processor, through the netlist at a selected depth to locate errors within the netlist by a plurality of trials, each of the plurality of trials having a plurality of iterations, wherein iteratively searching, by the processor, through the netlist at a selected depth to locate errors within the netlist comprises performing a simulation process and a symbolic analysis process;
adaptively adjusting, by the processor, the selected depth depending on any errors within the netlist being located, the selected depth increasing over time from an initial value as between the plurality of iterations;
adaptively adjusting, by the processor, an amount of coverage of the netlist depending on any errors within the netlist being located, the amount of coverage of the netlist decreasing over time from an initial amount as between the plurality of iterations; and
manufacturing the integrated circuit design.

2. The computer-implemented method of claim 1 wherein the selected depth of the netlist comprises a number of simulation cycles by which iteratively searching by the processor is performed.

3. The computer-implemented method of claim 1 wherein an amount of coverage of the netlist is determined by at least one of analysis of the functional states of the components of the integrated circuit design and of analysis of secondary properties of the components of the integrated circuit design.

4. The computer-implemented method of claim 1 further comprising determining, by the processor, a depth of the netlist depending on a length of a trace associated with a gate component of the integrated circuit design, and shortening, by the processor, the length of the trace, wherein the trace comprises a sequence of valuations of the gate component of the integrated circuit design.

5. The computer-implemented method of claim 4 further comprising shortening, by the processor, the length of the trace starting from a first state of the gate component that is later in time than a second state of the gate component.

6. The computer-implemented method of claim 1 wherein the processor is located in a cloud computing environment, and wherein the method is implemented in software run by the processor located in the cloud computing environment.

Assignees

• IBM

Inventors

• Baumgartner Jason R
• Gajavelly Raj K
• Mony Hari
• Nalla Pradeep K

Classifications

• G06F30/3323 Primary

  using formal methods, e.g. equivalence checking or property checking · CPC title

• G06F2111/02

  CAD in a network environment, e.g. collaborative CAD or distributed simulation · CPC title

• G06F30/394

  Routing (G06F30/396 takes precedence) · CPC title

• G06F17/504 Primary

  Physics · mapped topic

• G06F17/5077

  Physics · mapped topic