System, method, and computer program product for oscillating loop detection in formal verification

Patent metadata

Field	Value
Publication number	US-10176286-B1
Application number	US-201715462161-A
Country	US
Kind code	B1
Filing date	Mar 17, 2017
Priority date	Mar 17, 2017
Publication date	Jan 8, 2019
Grant date	Jan 8, 2019

Abstract

The present disclosure relates to a computer-implemented method for electronic design verification. The method may include receiving, using a processor, an electronic design having a plurality of loops and removing a section of each of the plurality of loops. The method may further include obtaining an input/output net for each of the plurality of loops and generating a copy of at least a portion of the electronic design. The method may include connecting all inputs except a loop cut input net associated with the removed section and analyzing a loop output net using formal verification.

First claim

What is claimed is:

1. A computer-implemented method for electronic design verification comprising:
receiving, using a processor, an electronic design having a plurality of loops;
removing a section of each of the plurality of loops;
obtaining an input/output net for each of the plurality of loops;
generating a copy of at least a portion of the electronic design;
connecting all inputs except a loop cut input net associated with the removed section; and
analyzing a loop output net using formal verification.

2. The computer-implemented method of claim 1 , wherein generating the copy includes generating two copies.

3. The computer-implemented method of claim 1 , wherein analyzing is based upon, at least in part, a miter.

4. The computer-implemented method of claim 1 , wherein if analyzing is successful an oscillating loop is detected.

5. The computer-implemented method of claim 1 , wherein if analyzing is unsuccessful a false loop or stable loop is detected.

6. The computer-implemented method of claim 3 , wherein analyzing includes checking for a miter value.

7. The computer-implemented method of claim 1 , further comprising:
inverting an I/O value set in the copy, based upon, at least in part, an I/O value set in an original loop.

8. A non-transitory computer-readable storage medium for electronic design verification, the computer-readable storage medium having stored thereon instructions that when executed by a machine result in one or more operations, the operations comprising:
receiving, using a processor, an electronic design having a plurality of loops;
removing a section of each of the plurality of loops;
obtaining an input/output net for each of the plurality of loops;
generating a copy of at least a portion of the electronic design;
connecting all inputs except a loop cut input net associated with the removed section; and
analyzing a loop output net using formal verification.

9. The computer-readable storage medium of claim 8 , wherein generating the copy includes generating two copies.

10. The computer-readable storage medium of claim 8 , wherein analyzing is based upon, at least in part, a miter.

11. The computer-readable storage medium of claim 8 , wherein if analyzing is successful an oscillating loop is detected.

12. The computer-readable storage medium of claim 8 , wherein if analyzing is unsuccessful a false loop or stable loop is detected.

13. The computer-readable storage medium of claim 10 , wherein analyzing includes checking for a miter value.

14. The computer-readable storage medium of claim 8 , further comprising:
inverting an I/O value set in the copy, based upon, at least in part, an I/O value set in an original loop.

15. A system for electronic design verification comprising:
a computing device having at least one processor configured to receive an electronic design having a plurality of loops and to remove a section of each of the plurality of loops, the at least one processor further configured to obtain an input/output net for each of the plurality of loops and to generate a copy of at least a portion of the electronic design, the at least one processor further configured to connect all inputs except a loop cut input net associated with the removed section and to analyze a loop output net using formal verification.

16. The system of claim 15 , wherein generating the copy includes generating two copies.

17. The system of claim 15 , wherein analyzing is based upon, at least in part, a miter.

18. The system of claim 15 , wherein if analyzing is successful an oscillating loop is detected.

19. The system of claim 15 , wherein if analyzing is unsuccessful a false loop or stable loop is detected.

20. The system of claim 17 , wherein analyzing includes checking for a miter value.

Assignees

• Cadence Design Systems Inc

Inventors

• Goyal Pradeep
• Kumar Ravindra

Classifications

• G06F30/3323 Primary

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

• G06F17/504 Primary

  Physics · mapped topic