Research And Implementation Of Model Checking Cache Coherence Protocol For Multi-core Processor

With the rise in the level of integrated circuit technology, multi-core processors hasbecome a mainstream of high-performance microprocessor structure. To ease the speeddifference between the processor core and memory expanding Introduced Cache to solvethis problem. However, Cache to improve performance at the same time, it also bringsdata inconsistencies. Cache coherence protocol is commonly used to ensure Consisten-cy of data shared between multi-core processors. Cache coherence protocol design andimplementation of the correctness of the decision is not only functional correctness ofmulti-core processors, but also the entire processor size and performance Has a criticalinfluence. Therefore, it is necessary to verify the functional correctness of the Cachecoherency protocol.The SystemC language description of the multi-core processors Cache coherencyprotocol for the study, formal verification method using the most popular model checkingtechniques to complete protocol verification. We design and implement a testing platformfor hardware description language model to solve the verification of multicore processorcache coherence protocol.Cache coherence protocol consisting of multi-core processors parameterized systemverification problem, automatically abstract methods From nature to be validated param-eter system of abstract modeling and simplification, effective compression of the statespace. Application of research results to the classic Cache coherence protocols and FT-1000CPU protocol verification, and achieved good results.In order to verify the symbol migration system, the need for efficient migration ofthe system to complete the symbol Kripke structure model transformation. This paperpresents a new model conversion algorithm is able to generate a smaller scale Kripkestructure.