Method for waveform based debugging for cover failures from formal verification

Patent metadata

Field	Value
Publication number	US-10380301-B1
Application number	US-201715462068-A
Country	US
Kind code	B1
Filing date	Mar 17, 2017
Priority date	Mar 17, 2017
Publication date	Aug 13, 2019
Grant date	Aug 13, 2019

Abstract

The present disclosure relates to a method for waveform based debugging in a formal verification of an integrated circuit. The method may include receiving, using at least one processor, an electronic circuit design and partitioning a cone of influence for a cover property of the electronic circuit design into design logic and property logic. The method may further include applying an X-value to all inputs associated with the cone of influence and performing an X-simulation until a fixed point is reached. The method may also include identifying a non-X node and providing a path of X-diffusion at a property output.

First claim

What is claimed is:

1. A computer-implemented method for waveform based debugging in a formal verification of an integrated circuit comprising:
receiving, using at least one processor, an electronic circuit design;
partitioning a cone of influence for a cover property of the electronic circuit design into design logic that is driving the cover property and property logic corresponding to an expression of the cover property;
applying an X-value to all inputs associated with the cone of influence;
performing an X-simulation until a fixed point is reached;
identifying a non-X node; and
providing a path of X-diffusion at a property output.

2. The computer-implemented method of claim 1 , wherein identifying the non-X node includes marking the non-X node.

3. The computer-implemented method of claim 1 , wherein applying the X-value includes applying a zero value and a one value simultaneously.

4. The computer-implemented method of claim 1 , wherein the fixed point is based upon, at least in part, no change in the X-value of all inputs.

5. The computer-implemented method of claim 1 , further comprising:
identifying the X-value converted to a Boolean value prior to reaching the fixed point.

6. The computer-implemented method of claim 1 , wherein providing includes displaying at least a portion of the path at a waveform viewer.

7. The computer-implemented method of claim 6 wherein the waveform viewer displays a debug trace for a cover failure.

8. A computer-readable storage medium having stored thereon instructions, which when executed by a processor result in the following operations:
receiving, using at least one processor, an electronic circuit design;
partitioning a cone of influence for a cover property of the electronic circuit design into design logic that is driving the cover property and property logic corresponding to an expression of the cover property;
applying an X-value to all inputs associated with the cone of influence;
performing an X-simulation until a fixed point is reached;
identifying a non-X node; and
providing a path of X-diffusion at a property output.

9. The computer-readable storage medium of claim 8 , wherein identifying the non-X node includes marking the non-X node.

10. The computer-readable storage medium of claim 8 , wherein applying the X-value includes applying a zero value and a one value simultaneously.

11. The computer-readable storage medium of claim 8 , wherein the fixed point is based upon, at least in part, no change in the X-value of all inputs.

12. The computer-readable storage medium of claim 8 , further comprising:
identifying the X-value converted to a Boolean value prior to reaching the fixed point.

13. The computer-readable storage medium of claim 8 , wherein providing includes displaying at least a portion of the path at a waveform viewer.

14. The computer-readable storage medium of claim 13 , wherein the waveform viewer displays a debug trace for a cover failure.

15. A computing system for debugging in a formal verification of an integrated circuit comprising:
at least one processor configured to receive an electronic circuit design and to partition a cone of influence for a cover property of the electronic circuit design into design logic that is driving the cover property and property logic corresponding to an expression of the cover property,
the at least one processor further configured to apply an X-value to all inputs associated with the cone of influence and to perform an X-simulation until a fixed point is reached,
the at least one processor further configured to identify a non-X node and to provide a path of X-diffusion at a property output.

16. The computing system of claim 15 , wherein identifying the non-X node includes marking the non-X node.

17. The computing system of claim 15 , wherein applying the X-value includes applying a zero value and a one value simultaneously.

18. The computing system of claim 15 , wherein the fixed point is based upon, at least in part, no change in the X-value of all inputs.

19. The computing system of claim 15 , further comprising:
identifying the X-value converted to a Boolean value prior to reaching the fixed point.

20. The computing system of claim 15 , wherein providing includes displaying at least a portion of the path at a waveform viewer.

Assignees

• Cadence Design Systems Inc

Inventors

• Goyal Pradeep
• Sharma Mudit

Classifications

• G06F30/3323 Primary

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

• G06F30/30 Primary

  Circuit design · CPC title

• G06F17/5045 Primary

  Physics · mapped topic