Helper assertion guidance for circuit design verification
AssigneeCadence Design Systems, Inc.
InventorCraig Franklin Deaton
Life of this patent
Estimating the term…
Abstract
Various embodiments provide for determining guidance that assist in determining one or more helper assertions for circuit design verification, which used as part of an electronic design automation (EDA) software.
Claims20
A system for determining guidance that assists in determining one or more helper assertions for circuit design verification, the system comprising:
- a memory storing instructions;
- and
- a hardware processor communicatively coupled to the memory and configured by the instructions to perform operations comprising:
- accessing a cover for an assertion of a circuit design, the assertion describing a design property of the circuit design, the cover being configured to show that the assertion holds true at least once for the circuit design;
- generating a first trace that proves the cover for the circuit design starting from a reset state of the circuit design;
- generating a second trace to prove that the assertion always holds true for circuit design starting from a non-reset state of the circuit design;
- regenerating the second trace, the regenerating comprising causing one or more relevant values of the second trace to become similar to one or more relevant values of the first trace based on a similarity condition by iteratively adjusting and regenerating the one or more relevant values of the second trace;
- and
- causing the first trace and the regenerated second trace to be displayed in a graphical user interface with a set of highlights, each highlight in the set of highlights indicating at least one of a similarity or a difference between the first trace and the regenerated second trace, the set of highlights being used as guidance for determining the one or more helper assertions.
A non-transitory computer-readable medium comprising instructions that, when executed by a hardware processor of a device, cause the device to perform operations for determining guidance that assists in determining one or more helper assertions for circuit design verification, the operations comprising:
- accessing a cover for an assertion of a circuit design, the assertion describing a design property of the circuit design, the cover being configured to show that the assertion holds true at least once for the circuit design;
- generating a first trace that proves the cover for the circuit design starting from a reset state of the circuit design;
- generating a second trace to prove that the assertion always holds true for circuit design starting from a non-reset state of the circuit design;
- regenerating the second trace, the regenerating comprising causing one or more relevant values of the second trace to become similar to one or more relevant values of the first trace based on a similarity condition by iteratively adjusting and regenerating the one or more relevant values of the second trace;
- and
- causing the first trace and the regenerated second trace to be displayed in a graphical user interface with a set of highlights, each highlight in the set of highlights indicating at least one of a similarity or a difference between the first trace and the regenerated second trace, the set of highlights being used as guidance for determining the one or more helper assertions.
A method for determining guidance that assists in determining one or more helper assertions for circuit design verification, the method comprising:
- accessing, by a hardware processor, a cover for an assertion of a circuit design, the assertion describing a design property of the circuit design, the cover being configured to show that the assertion holds true at least once for the circuit design;
- generating, by the hardware processor, a first trace that proves the cover for the circuit design starting from a reset state of the circuit design;
- generating, by the hardware processor, a second trace to prove that the assertion always holds true for circuit design starting from a non-reset state of the circuit design;
- regenerating the second trace by the hardware processor, the regenerating comprising causing one or more relevant values of the second trace to become similar to one or more relevant values of the first trace based on a similarity condition by iteratively adjusting and regenerating the one or more relevant values of the second trace;
- and
- causing, by the hardware processor, the first trace and the regenerated second trace to be displayed in a graphical user interface with a set of highlights, each highlight in the set of highlights indicating at least one of a similarity or a difference between the first trace and the regenerated second trace, the set of highlights being used as guidance for determining the one or more helper assertions.
Dependencies are inferred from the claim text.