Verifying a graph-based coherency verification tool
Verification is provided of 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 them. The verifying includes (i) 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 (ii) 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.
1. A computer-implemented for improving correctness of a graph-based coherency verification tool and cache coherency reliability, the 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 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, wherein the test case is a failing scenario; 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 the Fetch of a cache line into the memory hierarchy, and statements of type cross invalidate represent the invalidation of a cache line or a change of the cache line 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 producing the permutation of trace events is based on whether attributes of the trace events are defined.
11. 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.
12. A computer system for improving correctness of a graph-based coherency verification tool and cache coherency reliability, the computer system comprising:
a memory; and
a 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 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, wherein the test case is a failing scenario; 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, p-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. A computer program product for improving correctness of a graph-based coherency verification tool and cache coherency reliability, the computer program product comprising:
a 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 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, wherein the test case is a failing scenario; 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.
18. The computer program product of claim 17 , 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.
19. The computer program product of claim 17 , 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.