Methods, systems, and computer program product for verifying electronic designs with clock domain crossing paths

Patent metadata

Field	Value
Publication number	US-9633151-B1
Application number	US-201514675699-A
Country	US
Kind code	B1
Filing date	Mar 31, 2015
Priority date	Mar 31, 2015
Publication date	Apr 25, 2017
Grant date	Apr 25, 2017

Abstract

Various mechanisms and approaches identify a first electronic design component at least by traversing at least a portion of the electronic design and generate a representation of the electronic design by interconnecting one or more duplicated electronic design components within the representation. The first electronic design component may include a destination electronic design component with a backward traversal of the electronic design. One or more fan-in electronic design components may be duplicated into the one or more duplicated electronic design components. One or more CDC effect models are automatically injected into the representation by adding the one or more CDC effect models along one or more paths in the representation. Proof results are generated at least via proving or disproving one or more checkers for the electronic design by verifying or simulating the representation with the one or more CDC effect models that are automatically injected into the representation.

First claim

We claim:

1. A computer implemented method for verifying an electronic design with clock domain crossing paths, comprising:
executing a process with at least one micro-processor of a computing system, the process comprising:
identifying, at a clock domain crossing (CDC) identification module including or coupled with a design traversal module and at least one micro-processor of a computing system, a first electronic design component for verification of the electronic design at least by traversing at least a portion of the electronic design;
generating a representation of the electronic design at least by interconnecting one or more duplicated electronic design components, which are duplicated from one or more corresponding electronic design components in the electronic design, with the first electronic design component;
injecting one or more CDC effect models into the presentation at least by reducing a set of injection candidates into a reduced set of injection candidates with an application of one or more CDC rules and by adding the one or more CDC effect models along one or more paths associated with the reduced set of injection candidates in the representation of the electronic design; and
generating proof results at least via proving or disproving one or more checkers for the electronic design by verifying or simulating the representation with the one or more CDC effect models.

2. The computer implemented method of claim 1 , the process further comprising:
identifying a CDC path operatively coupled with the first electronic design component in the electronic design, wherein at least one CDC rule of the one or more CDC rules is used at least to identify a first electronic design component that is time-dependent and includes multiple inputs and to determine whether the multiple inputs of the first electronic design component correspond to different clock domains.

3. The computer implemented method of claim 1 , the process further comprising:
identifying a destination electronic design component as the first electronic design component associated with a CDC path that connects two or more clock domains.

4. The computer implemented method of claim 3 , the process further comprising:
identifying one or more fan-in electronic design components for the first electronic design component, wherein the design traversal module backward traverses at least a portion of the electronic design.

5. The computer implemented method of claim 4 , the process further comprising:
duplicating the one or more electronic design components into the one or more duplicated electronic design components in the representation of the electronic design; and
interconnecting the one or more duplicated electronic design components in the representation by using at least connectivity information of the electronic design.

6. The computer implemented method of claim 1 , wherein the representation of the electronic design includes an in-memory representation of the electronic design, and the one or more duplicated electronic design components are interconnected in the in-memory representation of the electronic design by using at least connectivity information of the electronic design.

7. The computer implemented method of claim 1 , determining the representation of the electronic design further comprising:
removing a path in the representation of the electronic design; and
creating at least one additional path by interconnecting the first electronic design component with at least one duplicated electronic design component of the one or more electronic design components.

8. The computer implemented method of claim 1 , the process further comprising:
identifying the one or more CDC rules for the electronic design; and
determining one or more locations for the one or more CDC effect models in the representation of the electronic design based in part or in whole upon the one or more CDC rules.

9. The computer implemented method of claim 8 , the one or more CDC rules including:
identifying a first time-dependent electronic design component having multiple inputs;
determining whether the multiple inputs belong to different clock domains; and
injecting a first CDC effect model at an output of the time-dependent electronic design component, where the multiple inputs of the time-dependent electronic design component are determined to belong to the different clock domains.

10. The computer implemented method of claim 8 , the one or more CDC rules including:
identifying a second time-dependent electronic design component having an output propagated to multiple electronic design components;
determining whether the multiple electronic design components belong to a same clock domain; and
injecting a second CDC effect model at outputs of the multiple electronic design components, where the multiple electronic design components are determined to belong to the same clock domain.

11. The computer implemented method of claim 1 , the process further comprising:
performing an iterative process, the iterative process comprising:
determining a property corresponding to at least one checker of the one or more checkers;
modifying the electronic design, the at least one checker, or the property by making one or more changes based in part or in whole upon the proof results for the at least one checker;
proving or disproving the at least one checker with the one or more changes; and
committing the one or more changes into a persistent storage device.

12. An article of manufacture comprising a non-transitory computer accessible storage medium having stored thereupon a sequence of instructions which, when executed by at least one processor, causes the at least one processor to perform a set of acts for verifying an electronic design with clock domain crossing paths, the set of acts comprising:
executing a process with at least one micro-processor of a computing system, the process comprising:
identifying, with an aid of a clock domain crossing (CDC) identification module coupled with at least one micro-processor of a computing system and a design traversal module, a first electronic design component at least by traversing at least a portion of the electronic design;
generating a representation of the electronic design at least by interconnecting one or more duplicated electronic design components, which are duplicated from one or more corresponding electronic design components in the electronic design, with the first electronic design component;
injecting one or more CDC effect models into the representation at least by reducing a set of injection candidates into a reduced set of injection candidates with an application of one or more CDC rules and by adding the one or more CDC effect models along one or more paths associated with the reduced set of injection candidates in the representation of the electronic design; and
generating proof results at least by proving one or more checkers for the electronic design by verifying or simulating the representation with the one or more CDC effect models.

13. The article of manufacture of claim 12 , further comprising the sequence of instructions which, when executed by at least one processor, causes the at least one processor to perform the process that further comprises:
identifying a CDC path operatively coupled with the first electronic design component in the electronic design.

14. The article of manufacture of claim 12 , further comprising the sequence of instructions which, when executed by at least one processor, causes the at least one processor to perform the process that further comprises:
identifying a desti

Assignees

• Cadence Design Systems Inc

Inventors

• Sun Xiaoyang
• Gomes Marcus Vinicius Da Mata
• Tavares Andrea Iabrudi
• Loh Lawrence
• Peixoto Fabiano

Classifications

• G06F30/3312 Primary

  Timing analysis · CPC title

• G06F30/396

  Clock trees · CPC title

• G06F17/504 Primary

  Physics · mapped topic

• G06F30/3308 Primary

  using simulation · CPC title

• G06F30/3323

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