| CPC G06F 30/398 (2020.01) [G06F 30/396 (2020.01)] | 20 Claims |
|
1. A method for formal verification of a multi cycle path (MCP) circuit, the method comprising:
obtaining information on a structure of a MCP circuit;
for at least one selected point in the MCP circuit:
performing backward traversal analysis of the MCP circuit along the cone of influence (COI) of each of the at least one selected point stopping at sequential elements directly driving that point;
constructing a counter circuit for each of the sequential elements directly driving the at least one selected point, and combining the constructed counter circuits to a combined logic circuit of all of the counters in the COI, designed to determine whether signal paths in the COI are stable up to the at least one selected point;
performing a forward traversal analysis of the MCP circuit in a fanout from each of the at least one selected point and up to next immediate sequential elements downstream in signal paths found in the fanout;
constructing a combinational logic circuit for each combinational element in the fanout 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 the combined logic circuit of all of the counters in the COI of said at least one selected point to obtain a monitor circuit; and
performing a formal verification to check an assertion that inputs of the next immediate sequential elements of the monitor circuit are stable at all times.
|