Glitch detection at clock domain crossing

1. A method comprising:

identifying, by a computing system, combinational logic in a circuit design, which is configured to generate an output signal based, at least in part, on an input signal received by the combinational logic and an inversion of the input signal, wherein the output signal generated by the combinational logic is configured to cross between clock domains in the circuit design;

generating, by the computing system, a glitch expression based, at least in part, on a configuration of the combinational logic, wherein the glitch expression includes conditions, the satisfaction of which causes the combinational logic to generate the output signal using both the input signal and the inversion of the input signal; and

determining, by the computing system, the combinational logic is configured to generate at least one glitch in the output signal based, at least in part, on the glitch expression.

2. The method of claim 1 , wherein generating the glitch expression further comprises identifying the conditions, the satisfaction of which causes the combinational logic to generate the output signal using both the input signal and the inversion of the input signal, wherein generating the glitch expression is based, at least in part, on the identified conditions.

3. The method of claim 2 , wherein determining the combinational logic is configured to generate at least one glitch in the output signal further comprises:

performing formal verification operations on the glitch expression; and

determining the combinational logic is configured to generate at least one glitch in the output signal when the formal verification operations indicate the conditions in the glitch expression are capable of being satisfied.

4. The method of claim 1 , further comprising generating, by the computing system, a cover expression representing additional logic that, when combined to the combinational logic, eliminates glitches introduced by the combinational logic in the output signal.

5. The method of claim 4 , further comprising modifying, by the computing system, the circuit design to combine the additional logic with the combinational logic.

6. The method of claim 1 , wherein the glitch in the output signal is an unintended value-level in the output signal due to differences in signal propagation delay through the combinational logic.

7. A system comprising:

a memory device configured to store machine-readable instructions; and

a computing system including one or more processing devices, in response to executing the machine-readable instructions, configured to:

identify combinational logic in a circuit design, which is configured to generate an output signal based, at least in part, on an input signal received by the combinational logic and an inversion of the input signal, wherein the output signal generated by the combinational logic is configured to cross between clock domains in the circuit design;

generate a glitch expression based, at least in part, on a configuration of the combinational logic, wherein the glitch expression includes conditions, the satisfaction of which causes the combinational logic to generate the output signal using both the input signal and the inversion of the input signal; and

determine the combinational logic is configured to generate at least one glitch in the output signal based, at least in part, on the glitch expression.

8. The system of claim 7 , wherein the one or more processing devices, in response to executing the machine-readable instructions, are further configured to generate the glitch expression by:

identifying the conditions, the satisfaction of which causes the combinational logic to generate the output signal using both the input signal and the inversion of the input signal; and

generating the glitch expression based, at least in part, on the identified conditions.

9. The system of claim 8 , wherein the one or more processing devices, in response to executing the machine-readable instructions, are further configured to determine the combinational logic is configured to generate at least one glitch in the output signal by:

performing formal verification operations on the glitch expression; and

determining the combinational logic is configured to generate at least one glitch in the output signal when the formal verification operations indicate the conditions in the glitch expression are capable of being satisfied.

10. The system of claim 7 , wherein the one or more processing devices, in response to executing the machine-readable instructions, are further configured to generate a cover expression representing additional logic that, when combined to the combinational logic, eliminates glitches introduced by the combinational logic in the output signal.

11. The system of claim 10 , wherein the one or more processing devices, in response to executing the machine-readable instructions, are further configured to modify the circuit design to combine the additional logic with the combinational logic.

12. An apparatus comprising at least one computer-readable memory device storing instructions configured to cause one or more processing devices to perform operations comprising:

identifying combinational logic in a circuit design, which is configured to generate an output signal based, at least in part, on an input signal received by the combinational logic and an inversion of the input signal, wherein the output signal generated by the combinational logic is configured to cross between clock domains in the circuit design;

generating a glitch expression based, at least in part, on a configuration of the combinational logic, wherein the glitch expression includes conditions, the satisfaction of which causes the combinational logic to generate the output signal using both the input signal and the inversion of the input signal; and

determining the combinational logic is configured to generate at least one glitch in the output signal based, at least in part, on the glitch expression.

13. The apparatus of claim 12 , wherein generating the glitch expression further comprises identifying the conditions, the satisfaction of which causes the combinational logic to generate the output signal using both the input signal and the inversion of the input signal, wherein generating the glitch expression is based, at least in part, on the identified conditions.

14. The apparatus of claim 13 , wherein determining the combinational logic is configured to generate at least one glitch in the output signal further comprises:

performing formal verification operations on the glitch expression; and

determining the combinational logic is configured to generate at least one glitch in the output signal when the formal verification operations indicate the conditions in the glitch expression are capable of being satisfied.

15. The apparatus of claim 12 , wherein the instructions are configured to cause the one or more processing devices to perform operations further comprising generating a cover expression representing additional logic that, when combined to the combinational logic, eliminates glitches introduced by the combinational logic in the output signal.

16. The apparatus of claim 15 , wherein the instructions are configured to cause the one or more processing devices to perform operations further comprising modifying the circuit design to combine the additional logic with the combinational logic.

17. The apparatus of claim 12 , wherein the glitch in the output signal is an unintended value-level in the output signal due to differences in signal propagation delay through the combinational logic.