System and method for coherency protocol verification
A system and corresponding method perform verification. The system comprises a verification checker that monitors protocol messages of a coherency protocol. The coherency protocol is implemented via register-transfer level (RTL) logic of a chip to maintain cache coherency on the chip. The protocol messages are generated via the RTL logic. The system further comprises at least one memory. The verification checker performs verification of the coherency protocol based on system state stored in the at least one memory. The verification performed includes updating the system state based on the protocol messages monitored and controlling timing for the updating based on message classes. The message classes are associated with the protocol messages monitored. The verification checker reduces the likelihood that a processor design will have data inconsistency issues and can reduce time-to-market as verification implemented via the verification checker can make the verification effort more efficient.
1 . A system comprising:
a verification checker configured to monitor protocol messages of a coherency protocol implemented via register-transfer level (RTL) logic of a chip to maintain cache coherency on the chip, the protocol messages generated via the RTL logic; and
at least one memory, the verification checker further configured to perform verification of the coherency protocol based on system state stored in the at least one memory, the verification performed including updating the system state based on the protocol messages monitored and controlling timing for the updating based on message classes, the message classes including a fast-path message class and a slow-path message class, the message classes associated with the protocol messages monitored.
2 . The system of claim 1 , wherein the system further comprises a simulator configured to perform simulation of the RTL logic and wherein the protocol messages are generated via the simulation performed.
3 . The system of claim 1 , wherein the timing for the updating is immediate in an event the fast-path message class is associated with a protocol message of the protocol messages monitored.
4 . The system of claim 1 , wherein the fast-path message class indicates that the protocol message associated therewith results in access to memory being granted.
5 . The system of claim 1 , wherein the timing for the updating is delayed and responsive to a trigger in an event the slow-path message class is associated with a protocol message of the protocol messages monitored.
6 . The system of claim 5 , wherein the trigger is a response protocol message of the coherency protocol and wherein the slow-path message class indicates that the protocol message associated therewith results in access to memory being removed.
7 . The system of claim 1 , wherein the verification checker is further configured to:
determine, responsive to the updating, whether the system state updated is a legal state or an illegal state; and
generate an output in an event the system state updated is determined to be the illegal state.
8 . The system of claim 7 , wherein the output is an error message, wherein the verification checker is further configured to output the error message to a simulation log file, and wherein the error message includes a representation of a cache line address associated with the illegal state, a reason for the illegal state, or a combination thereof.
9 . The system of claim 7 , wherein the illegal state is determined based on an ownership state for a cache line indicating multiple exclusive owners.
10 . The system of claim 1 , wherein the verification checker is further configured to:
update the system state and control the timing for the updating on a protocol-message-by-protocol-message basis; and
identify, on the protocol-message-by-protocol-message basis, a respective message class associated with a protocol message of the protocol messages monitored.
11 . The system of claim 1 , wherein the verification checker is further configured to identify the message classes associated with the protocol messages monitored by employing a protocol-message-to-message-class map and wherein the protocol-message-to-message-class map includes mappings between opcodes of the protocol messages monitored and identifiers of the message classes.
12 . The system of claim 1 , wherein the chip includes a plurality of processor cores and wherein the system state includes per-cache-line-per-processor-core ownership state for each processor core of the plurality of processor cores.
13 . A method comprising:
monitoring protocol messages of a coherency protocol implemented via register-transfer level (RTL) logic of a chip to maintain cache coherency on the chip, the protocol messages generated via the RTL logic; and
performing verification of the coherency protocol based on system state, the verification performed including updating the system state based on the protocol messages monitored and controlling timing for the updating based on message classes, the message classes including a fast-path message class and a slow-path message class, the message classes associated with the protocol messages monitored.
14 . The method of claim 13 , wherein the method further comprises performing simulation of the RTL logic and wherein the protocol messages are generated via the simulation performed.
15 . The method of claim 13 , wherein the timing for the updating is immediate in an event the fast-path message class is associated with a protocol message of the protocol messages monitored.
16 . The method of claim 13 , wherein the fast-path message class indicates that the protocol message associated therewith results in access to memory being granted.
17 . The method of claim 13 , wherein the timing for the updating is delayed and responsive to a trigger in an event the slow-path message class is associated with a protocol message of the protocol messages monitored.
18 . The method of claim 17 , wherein the trigger is a response protocol message of the coherency protocol and wherein the slow-path message class indicates that the protocol message associated therewith results in access to memory being removed.
19 . The method of claim 13 , further comprising:
determining, responsive to the updating, whether the system state updated is a legal state or an illegal state; and
generating an output in an event the system state updated is determined to be the illegal state.
20 . The method of claim 19 , wherein the output is an error message, wherein the method further comprises outputting the error message to a simulation log file, and wherein the error message includes a representation of a cache line address associated with the illegal state, a reason for the illegal state, or a combination thereof.
21 . The method of claim 19 , wherein the illegal state is determined based on an ownership state for a cache line indicating multiple exclusive owners.
22 . The method of claim 13 , further comprising:
updating the system state and controlling the timing for the updating on a protocol-message-by-protocol-message basis; and
identifying, on the protocol-message-by-protocol-message basis, a respective message class associated with a protocol message of the protocol messages monitored.
23 . The method of claim 13 , further comprising identifying the message classes associated with the protocol messages monitored, the identifying including employing a protocol-message-to-message-class map, the protocol-message-to-message-class map including mappings between opcodes of the protocol messages monitored and identifiers of the message classes.
24 . The method of claim 13 , wherein the chip includes a plurality of processor cores and wherein the system state includes per-cache-line-per-processor-core ownership state for each processor core of the plurality of processor cores.
25 . A non-transitory computer-readable medium having encoded thereon a sequence of instructions which, when loaded and executed by at least one processor, causes the at least one processor to:
monitor protocol messages of a coherency protocol implemented via register-transfer level (RTL) logic of a chip to maintain cache coherency on the chip, the protocol messages generated via the RTL logic; and
perform verification of the coherency protocol based on system state, the verification performed including updating the system state based on the protocol messages monitored and controlling timing for the updating based on message classes, the message classes including a fast-path message class and a slow-path message class, the message classes associated with the protocol messages monitored.
26 . An apparatus comprising:
means for monitoring protocol messages of a coherency protocol implemented via register-transfer level (RTL) logic of a chip to maintain cache coherency on the chip, the protocol messages generated via the RTL logic; and
means for performing verification of the coherency protocol based on system state, the verification performed including updating the system state based on the protocol messages monitored and controlling timing for the updating based on message classes, the message classes including a fast-path message class and a slow-path message class, the message classes associated with the protocol messages monitored.