# US 2020/0401750 A1 · Verifying glitches in reset path using formal verification and simulation > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 2020/0401750 A1 - Document ID: US20200401750A1 - Status: Published application - Kind: A1 - Application number: 16/910,953 - Filed: 2020-06-24 - Published: 2020-12-24 - Earliest claimed: 2019-06-24 - Assignees: Synopsys, Inc. - Applicants: Synopsys, Inc. - Inventors: Sudeep MONDAL; Paras MAL JAIN; Anshul TUTEJA - Web page: https://patentgrep.com/patent/US20200401750A1 ## CPC - G06F 30/3308: using simulation - G06F 30/323: Translation or migration, e.g. logic to logic, hardware description language [HDL] translation or netlist translation - G06F 30/3323: using formal methods, e.g. equivalence checking or property checking - G06F 2119/12: Timing analysis or timing optimisation - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract A method and a system for identifying glitches in a circuit are provided. The method includes identifying a sub-circuit that drives a net from a plurality of nets in a circuit, generating a glitch detection circuit comprising dual-rail encoding from the net to a signal driver of the sub-circuit, modifying the sub-circuit to include the glitch detection circuit, generating an optimized hardware design language (HDL) output file associated with the glitch detection circuit and the sub-circuit, and performing a simulation or a formal verification of the optimized HDL output file to determine whether a signal associated with the net glitches. ## Claims ### Claim 1 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, a glitch detection circuit comprising dual-rail encoding from the net to a signal driver of the sub-circuit; modifying, by the at least one computer processor, the sub-circuit to include the glitch detection circuit; generating, by the at least one computer processor, an optimized hardware design language (HDL) output file associated with the glitch detection circuit and the sub-circuit; and performing a simulation or a formal verification, by the at least one computer processor, of the optimized HDL output file to determine whether a signal associated with the net glitches. ### Claim 2 (depends on 1) The method of claim 1, wherein the dual-rail encoding is based on a functional expression and the functional expression is defined in the optimized HDL output file. ### Claim 3 (depends on 2) The method of claim 2, wherein the optimized HDL output file is optimized for readability and to minimize the number of lines in the optimized HDL output file. ### Claim 4 (depends on 1) The method of claim 1, wherein generating the optimized HDL output file includes: resynthesizing a netlist of an HDL output file; and converting the HDL output file from a first format to a second format. ### Claim 5 (depends on 1) The method of claim 1, wherein generating the optimized HDL output file includes: segregating an HDL output file into two or more sections; and modifying a signal name as a function of an associated respective section of the two or more sections. ### Claim 6 (depends on 1) The method of claim 1, wherein the optimized HDL output file is a Verilog file. The method of claim 1, wherein the net is connected to a reset pin of a device. ### Claim 8 (depends on 1) The method of claim 1, wherein modifying the sub-circuit includes: providing an input value to the glitch detection circuit based on a preset condition. ### Claim 9 (depends on 8) The method of claim 8, wherein providing the input value to the glitch detection circuit comprises: setting the input value to the glitch detection circuit to a NULL state when a previous value and a current value of the input value of the sub-circuit are different. ### Claim 10 (depends on 9) The method of claim 9, wherein providing the input value to the glitch detection circuit comprises: setting the input value to the glitch detection circuit to a zero input when a previous value of the input value to the glitch detection circuit is equal to a current value of the input value to the glitch detection circuit, the previous value being equal to zero; and setting the input value to the glitch detection circuit to a one input when the previous value of the input value to the glitch detection circuit is equal to the current value of the input value to the glitch detection circuit, the previous value being equal to one. ### Claim 11 (depends on 1) The method of claim 1, wherein modifying the sub-circuit includes: determining that a glitch occurred when an output of the glitch detection circuit switches from a de-asserted state to an asserted state. ### Claim 12 (depends on 1) The method of claim 1, wherein generating the glitch detection circuit comprises: generating previous cycle variables for a plurality of inputs to the sub-circuit; combining the plurality of inputs to the sub-circuit to generate a high rail net value; and combining the previous cycle variables to generate a low rail net value. ### Claim 13 (depends on 1) The method of claim 1, further comprising: generating an abstract port associated with a primary input; and associating a clock to the abstract port. ### Claim 14 (depends on 13) The method of claim 13, wherein the clock is a virtual clock when a block associated with the primary input is abstracted out and is not available. ### Claim 15 (depends on 1) The method of claim 1, further comprising encoding the optimized HDL output file. ### Claim 16 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. ### Claim 17 (depends on 16) The system of claim 16, wherein the dual-rail encoding is based on a functional expression and the functional expression is defined in the optimized HDL output file. ### Claim 18 (depends on 16) The system of claim 16, wherein the optimized HDL output file is a Verilog file. ### Claim 19 (depends on 16) The system of claim 16, wherein the processor is further configured to: generate an abstract port associated with a primary input; and associate a clock to the abstract port. ### Claim 20 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.