Verifying glitches in reset path using formal verification and simulation

A system comprising:

• a memory storing instructions;
• and
• a processor, coupled with the memory and to execute the instructions, the instructions when executed cause the processor to:
• identify a sub-circuit that drives a net from a plurality of nets in a circuit,
• generate a glitch detection circuit comprising dual-rail encoding from the net to a signal driver of the sub-circuit,
• modify the sub-circuit to include the glitch detection circuit,
• generate an optimized hardware design language (HDL) output file associated with the glitch detection circuit and the sub-circuit, and
• perform a simulation or a formal verification of the optimized HDL output file to determine whether a signal associated with the net glitches.

A method, comprising:

• identifying, by at least one computer processor, a sub-circuit that drives a net from a plurality of nets in a circuit;
• generating, by the at least one computer processor, an abstract port for a signal driver of the sub-circuit when the signal driver is associated with a primary port of the circuit;
• generating, by the at least one computer processor, a glitch detection circuit comprising dual-rail encoding from the net to the signal driver of the sub-circuit;
• modifying, by the at least one computer processor, the sub-circuit to include the glitch detection circuit;
• and
• performing one of a simulation and a formal verification, by the at least one computer processor, of the output file to determine whether a signal associated with the net glitches.