Selective Annotation Of Circuits For Efficient Formal Verification With Low Power Design Considerations

Patent metadata

Field	Value
Publication number	US-2016154902-A1
Application number	US-201514596500-A
Country	US
Kind code	A1
Filing date	Jan 14, 2015
Priority date	Nov 30, 2014
Publication date	Jun 2, 2016
Grant date	—

Abstract

Formal verification of a circuit design is performed with low power considerations. The formal verification process receives a circuit design and a low power design specification. The low power design specification identifies power domains for the circuit. The system models undefined signal reaching nodes of the circuit from components of power domains that are switched off. The system selects a subset of nodes at which undefined signal reaches, thereby excluding certain nodes from the analysis. The selection of a small subset of nodes for analyzing undefined signals increases the efficiency of the formal verification process. The system annotates the circuit design to allow undefined signals to be introduced at the selected nodes. The system performs formal verification of the annotated circuit design.

First claim

What is claimed is:

1 . A computer-implemented method for performing formal verification of a circuit in view of low power design specification, the method comprising:
receiving a request to perform formal verification of an input circuit; receiving low power design specification for the input circuit, the low power design specification identifying power domains, each power domain associated with one or more components of the input circuit, the input circuit comprising a set of corrupted nodes, each corrupted node receiving an undefined signal from a component of a power domain that is switched off; selecting a subset of the set of corrupted nodes for injecting undefined signals at the selected corrupted nodes for performing formal verification; annotating the circuit design to be able to provide an undefined signal at each of the subset of corrupted nodes; performing formal verification of the annotated circuit design.

2 . The computer-implemented method of claim 1 , wherein annotating the circuit design to provide an undefined signal at a corrupted node comprises adding one or more components to the circuit design to allow the signal of the corrupted node to be set based on an input representing the undefined signal.

3 . The computer-implemented method of claim 1 , wherein selecting the subset of corrupted nodes comprises:
determining if a node is associated with a boundary of the power domain; and including the node in the subset of corrupted nodes if the node is associated with a boundary of the power domain.

4 . The computer-implemented method of claim 3 , wherein a node is determined to be associated with the boundary of the power domain if the node is connected to a first component belonging to the power domain and a second component outside the power domain.

5 . The computer-implemented method of claim 4 , wherein the node connects an output of the first component belonging to the power domain with an input of the second component outside the power domain.

6 . The computer-implemented method of claim 4 , wherein the node connects an output of the second component outside the power domain with an input of the first component belonging to the power domain.

7 . The computer-implemented method of claim 1 , wherein selecting the subset of corrupted nodes comprises:
determining if a node is an internal node of the power domain, wherein an internal node connects a plurality of combinational components, each of the plurality of combinational components belonging to the power domain; and determining that the node is not included in the subset of corrupted nodes if the node is determined to be an internal node of the power domain.

8 . The computer-implemented method of claim 1 , wherein identifying the set of nodes comprises:
determining if a node is connected to an output of a sequential element belonging to the power domain; and including the node in the subset of corrupted nodes if the node is determined to be the output of the sequential element belonging to the power domain.

9 . The computer-implemented method of claim 1 , wherein identifying the subset of corrupted nodes comprises:
determining if a node connects a first component powered by a first power supply with a second component powered by a second power supply; and including the node in the subset of corrupted nodes based on the determination that the first power supply is distinct from the second power supply.

10 . The computer-implemented method of claim 9 , further comprising:
determining if the first power supply is equivalent to the second power supply based on the low power design specification; and wherein the node is included in the subset of corrupted nodes if the first power supply is determined to be not equivalent to the second power supply.

11 . The computer-implemented method of claim 1 , wherein selecting the subset of corrupted nodes comprises:
determining not to include a node in the subset of corrupted nodes if the node connects a first component powered by a first power supply with a second component powered by a second power supply and the first power supply is equivalent to the second power supply based on the low power design specification.

12 . The computer-implemented method of claim 1 , wherein selecting the subset of corrupted nodes comprises:
determining not to include a node in the subset of corrupted nodes if the node is connected to an output of a sequential element of the power domain wherein a power supply controller resets the state of the sequential element if the power domain switches from an off state to an on state.

13 . The computer-implemented method of claim 1 , wherein selecting the subset of corrupted nodes comprises:
identifying a node connected to an output of a sequential element of the power domain; determining if a power supply controller resets state of the sequential element when the power domain switches from off state to on state; and including the node in the subset of corrupted nodes if the power supply controller is determined not to reset the state of the sequential element when the power domain switches from off state to on state.

14 . A non-transitory computer readable storage medium storing instructions for:
receiving a request to perform formal verification of an input circuit; receiving low power design specification for the input circuit, the low power design specification identifying power domains, each power domain associated with one or more components of the input circuit, the input circuit comprising a set of corrupted nodes, each corrupted node receiving an undefined signal from a component of a power domain that is switched off; selecting a subset of the set of corrupted nodes for injecting undefined signals at the selected corrupted nodes for performing formal verification; annotating the circuit design to be able to provide an undefined signal at each of the subset of corrupted nodes; performing formal verification of the annotated circuit design.

15 . The non-transitory computer readable storage medium of claim 14 , wherein annotating the circuit design to provide an undefined signal at a corrupted node comprises adding one or more components to the circuit design to allow the signal of the corrupted node to be set based on an input representing the undefined signal.

16 . The non-transitory computer readable storage medium of claim 14 , wherein selecting the subset of corrupted nodes comprises:
determining if a node is associated with a boundary of the power domain; and including the node in the subset of corrupted nodes if the node is associated with a boundary of the power domain.

17 . The non-transitory computer readable storage medium of claim 14 , wherein selecting the subset of corrupted nodes comprises:
determining if a node is an internal node of the power domain, wherein an internal node connects a plurality of combinational components, each of the plurality of combinational components belonging to the power domain; and determining that the node is not included in the subset of corrupted nodes if the node is determined to be an internal node of the power domain.

18 . The non-transitory computer readable storage medium of claim 14 , wherein identifying the set of nodes comprises:
determining if a node is connected to an output of a sequential element belonging to the power domain; and including the node in the subset of corrupted nodes if the node is determined to be the output of the sequential element belonging to the power domain.

Assignees

• Synopsys Inc

Inventors

• Korthikanti Vijay Anand
• Tiwari Praveen

Classifications

• G06F30/3323 Primary

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

• G06F30/30

  Circuit design · CPC title

• G06F17/504 Primary

  Physics · mapped topic

• G06F17/5045

  Physics · mapped topic

• G06F2119/06

  Power analysis or power optimisation · CPC title