Cadence Design Systems, Inc.

Karam Abdelkader

Doron Bustan

Habeeb Farah

Thiago Radicchi Roque

Yaron Schiller

Felipe Althoff

Ayman Hanna

Almothana Sirhan

Method includes, for a point in MCP circuit, performing backward traversal of the circuit along the COI of that point, to sequential elements directly driving that point; constructing a counter circuit for all sequential elements driving that point, and combining the constructed counter circuits to a combined logical circuit of all of the counters in the COI, to determine whether signals in the COI are stable; performing a fan out traversal of the MCP circuit from the selected point and up to next immediate sequential elements downstream in the fan out; constructing a combinational logic circuit for the combinational elements in the fan out to determine whether that combinational element blocks a signal of the signal paths when that signal is unstable, and combining the combinational logic circuits to a combined combinational logic circuit; and checking an assertion that inputs of the next immediate sequential elements are stable.

System and method for formal verification of a multi-cycle path circuit

A method for enhancing performance of SEC of two representations of an electronic design (with and without gated clock) includes selecting one or more pairs of correlated flip-flops (FFs), a first FF of each pair in the first representation toggled by the gated clock controlled by an enable combinational logic and a second FF of the pair, correlating to the first FF, in the second representation toggled by the constantly toggling clock. The method also includes defining a modified enable combinational logic for the gated clock, as a disjunction of the enable combinational logic of the gated clock and an enable combinational logic for each FF of a plurality of FFs that are toggled by the gated clock. The method also includes performing SEC on the two representations design, using the modified enable combinational logic for the gated clock instead of the enable combinational logic of the gated clock.

Method and system for sequential equivalence checking

A method for sequential equivalence checking (SEC) of two representations of an electronic design may include using a processor, automatically selecting a plurality of cutpoints in the two representations of the electronic design; using a processor, automatically executing a prove-from strategy on the plurality of cut point pairs to identify a failed cut point pair in the two electronic designs; and using the processor, automatically extending a trace corresponding to the identified failed cut point pair to identify a deeper failed cut point pair or a failed output pair in the two electronic designs.

A method for sequential equivalence checking (SEC) of two representations of an electronic design includes selecting by a processor a plurality of cutpoints in the two representations of the electronic design, rendering the two representations of the electronic design abstracted; executing by the processor an assume-guarantee (AG) proof on the two abstracted representations of the electronic design; identifying by the processor a failed assertion indicating non-equivalence of a signal pair relating to one of the cutpoints; and performing by the processor a simulation on the two representations of the electronic design by successively inputting input stimuli of a trace corresponding to the failed assertion in a sequential order in which the input stimuli appear in the trace at inputs of the two representations of the electronic design to identify whether there is one or a plurality of additional non-equivalent signal pairs relating to other cutpoints of said plurality of cutpoints.

Growing community of inventors

Haifa, Israel

Karam Abdelkader