System, method, and computer program product for analyzing X-propagation failures in formal verification

Patent metadata

Field	Value
Publication number	US-10031990-B1
Application number	US-201615278441-A
Country	US
Kind code	B1
Filing date	Sep 28, 2016
Priority date	Sep 28, 2016
Publication date	Jul 24, 2018
Grant date	Jul 24, 2018

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 at a verification environment and generating a symbolic constant for use with the verification environment. The method may further include identifying a plurality of X sources associated with the verification environment and modifying the plurality of X sources based upon, at least in part, the symbolic constant. The method may also include running a first target node and if the first target node is proven, run at least one additional target node until all target nodes are proven.

First claim

What is claimed is:

1. A computer-implemented method for electronic design verification comprising:
receiving, using a processor, an electronic design at a verification environment;
generating a symbolic constant for use with the electronic design and the verification environment, wherein the symbolic constant is assigned an arbitrary value for use throughout a verification process;
identifying a plurality of X sources associated with the electronic design and the verification environment;
modifying the plurality of X sources based upon, at least in part, the symbolic constant;
running a first target node associated with the electronic design and the verification environment;
if the first target node is proven, running at least one additional target node until all target nodes are proven;
if the first target node is a failure, fetching a symbolic constant value from a counter-example; and
generating an integrated circuit after all target nodes are proven.

2. The computer-implemented method of claim 1 , further comprising:
providing a path from a selected X source to the target node; and
running a second target node.

3. The computer-implemented method of claim 1 , further comprising:
inserting at least one extra circuitry component to the verification environment.

4. The computer-implemented method of claim 3 , wherein the at least one extra circuitry component is configured to enable all X sources and to maintain a singular X source active non-deterministically.

5. The computer-implemented method of claim 3 , wherein the at least one extra circuitry component is a multiplexer.

6. A 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 at a verification environment;
generating a symbolic constant for use with the verification environment, wherein the symbolic constant is assigned an arbitrary value for use throughout a verification process;
identifying a plurality of X sources associated with the verification environment;
modifying the plurality of X sources based upon, at least in part, the symbolic constant;
running a first target node;
if the first target node is proven, running at least one additional target node until all target nodes are proven;
if the first target node is a failure, fetching a symbolic constant value from a counter-example; and
generating an integrated circuit after all target nodes are proven.

7. The computer-readable storage medium of claim 6 further comprising:
providing a path from a selected X source to the target node; and
running a second target node.

8. The computer-readable storage medium of claim 6 , further comprising:
inserting at least one extra circuitry component to the verification environment.

9. The computer-readable storage medium of claim 8 , wherein the at least one extra circuitry component is configured to enable all X sources and to maintain a singular X source active non-deterministically.

10. The computer-readable storage medium of claim 8 , wherein the at least one extra circuitry component is a multiplexer.

11. A system for electronic design verification comprising:
a computing device having at least one processor configured to receive an electronic design at a verification environment and to generate a symbolic constant for use with the verification environment, wherein the symbolic constant is assigned an arbitrary value for use throughout a verification process, the at least one processor is further configured to identify a plurality of X sources associated with the verification environment, the at least one processor is further configured to modify the plurality of X sources based upon, at least in part, the symbolic constant, the at least one processor is further configured to run a first target node and if the first target node is proven, run at least one additional target node until all target nodes are proven if the first target node is a failure, the at least one processor is further configured to fetch a symbolic constant value from a counter-example, generating an integrated circuit after all target nodes are proven.

12. The system of claim 11 , wherein the at least one processor is further configured to provide a path from a selected X source to the target node and run a second target node.

13. The system of claim 11 , wherein the at least one processor is further configured to insert at least one extra circuitry component to the verification environment.

14. The system of claim 11 , wherein the at least one extra circuitry component is configured to enable all X sources and to maintain a singular X source active non-deterministically.

Assignees

• Cadence Design Systems Inc

Inventors

• Goyal Pradeep
• Yadav Deepak
• Narula Jasmeet Singh

Classifications

• G06F30/3323 Primary

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

• G06F17/504 Primary

  Physics · mapped topic