Modeling and verification of circuit with dual-edge clocked logic

A method comprising:

• receiving a logical model of a circuit written in a hardware description language (HDL), the logical model of the circuit comprising normalized and ratioed clocks, and simulation-efficient edge-triggered latches or flip-flops;
• translating the logical model of the circuit into a physical model of the circuit in the HDL via a software application, wherein the translating comprises replacing the normalized and ratioed clocks in the logical model of the circuit with a base system clock, divider logic generating hold waveforms to achieve ratioed behavior, and pulse-enabled latches, and replacing the edge-triggered latches or flip-flops with pulse-generation logic and pulse-enabled latches;
• executing a formal verification which determines whether the logical model of the circuit is functionally equivalent to the physical model of the circuit;
• and
• displaying results of the formal verification via a graphical user interface (GUI) of the software application.

A computer-readable hardware storage medium comprising instructions which when executed by a processor cause the processor to perform:

• receiving a logical model of a circuit written in a hardware description language (HDL), the logical model of the circuit comprising normalized and ratioed clocks, and simulation-efficient edge-triggered latches or flip-flops;
• translating the logical model of the circuit into a physical model of the circuit in the HDL via a software application, wherein the translating comprises replacing the normalized and ratioed clocks in the logical model of the circuit with a base system clock, divider logic generating hold waveforms to achieve ratioed behavior, and pulse-enabled latches, and replacing the edge-triggered latches or flip-flops with pulse-generation logic and pulse-enabled latches;
• executing a formal verification which determines whether the logical model of the circuit is functionally equivalent to the physical model of the circuit;
• and
• displaying results of the formal verification via a graphical user interface (GUI) of the software application.