# US 10,769,008 B1 · Systems and methods for automatic formal metastability fault analysis in an electronic design

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 10,769,008 B1
- Document ID: US10769008B1
- Status: Granted
- Kind: B1
- Application number: 15/370,565
- Filed: 2016-12-06
- Granted: 2020-09-08
- Earliest claimed: 2016-12-06
- Assignees: Cadence Design Systems, Inc.
- Applicants: Cadence Design Systems, Inc.
- Inventors: Alberto Manuel Arias Drake; Andrea Iabrudi Tavares; Artur Melo Mota Costa; Fabiano Cruz Peixoto; Laiz Lipiainen Santos; Lucas Ferreira de Melo Diniz; Nathália Peixoto Reis; Patricia Sette Câmara Haizer; Regina Mara Amaral Fonseca; Tamires Vargas Capanema Franco Santos
- Web page: https://patentgrep.com/patent/US10769008B1

## CPC

- G06F 11/079: {Root cause analysis, i.e. error or fault diagnosis (in a hardware test environment G06F11/22; in a software test environment G06F11/36)}
- G06F 30/3323: using formal methods, e.g. equivalence checking or property checking
- G06F 11/0724: {in a multiprocessor or a multi-core unit (multiprocessors per se G06F15/80)}
- G06F 2119/02: Reliability analysis or reliability optimisation; Failure analysis, e.g. worst case scenario performance, failure mode and effects analysis [FMEA]
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## Abstract

The present disclosure relates to a computer-implemented method for use in an electronic design. The method may include receiving, using at least one processor, an electronic design and analyzing the electronic design. The method may further include generating one or more preconditions representative of metastability effects at the output of at least one synchronizer associated with the electronic design. The method may also include generating, based upon, at least in part, the one or more preconditions, one or more properties configured to analyze a propagation of the metastability effects associated with the at least one synchronizer.

## Claims

### Claim 1

A computer-implemented method for use in a formal verification of an electronic design comprising:
receiving, using at least one processor, a clock-domain crossing electronic design;
analyzing the electronic design;
automatically generating a set of nodes where metastability can be originated;
automatically generating one or more preconditions representative of metastability effects at the output of at least one synchronizer associated with the electronic design;
automatically generating, based upon, at least in part, the one or more preconditions, one or more properties configured to analyze a propagation of the metastability effects associated with the at least one synchronizer; and
visually displaying at least one of the metastability effects and one or more unaffected areas at an annotated graph configured to display the at least one synchronizer and at least one clock domain.

### Claim 2 (depends on 1)

The computer-implemented method of claim 1, wherein analyzing the propagation of the metastability effects includes analyzing a fan-out cone associated with the at least one synchronizer.

### Claim 3 (depends on 1)

The computer-implemented method of claim 1, wherein the annotated graph is configured to display at least one of an area unaffected by a metastability issue, a node reached by metastability effects, and a metastability convergence point.

### Claim 4 (depends on 1)

The computer-implemented method of claim 1, wherein the annotated graph is configured to display at least one node and wherein the at least one node corresponds to a flip-flop, an input port, or an output port.

### Claim 5

A non-transitory computer-readable storage medium having stored thereon instructions that when executed by a machine result in the following operations for use in a formal verification of an electronic design:
receiving, using at least one processor, a clock-domain crossing electronic design;
analyzing the electronic design;
automatically generating a set of nodes where metastability can be originated;
automatically generating one or more preconditions representative of metastability effects at the output of at least one synchronizer associated with the electronic design;
automatically generating, based upon, at least in part, the one or more preconditions, one or more properties configured to analyze a propagation of the metastability effects associated with the at least one synchronizer; and
visually displaying at least one of the metastability effects and one or more unaffected areas at an annotated graph configured to display the at least one synchronizer and at least one clock domain, wherein the annotated graph displays a node unaffected by metastability in a first manner and a node affected by metastability in a second manner distinct from the first manner.

### Claim 6 (depends on 5)

The computer-readable storage medium of claim 5, wherein analyzing the propagation of the metastability effects includes analyzing a fan-out cone associated with the at least one synchronizer.

### Claim 7 (depends on 5)

The computer-readable storage medium of claim 5, wherein the annotated graph is configured to display at least one of an area unaffected by a metastability issue, a node reached by metastability effects, and a metastability convergence point.

### Claim 8 (depends on 5)

The computer-readable storage medium of claim 5, wherein the annotated graph is configured to display at least one node and wherein the at least one node corresponds to a flip-flop, an input port, or an output port.

### Claim 9

A system for a formal verification of an electronic design comprising:
a computing device configured to receive, using at least one processor, a clock-domain crossing electronic design, the at least one processor further configured to analyze the electronic design and automatically generate a set of nodes where metastability can be originated, the at least one processor further configured to automatically generate one or more preconditions representative of metastability effects at the output of at least one synchronizer associated with the electronic design, the at least one processor further configured to automatically generate, based upon, at least in part, the one or more preconditions, one or more properties configured to analyze a propagation of the metastability effects associated with the at least one synchronizer, wherein analyzing the propagation of the metastability effects includes analyzing a fan-out cone associated with the at least one synchronizer, the at least one processor further configured to visually display the metastability effects and one or more unaffected areas at an annotated graph configured to display the at least one synchronizer and at least one clock domain.

### Claim 10 (depends on 9)

The system of claim 9, wherein analyzing the propagation of the metastability effects includes analyzing a fan-out cone associated with the at least one synchronizer.

### Claim 11 (depends on 9)

The system of claim 9, wherein the annotated graph is configured to display at least one of an area unaffected by a metastability issue, a node reached by metastability effects, and a metastability convergence point.

### Claim 12 (depends on 9)

The system of claim 9, wherein the annotated graph is configured to display at least one node and wherein the at least one node corresponds to a flip-flop, an input port, or an output port.