Solving multiple array problems interacting with each other in constraint solving for functional verification of logic designs
In some aspects, a logic design undergoes functional verification, which includes generating a test stimulus to apply to the logic design. The test stimulus includes test values for variables representing signals in the logic design. Generating the test stimulus involves a first problem of solving for the test values of the variables subject to constraints on the test values. It is solved as follows. A specification of the logic design is accessed. An array implication graph is generated from the specification. The array implication graph represents the problem as a set of two or more single-array constraint problems. Each single-array constraint problem solves for the test values of a single array of the variables subject to the constraints within that single array. The array implication graph also represents dependencies between different single-array constraint problems. The problem is solved based on the dependencies represented in the array implication graph.
1 . A method comprising:
accessing a specification describing a logic design undergoing functional verification, wherein the functional verification includes generating a test stimulus comprising test values for a plurality of variables representing signals in the logic design, and generating the test stimulus comprises a first problem of solving for the test values of the variables subject to constraints on the test values;
generating, by a processing device, an array implication graph from the specification, wherein:
the array implication graph represents the first problem as a set of two or more single-array constraint problems;
each single-array constraint problem solves for the test values of a single array of the variables subject to the constraints within that single array; and
the array implication graph represents dependencies between different single-array constraint problems;
solving the first problem based on the dependencies represented in the array implication graph; and
generating the test stimulus based on the solved first problem, and applying the test stimulus to the logic design for the functional verification of the logic design.
2 . The method of claim 1 wherein generating the array implication graph from the specification comprises:
recognizing, based on the specification, a type of single-array constraint problem for at least some of single-array constraint problems in the set; and
generating the array implication graph based on the recognized types.
3 . The method of claim 2 wherein recognizing the type of single-array constraint problem uses rule-based pattern recognition.
4 . The method of claim 1 wherein generating the array implication graph from the specification comprises:
recognizing, based on the specification, the dependencies between different single-array constraint problems; and
generating the array implication graph based on the recognized dependencies.
5 . The method of claim 4 wherein recognizing dependencies between different single-array constraint problems uses rule-based pattern recognition.
6 . The method of claim 1 wherein generating the array implication graph from the specification comprises:
generating a word-level syntax tree representation of the first problem from the specification;
recognizing, based on the syntax tree representation, a type of single-array constraint problem for at least some of the single-array constraint problems in the set;
recognizing, based on the syntax tree representation, the dependencies between different single-array constraint problems; and
generating the array implication graph based on the recognized types and the recognized dependencies.
7 . The method of claim 1 wherein solving the first problem based on the dependencies represented in the array implication graph comprises:
individually solving the single-array constraint problems according to the array implication graph.
8 . The method of claim 7 wherein individually solving the single-array constraint problems according to the array implication graph comprises:
determining, from the dependencies represented in the array implication graph, an order for solving the single-array constraint problems; and
individually solving the single-array constraint problems in the determined order.
9 . The method of claim 7 wherein individually solving the single-array constraint problems according to the array implication graph comprises:
when individually solving any particular single-array constraint problem, further constraining the solution based on a previous solution for another single-array constraint problem adjacent to the particular single-array constraint problem in the array implication graph, wherein the further constraint is determined based on the previous solution for the other single-array constraint problem and on the dependency in the array implication graph between the two single-array constraint problems.
10 . The method of claim 9 wherein the other single-array constraint problem implies to the particular single-array constraint problem.
11 . The method of claim 9 wherein the particular single-array constraint problem implies to the other single-array constraint problem.
12 . A system comprising:
a memory storing instructions and an array implication graph for a multi-array constraint problem relating to a logic design; wherein the multi-array constraint problem comprises a set of two or more single-array constraint problems, each single-array constraint problem is a problem to solve for values of variables in a single array subject to constraints on those values, and at least two of the single-array constraint problems interact with each other; and the array implication graph comprises nodes and edges, wherein each node represents one of the single-array constraint problems, and an Imply edge between two nodes represents a dependency between the single-array constraint problems represented by the two nodes; and
a processing device, coupled with the memory and to execute the instructions, the instructions when executed cause the processing device to:
individually solve the single-array constraint problems according to the array implication graph
generating the test stimulus based on the solved first problem; and
applying the test stimulus to the logic design for the functional verification of the logic design.
13 . The system of claim 12 wherein the array implication graph further comprises Join operators and JoinImply edges that represent a dependency involving at least three single-array constraint problems.
14 . The system of claim 12 wherein at least one of the dependencies is a conditional implication.
15 . The system of claim 12 wherein at least one of the edges is unidirectional, and at least one of the edges is bidirectional.
16 . The system of claim 12 wherein the array implication graph contains sufficient information to define each of the single-array constraint problems.
17 . A non-transitory computer readable medium comprising stored instructions, which when executed by a processor device, cause the processor device to:
generate an array implication graph for a multi-array constraint problem, relating to a logic design; wherein the multi-array constraint problem comprises a set of two or more single-array constraint problems, each single-array constraint problem is a problem to solve for values of variables in a single array subject to constraints on those values, at least two of the single-array constraint problems interact with each other, and the array implication graph represents dependencies between single-array constraint problems within the multi-array constraint problem; and
solve the individual single-array constraint problems in accordance with the array implication graph
generating the test stimulus based on the solved first problem; and
applying the test stimulus to the logic design for the functional verification of the logic design.
18 . The non-transitory computer readable medium of claim 17 wherein the multi-array constraint problem solves for test values of variables representing signals in a logic design undergoing logic simulation, subject to constraints on the test values.
19 . The non-transitory computer readable medium of claim 18 wherein the array implication graph is generated from a hardware description language (HDL) specification for the logic design.
20 . The non-transitory computer readable medium of claim 17 wherein the single-array constraint problems comprise one or more of: N-Queens problems, summation problems on multi-dimensional arrays on rows and/or columns, cardinality problems, difference logic problems, counting number of occurrences of a value in an array (e.g., count-ones), ordering problems, and uniqueness problems.