US 10,540,468 B1Granted

Verification complexity reduction via range-preserving input-to-constant conversion

AssigneeInternational Business Machines Corporation

InventorsRaj Kumar Gajavelly, Jason R. Baumgartner, Robert L. Kanzelman, Alexander Ivrii, Pradeep Kumar Nalla

Life of this patent

Estimating the term…

Loading patent…

Abstract

A logic verification program, method and system provide an efficient behavior when verifying large logic designs. The logic is partitioned by cut-nodes that dominate two or more RANDOMS and a check is performed for a given cut-node to determine whether any of the dominated RANDOMS can be merged to a constant by performing satisfiability checks with each RANDOM merged to a constant, to determine whether a range of output values for the given cut-node has been reduced by merging the RANDOM. If the range is not reduced, the RANDOM can be added to the set of merge-able RANDOMS along with the corresponding constant value. If the range has been reduced, the opposite constant value is tried for a node and if the range is reduced for both constants, then the cut-node is abandoned for merging that dominated RANDOM and the next dominated RANDOM is tried.

Claims20

Dependent claims

A computer performed method performed by a general-purpose computer system that verifies equivalence of a logic design, the method comprising:

within the computer system, first identifying a set of one or more cut-nodes, wherein the one or more cut-nodes are output nodes of corresponding partitions of a logic representation in a memory of the computer system that represents the logic design, wherein the one or more cut-nodes each or together dominate at least two corresponding RANDOMS that are input to the corresponding partitions of the logic;
within the computer system, responsive to first identifying the set of one or more cut-nodes, second identifying a set of RANDOMS corresponding to a given cut-node that can individually be merged to either FALSE or TRUE without altering a range of values producible at the given cut-node over non-dominated RANDOMS, along with identifying a constant corresponding to FALSE or TRUE for individual ones of the identified set of RANDOMS for the corresponding cut-node;
responsive to identifying the set of RANDOMS that can be merged, replacing the individual RANDOMS within the identified set of RANDOMS with the corresponding constant for the individual RANDOMS in the corresponding partition of the logic represented in the memory of the computer system, to merge the identified RANDOMS to reduce the number of the input RANDOMS to the corresponding partition of the logic;
and
completing verification of the logic across non-dominated RANDOMS and non-merged RANDOMS to verify the logic.

2 more elements

A computer system comprising a processor for executing program instructions coupled to a memory for storing the program instructions, wherein the program instructions are program instructions for simulating a logic design, wherein the program instructions comprise program instructions for:

within the computer system, first identifying a set of one or more cut-nodes, wherein the one or more cut-nodes are output nodes of corresponding partitions of a logic represented in a memory of the computer system, wherein the one or more cut-nodes each or together dominate at least two corresponding RANDOMS that are input to the corresponding partitions of the logic;
within the computer system, responsive to first identifying the set of one or more cut-nodes, second identifying a set of RANDOMS corresponding to a given cut-node that can individually be merged to either FALSE or TRUE without altering a range of values producible at the given cut-node over non-dominated RANDOMS, along with identifying a constant corresponding to FALSE or TRUE for individual ones of the identified set of RANDOMS for the corresponding cut-node;
responsive to identifying the set of RANDOMS that can be merged, replacing the individual RANDOMS within the identified set of RANDOMS with the corresponding constant for the individual RANDOMS in the corresponding partition of the logic represented in the memory of the computer system, to merge the identified RANDOMS to reduce the number of the input RANDOMS to the corresponding partition of the logic;
completing verification of the logic across non-dominated RANDOMS and non-merged RANDOMS to verify the logic;
and
responsive to successful verification of the logic, fabricating an integrated circuit from a design of the logic.

3 more elements

A computer program product comprising a computer-readable storage medium storing program instructions for execution by a general-purpose computer system, wherein the program instructions are program instructions for simulating a logic design, wherein the program instructions comprise program instructions for:

within the computer system, first identifying a set of one or more cut-nodes, wherein the one or more cut-nodes are output nodes of corresponding partitions of a logic represented in a memory of the computer system, wherein the one or more cut-nodes each or together dominate at least two corresponding RANDOMS that are input to the corresponding partitions of the logic;
within the computer system, responsive to first identifying the set of one or more cut-nodes, second identifying a set of RANDOMS corresponding to a given cut-node that can individually be merged to either FALSE or TRUE without altering a range of values producible at the given cut-node over non-dominated RANDOMS, along with identifying a constant corresponding to FALSE or TRUE for individual ones of the identified set of RANDOMS for the corresponding cut-node;
responsive to identifying the set of RANDOMS that can be merged, replacing the individual RANDOMS within the identified set of RANDOMS with the corresponding constant for the individual RANDOMS in the corresponding partition of the logic represented in the memory of the computer system, to merge the identified RANDOMS to reduce the number of the input RANDOMS to the corresponding partition of the logic;
completing verification of the logic across non-dominated RANDOMS and non-merged RANDOMS to verify the logic;
and
responsive to successful verification of the logic, fabricating an integrated circuit from a design of the logic.

3 more elements

Dependencies are inferred from the claim text.

Facts

Application: 16/032,786Filed 11 Jul 2018
Published: US 2020/0019653 A116 Jan 2020
Granted: 21 Jan 2020
Term ends: Not estimatedThe source records don’t support an estimate.

Classification4 codes

G06F 30/327
Circuit design at the digital level: logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist
G06F 30/33
Circuit design at the digital level: design verification, e.g. functional simulation or model checking
G06F 2117/08
Details relating to the type or aim of the circuit design: hW-SW co-design, e.g. HW-SW partitioning
G06F
Computing and data processing