Verifying a graph-based coherency verification tool

1. A computer-implemented method comprising:

verifying a functional correctness of a graph-based coherency verification tool for logic designs of arrangements of processors and processor caches, the graph-based coherency verification tool using trace files as input for verifying memory ordering rules of a given processor architecture for accesses to the caches, wherein nodes in a graph represent memory accesses and edges represent dependencies between the nodes, the verifying the functional correctness comprising:

providing a specification of a test case for a self-checking tool, the test case comprising a sequence of statements in a high-level description language format, representing memory access events and system events; and

generating trace files with the self-checking tool for the graph-based coherency verification tool by producing permutations of trace events, which are defined by the sequence of statements of the test case.

2. The method of claim 1 , wherein the graph-based coherency verification tool is configured for using trace files of simulations of logic descriptions as input.

3. The method of claim 1 , wherein the trace events comprise at least one of: a system event, an instruction, μ-operations, a Fetch command, a Store command, a cross invalidate command, or a Nest Fetch command.

4. The method of claim 3 , wherein statements of types Fetch and Store represent, respectively, a read and write of a portion of a cache line, statements of type Nest Fetch represent a fetch of a cache line into a memory hierarchy, and statements of type cross invalidate represent an invalidation of a cache line or a change of the cache line's state.

5. The method of claim 1 , further comprising:

parsing a high-level description file comprising the sequence of statements to a matrix data structure of the test case;

expanding the parsed high-level description file to create the permutations of the trace events defined by the sequence of statements, and returning a table data structure; and

iterating over the matrix data structure and the table data structure such that the high-level description file expands to the trace files, each comprising several detailed trace events.

6. The method of claim 5 , wherein parsing the high-level description file comprises:

reading the high-level description file;

processing the trace events defined by the sequence of statements and reading their corresponding attributes; and

returning the matrix data structure, the matrix data structure comprising rows corresponding to the trace events and corresponding attributes.

7. The method of claim 5 , wherein expanding the parsed high-level description file creates variations of the trace events and comprises:

for each row of the matrix data structure, evaluating the corresponding trace event and attributes;

creating permutations of the trace events; and

creating the table data structure from combinations of the created permutations for each trace event, and returning the table data structure containing rows according to the created permutations.

8. The method of claim 5 , wherein the iterating comprises:

iterating over the table data structure in an outer loop to create a trace file for each row of the table data structure; and

iterating over each row of the matrix data structure an inner loop to create one or more detailed trace events for each row of the matrix data structure, to be input to the graph-based coherency verification tool.

9. The method of claim 1 , wherein producing the permutations of the trace events comprises producing all possible permutations of the trace events based on no specific attributes in a trace event being defined.

10. The method of claim 1 , wherein the test case is configured to produce at least one error in memory access order indicated by the graph.

11. The method of claim 1 , wherein the producing the permutation of trace events is based on whether attributes of the trace events are defined.

12. A computer system comprising:

a memory; and

a hardware processor in communication with the memory, wherein the computer system is configured to perform a method comprising:

verifying a functional correctness of a graph-based coherency verification tool for logic designs of arrangements of processors and processor caches, the graph-based coherency verification tool using trace files as input for verifying memory ordering rules of a given processor architecture for accesses to the caches, wherein nodes in a graph represent memory accesses and edges represent dependencies between the nodes, the verifying the functional correctness comprising:

providing a specification of a test case for a self-checking tool, the test case comprising a sequence of statements in a high-level description language format, representing memory access events and system events; and

generating trace files with the self-checking tool for the graph-based coherency verification tool by producing permutations of trace events, which are defined by the sequence of statements of the test case.

13. The computer system of claim 12 , wherein the trace events comprise at least one of: a system event, an instruction, μ-operations, a Fetch command, a Store command, a cross invalidate command, or a Nest Fetch command.

14. The computer system of claim 12 , wherein the method further comprises:

parsing a high-level description file comprising the sequence of statements to a matrix data structure of the test case;

expanding the parsed high-level description file to create the permutations of the trace events defined by the sequence of statements, and returning a table data structure; and

iterating over the matrix data structure and the table data structure such that the high-level description file expands to the trace files, each comprising several detailed trace events.

15. The computer system of claim 14 , wherein parsing the high-level description file comprises:

reading the high-level description file;

processing the trace events defined by the sequence of statements and reading their corresponding attributes; and

returning the matrix data structure, the matrix data structure comprising rows corresponding to the trace events and corresponding attributes.

16. The computer system of claim 12 , wherein producing the permutations of the trace events comprises producing all possible permutations of the trace events based on no specific attributes in a trace event being defined.

17. The computer system of claim 12 , wherein the test case is configured to produce at least one error in memory access order indicated by the graph.

18. A computer program product comprising:

a non-transitory computer readable storage medium readable by a processor and storing instructions for execution by the processor for performing a method comprising:

verifying a functional correctness of a graph-based coherency verification tool for logic designs of arrangements of processors and processor caches, the graph-based coherency verification tool using trace files as input for verifying memory ordering rules of a given processor architecture for accesses to the caches, wherein nodes in a graph represent memory accesses and edges represent dependencies between the nodes, the verifying the functional correctness comprising:

providing a specification of a test case for a self-checking tool, the test case comprising a sequence of statements in a high-level description language format, representing memory access events and system events; and

generating trace files with the self-checking tool for the graph-based coherency verification tool by producing permutations of trace events, which are defined by the sequence of statements of the test case.

19. The computer program product of claim 18 , wherein the trace events comprise at least one of: a system event, an instruction, μ-operations, a Fetch command, a Store command, a cross invalidate command, or a Nest Fetch command.

20. The computer program product of claim 18 , wherein the method further comprises:

parsing a high-level description file comprising the sequence of statements to a matrix data structure of the test case;

expanding the parsed high-level description file to create the permutations of the trace events defined by the sequence of statements, and returning a table data structure; and

iterating over the matrix data structure and the table data structure such that the high-level description file expands to the trace files, each comprising several detailed trace events.