Shared Memory Verification for Multicore Chip Designs

A multicore chip usually provides a shared memory abstraction implemented by a cache coherence protocol. On-chip coherence can scale gracefully as the number of cores grows, and it plays a major role for general purpose applications. Besides, multicore architectures are likely to relax constraints on store atomicity and on the ordering between loads and stores. As a result, the validation of shared memory faces two main challenges: the higher number of valid execution behaviors and the larger coherence protocol's state space. This dissertation faces those challenges and targets an important design automation phase: the (pre-silicon) functional verification of the shared memory subsystem of a multicore chip, whose behavior is specified by a memory consistency model (MCM). The main scientific contribution is a novel approach to the building of MCM checkers, along with technical contributions on random test generation and directed test generation. The contributions were reported by two papers in a premier IEEE/ACM conference and two articles in the most prestigious IEEE journal on Computer Aided Design of Integrated Circuits and Systems.