公开(公告)号：US10380312B1

公开(公告)日：2019-08-13

申请号：US15371449

申请日：2016-12-07

Applicant: Cadence Design Systems, Inc.

Inventor： Craig Franklin Deaton ,  Lars Lundgren

IPC: G06F17/50

Abstract: The present disclosure relates to a method for electronic design verification. Embodiments may include receiving, using at least one processor, an electronic design and identifying one or more assumptions associated with the electronic design that are mutually in conflict. Embodiments may further include grouping the one or more assumptions that are mutually in conflict into a conflicting group of assumptions and iteratively disabling at least one of the conflicting group of assumptions. Embodiments may include generating at least one trace pair depicting a scenario where an assumption from a disabled set holds in a first trace but is violated in a second trace. Embodiments may further include identifying at least one signal associated with the first trace and at least one signal associated with the second trace and comparing the at least one signal associated with the first trace and the at least one signal associated with the second trace.

公开(公告)号：US11580284B1

公开(公告)日：2023-02-14

申请号：US17142360

申请日：2021-01-06

Applicant: Cadence Design Systems, Inc.

Inventor： Craig Franklin Deaton ,  Christopher William Komar ,  Lars Lundgren

IPC: G06F30/30 ,  G06F30/33 ,  G06F30/31 ,  G06F111/04 ,  G06Q10/10

Abstract: The present disclosure relates to a method for electronic circuit design. Embodiments may include receiving, using a processor, an electronic circuit design and performing a deadlock check on the electronic circuit design using a using a linear temporal logic property and a proof engine. Embodiments may further include analyzing a counterexample associated with the electronic circuit design for a loop escape condition, wherein analyzing includes proving a cover trace of a liveness obligation. If the loop escape condition is reachable from the counterexample, embodiments may include extracting one or more events associated with the loop escape condition and adding a waiver constraint to the deadlock check to force a no deadlock outcome.

公开(公告)号：US11520964B1

公开(公告)日：2022-12-06

申请号：US17336315

申请日：2021-06-02

Applicant: Cadence Design Systems, Inc.

Inventor： Ahmad S. Abo Foul ,  Lars Lundgren ,  Björn Håkan Hjort ,  Habeeb Farah ,  Eran Talmor ,  Paula S. Mathias

IPC: G06F30/3323 ,  H04L9/06

Abstract: A method for assertion-based formal verification includes executing a plurality of formal verification regression runs on a model of an electronic design; for each of the regression runs, using a unique signature function, calculating and saving a unique signature value for each instantiation of a property of a plurality of properties of the model of the electronic design and a status result for that instantiation of the property in that regression run; and signing off a current version of the model of the electronic device and presenting as a status result for each the instantiations of a plurality of the properties of the current version of the model of the electronic design the preferred status result obtained for that instantiation of the property per the same unique signature value that was calculated for that instantiation of the property in previous runs of the plurality of formal verification regression runs.

公开(公告)号：US11507720B1

公开(公告)日：2022-11-22

申请号：US17345857

申请日：2021-06-11

Applicant: Cadence Design Systems, Inc.

Inventor： Matheus Nogueira Fonseca ,  Thamara Karen Cunha Andrade ,  Lars Lundgren ,  Breno Guimaraes

IPC: G06F30/30 ,  G01R31/317 ,  G06F30/3323 ,  G06F30/3312 ,  G06F30/31 ,  G06F119/12

Abstract: This disclosure relates to signal observability rating. In an example, a method can include propagating a clock signal through a respective module of a circuit design in a forward and backward direction, evaluating clock signal propagation results for the respective module based on a forward and backward clock signal propagation of the clock signal to compute an observability rating for a data signal to be processed by the respective module during formal verification, and updating a current observability rating of the respective property for the data signal to the computed observability rating.

公开(公告)号：US20240311538A1

公开(公告)日：2024-09-19

申请号：US18121143

申请日：2023-03-14

Applicant: Cadence Design Systems, Inc.

Inventor： Matheus Nogueira Fonseca ,  Lars Lundgren ,  Gabriel Guedes de Azevedo Barbosa ,  Paula Selegato Mathias ,  Luis Humberto Rezende Barbosa ,  Bárbara Leite Almeida ,  Thamara Karen Cunha Andrade ,  Gustavo Augusto Silva Junqueira ,  João Paulo Magalhães de Melo dos Santos

IPC: G06F30/327 ,  G06F11/36 ,  G06F30/331

CPC classification number: G06F30/327 ,  G06F11/3652 ,  G06F30/331 ,  G06F2119/12

Abstract: Embodiments include herein are directed towards a system and method for glitch debugging in an electronic design. Embodiments may include receiving, using a processor, the electronic design and performing a formal glitch analysis of the electronic design to determine if one or more glitches are present in a clock logic of the electronic design. If a glitch is identified, embodiments may further include causing a generation of a graphical glitch debugger display. Embodiments may include receiving an edit to the electronic design and re-performing the formal glitch analysis of the electronic design to determine whether a glitch is present.

公开(公告)号：US11514219B1

公开(公告)日：2022-11-29

申请号：US17212150

申请日：2021-03-25

Applicant: Cadence Design Systems, Inc.

Inventor： Ahmad S. Abo Foul ,  Lars Lundgren ,  Björn Håkan Hjort ,  Habeeb Farah

IPC: G06F30/3323

Abstract: The present disclosure relates to a system and method for assertion-based formal verification in an electronic design environment. Embodiments may include executing, using a processor, an assertion-based formal verification proof process on a model of an electronic design and analyzing a first property associated with the model. Embodiments may further include generating at least one trace of the first property and determining a mapping function associated with the first property. Embodiments may also include storing the at least one trace and the mapping function. Embodiments may further include determining that a second property associated with the model shares a cone of influence with the first property and generating a new trace based upon, at least in part, the mapping function.

公开(公告)号：US10176285B1

公开(公告)日：2019-01-08

申请号：US15435831

申请日：2017-02-17

Applicant: Cadence Design Systems, Inc.

Inventor： Lars Lundgren

IPC: G06F17/50

Abstract: The present disclosure relates to a method for electronic design verification. Embodiments may include receiving, using at least one processor, an electronic design and identifying at least one property violation associated with the electronic design. Embodiments may further include generating a sensitivity path from an input to the at least one property violation. Embodiments may also include analyzing the electronic design to identify one or more of a portion of the electronic design that caused the at least one property violation, a portion of the electronic design that did not cause the at least one property violation, and a portion of the electronic design that has not been analyzed. Embodiments may further include applying at least one of a depth analysis and a breadth analysis to the sensitivity path.

公开(公告)号：US10108767B1

公开(公告)日：2018-10-23

申请号：US15282627

申请日：2016-09-30

Applicant: Cadence Design Systems, Inc.

Inventor： Victor Markus Purri ,  Michael Dennis Pedneau ,  Lars Lundgren ,  Pradeep Goyal

IPC: G06F17/50

Abstract: Disclosed are methods, systems, and articles of manufacture for implementing deadlock detection with formal verification techniques in an electronic design. These techniques identify one or more inputs that include at least an initial state of an electronic design and identify at least one deadlock candidate by sweeping at least a portion of a state space of the electronic design with formal verification techniques. These techniques then determine whether the at least one deadlock candidate is a real deadlock by using a second formal search with the formal verification techniques.