A method of checking equivalence between a first design comprising a shift register logic SRL chain and a second design comprising a memory block. The method comprises identifying an inductive invariant to replace the SRL chain or the memory block, and replacing the SRL chain and the memory block by a set of constraints, wherein the set of constraints state that the SRL chain and the memory block are equivalent for the checking of equivalence between the first design and the second design.

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.

A formal verification EDA application can be configured to receive a circuit design of an IC chip. The circuit design of the IC chip comprises a set of properties for the IC chip and constraints for the IC chip. The formal verification EDA application generates an array of CNF files based on the circuit design of the IC chip. Each CNF file can include a Boolean expression that characterizes a selected property of the set of properties and data fields characterizing initial states for literals in the Boolean expression and the constraints of the IC chip. The formal verification application can also be configured to output the array of CNF files to a hardware prototyping platform. The hardware prototyping platform can be configured to execute a hardware instantiated SAT solver for the Boolean expression in each CNF file in the array of CNF files.

A hardware design for a main data transformation component is verified. The main data transformation component is representable as a hierarchical set of data transformation components which includes (i) a plurality of leaf data transformation components which do not have children, and (ii) one or more parent data transformation components which each comprise one or more child data transformation components. For each of the plurality of leaf data transformation components, it is verified that an instantiation of the hardware design for the leaf data transformation component generates an expected output transaction in response to each of a plurality of test input transactions. For each of the one or more parent data transformation components, it is formally verified, using a formal verification tool, that an instantiation of an abstracted hardware design for the parent data transformation component generates an expected output transaction in response to each of a plurality of test input transactions. The abstracted hardware design for the parent data transformation component represents each of the one or more child data transformation components of the parent data transformation component with a corresponding abstracted component that for a specific input transaction to the child data transformation component is configured to produce a specific output transaction with a causal deterministic relationship to the specific input transaction.

The present disclosure provides a method and a system for determining the equivalence of the DRM data set and the DRC data set. The system retrieves a DRM data set and a DRC data set, and transforms the DRM data set and the DRC data set into a first data structure node and a second data structure node respectively. The system determines whether the first data structure node and the second data structure node are equivalent according to a data structure node comparison model.

Methods and systems for verifying a hardware design for an integrated circuit that implements a function that is polynomial in an input variable x over a set of values of x. The method includes formally verifying that a first instantiation of the hardware design implements a function that is polynomial of degree k in x by formally verifying that for all x in the set of values of x the first instantiation of the hardware design has a constant k.sup.th difference; and verifying that a second instantiation of the hardware design generates an expected output in response to each of at least k different values of x in the set of values of x.

A system and method for SAT-sweeping is disclosed. According to one embodiment, a method includes determining gate classes by inputting simulation patterns to gates in an integrated circuit design, selecting a candidate gate based on an inverse topological ordering of the gates, and then selecting a driver gate belonging to the same gate class as the candidate gate. A SAT-solver is called based on the candidate gate and the driver gate to confirm equivalence. The candidate gate and the driver gate are then merged in the integrated circuit design.

The present disclosure provides a method and a system for determining the equivalence of the DRM data set and the DRC data set. The system retrieves a DRM data set and a DRC data set, and transforms the DRM data set and the DRC data set into a first data structure node and a second data structure node respectively. The system determines whether the first data structure node and the second data structure node are equivalent according to a data structure node comparison model.

A method and system for improved design verification for a data processing device when performing a logic simulation. The system identifies certain corresponding coverpoints at different points in results of a logic simulation for a design. Using coverage results obtained for the design, a merging of the results is performed for the certain corresponding coverpoints in the design. In the merged results, a coverpoint is considered as covered if at least one corresponding coverpoint is covered during the logic simulation.

Superconducting circuit with virtual timing elements and related methods are described. A method includes specifying a superconducting circuit portion including a timing path comprising: (1) at least one logic gate to be implemented using Josephson junctions, (2) a first virtual timing element for defining a synchronization point along the timing path, and (3) a second virtual timing element for adding latency to the timing path. The method further includes synthesizing the superconducting circuit portion, where the synthesizing comprises treating the first virtual timing element as a first flip-flop and the second virtual timing element as a second flip-flop, where the first flip-flop is treated as being fixed in relation to the at least one logic gate along the timing path, but the second flip-flop is treated as being movable in relation to the at least one logic gate along the timing path.