US 7,257,786 B1 · Method and apparatus for solving constraints

Abstract

An approach to solving combinational constraints, comprising compile and generate phases, is presented. The compile phase constructs successive sets of constraints, each with a solution generator, according to blocks of a partition of the constraints' random variables. Interleaving conjunction of the constraints, with existential quantification of the constraints, is attempted. The generate phase uses a reverse-order, block-by-block, process for solving constraints, where variables of each solution generator processed have been predetermined, by the processing of earlier blocks, except for the random variables of the current block. The present invention can be used in conjunction with image computation. Successive sets of reachable states of an FSM at successive time steps can be determined by successive applications of the compile phase, with each set of solution generators being saved. The sets of solution generators permit a backward sequence of states, from an error state back to a start state, to be determined.

Claims10

Dependent claims

A computing environment comprising a computer program, the computer program for solving constraints during functional verification of a representation of an electronic design of an integrated circuit (IC), the computer program comprising the following steps when executed by a data processing system:

selecting a first set of block-related constraints, from a first set of constraints, according to a first block;
identifying a first set of non-block-related constraints, from the first set of constraints, not selected for the first set of block-related constraints;
conjoining the first set of block-related constraints to produce a first solution generator;
existentially quantifying the first block from the first solution generator to produce a first new constraint;
computing a union of the first new constraint and the first set of non-block-related constraints to produce a second set of constraints;
selecting a second set of block-related constraints, from the second set of constraints, according to a second block;
conjoining the second set of block-related constraints to produce a second solution generator;
solving the second solution generator;
and
solving the first solution generator using a second result of solving the second solution generator.

7 more elements

A computer program product for solving during functional verification of a representation of an electronic design of an integrated circuit (IC) comprising:

a computer usable medium having computer readable code embodied therein for determining a solution to a set of constraints, the computer program product including:
computer readable program code devices configured to cause a computer to effect selecting a first set of block-related constraints, from a first set of constraints, according to a first block;
computer readable program code devices configured to cause a computer to effect conjoining the first set of block-related constraints to produce a first solution generator;
computer readable program code devices configured to cause a computer to effect existentially quantifying the first block from the first solution generator to produce a first new constraint;
computer readable program code devices configured to cause a computer to effect identifying a first set of non-block-related constraints, from the first set of constraints, not selected for the first set of block-related constraints;
computer readable program code devices configured to cause a computer to effect computing a union of the first new constraint and the first set of non-block-related constraints to produce a second set of constraints;
computer readable program code devices configured to cause a computer to effect selecting a second set of block-related constraints, from the second set of constraints, according to a second block;
computer readable program code devices configured to cause a computer to effect conjoining the second set of block-related constraints to produce a second solution generator;
computer readable program code devices configured to cause a computer to effect solving the second solution generator;
and
computer readable program code devices configured to cause a computer to effect solving the first solution generator using a second result of solving the second solution generator.

8 more elements

Dependencies are inferred from the claim text.

Method and apparatus for solving constraints

Life of this patent

Method and apparatus for solving constraints

Life of this patent

Abstract

Claims10