Metastability injector for a circuit description

A method of verifying a design of a circuit under verification, the method comprising:

• transforming an original description of the circuit under verification by adding description of circuitry to inject effects of metastability into the circuit under verification, resulting in a transformed description;
• analyzing the transformed description using a model checking method, to automatically determine a stimulus sequence to violate a pre-determined assertion using an inverted clock domain crossing signal that is inverted to inject the effects of metastability by the added description of the circuitry;
• and
• outputting a result of the analysis.

A method of verifying a design of a circuit under verification, the method comprising:

• determining an original description of the circuit under verification;
• adding a description of metastability injection circuitry configured to inject effects of metastability into the circuit under verification to generate a transformed description of the original description of the circuit under verification;
• testing the transformed description to determine if a stimulus sequence violates a pre-determined assertion when the transformed description is tested with effects of metastability, wherein testing comprises:
• inverting a clock domain crossing signal to inject the effects of metastability;
• and
• analyzing one or more stimulus sequences to determine if the pre-determine assertion is violated using the inverted clock domain crossing signal for the one or more sequence;
• outputting a result of the test.

Software encoded in one or more computer-readable media for execution by the one or more processors and when executed operable to:

• determine an original description of a circuit under verification;
• add a description of metastability injection circuitry configured to inject effects of metastability into the circuit under verification to generate a transformed description of the original description of the circuit under verification;
• test the transformed description to determine if a stimulus sequence violates a pre-determined assertion when the transformed description is tested with effects of metastability, wherein software operable to test comprises software operable to:
• invert a clock domain crossing signal to inject the effects of metastability;
• and
• analyze one or more stimulus sequences to determine if the pre-determined assertion is violated using the inverted clock domain crossing signal for the one or more stimulus sequences;
• output a result of the test.