Cache coherence and relaxed memory consistency challenge the design verification of multicore chips. The well-known self-checking approach based on litmus tests has been successful in uncovering design errors, but it leads to limited coverage. That is why random or directed test generation approaches are used for proper coverage control, but they require a specialized checker to verify shared memory behavior. Unfortunately, the inference-based checkers that provide guarantees against false positives and false negatives are not scalable with core count (unless some memory orderings are known beforehand). On the other hand, scoreboard-based checkers are scalable, but do not offer guarantees against false diagnosis. This article proposes an event-driven algorithm that is scalable without renouncing verification quality, because it relies on direct partial order verification, on-the-fly detection of improper memory orderings, exploitation of extended observability not hampered by design optimizations, and agnostic handling of store atomicity at the implementation level. We compared the new algorithm with two scoreboard-based and one inference-based checker reported in the literature. EveCheck often reaches full error detection with half the test size required by the other checkers, has superior verification quality, and less sensitivity to test generation parameters. Its effort to detect errors was one order of magnitude inferior as compared to the inference-based checker. It did not raise false positives in correct designs, and it was able to discover all the errors studied in faulty designs.

The functional verification of multicore chips requires the generation of parallel test programs able to expose design errors and ensure high coverage in less time. Albeit the coherence hardware can scale gracefully as the number of cores grows, the state space of the coherence protocol increases exponentially. That is why this article describes a directed test generation approach that exploits random test generation (RTG) for avoiding explicit enumeration of the coherence state space while memory consistency is verified. The novel approach was designed for synergy between a data-driven engine that explores neighborhoods toward higher coverage and a model-based engine that exploits constraints while driving RTG toward faster coverage evolution. As compared to a state-of-the-art data-driven generator and to a model-based generator, the proposed approach led to superior coverage evolution with time, when targeting 32-core designs relying on different protocols. For MOESI 2-level, the novel approach was from 4.8 to 18.7 faster to reach the data-driven generator's maximal coverage, and it was up to 2.7 faster to reach the model-driven generator's. For MESI 3-level, it found, in 10 to 15 min, a few errors whose detection required the data-driven generator 45 min to 7 h.

Since nondeterministic behavior is key to exposing shared-memory errors, nonsynchronized parallel programs are often used for verification and test of multicore chips. In the verification phase, however, the slow execution in a simulator requires nonconventional constraints for enabling error exposure with shorter programs. This paper proposes two novel techniques that build upon conventional random test generation for efficient shared-memory verification. The first technique exploits canonical dependence chains for constraining the random generation of instruction sequences so that the races induced at runtime are likely to raise the coverage of state transitions due to memory events conflicting at a same shared location. The second one exploits address space constraints for biasing random address assignment so that the competition of distinct shared locations for a same cache set can be controlled for raising the coverage of state transitions due to eviction events. We built generators relying on each of the proposed techniques, as well as on their combination, and we compared them to a conventional constrained random test generator for 8, 16, and 32-core architectures. Each of the four generators synthesized 1200 distinct test programs for verifying ten faulty designs derived from each of the three architectures (144 000 verification runs in total). For 32-core designs, the combination of the proposed techniques made at least 50% of the generation space capable of exposing errors, improved the median functional coverage by 44% and 83% at the two highest hierarchical levels, and reduced the average verification effort by one order of magnitude in many cases.

Multicore architectures are likely to largely relax sequential consistency constraints on store atomicity and on the ordering between loads and stores, while preserving a coherent shared-memory abstraction. As a result, multicore chip design verification is challenged by the higher number of valid execution witnesses resulting from consistency relaxation and by the larger coherence protocol's state space induced by growing core counts. On the one hand, litmus test generation is effective in exposing consistency bugs, but their coverage of coherence events is limited. On the other hand, random test generation (RTG) leads to higher coverage, but requires specialized checkers and higher observability for detecting subtle consistency errors. Unfortunately, under RTG, no reported checker is able to handle the non-multiple-copy atomic (nMCA) stores arising from full relaxation. This paper proposes an approach that bridges that gap. It relies on an nMCA-compliant abstract specification for shared memory behavior and on an observability template for guiding the insertion of proper monitors into the design representation. We compared a checker built under the novel approach with a conventional one, when running the same test suites, each built with many programs of fixed size. For 4K-instruction programs, the conventional checker raised false positives for 1/3 of the test suites when targeting correct 32-core nMCA designs, whereas the new checker raised none. The improved verification quality resulting from the more general specification of memory behavior came at the expense of negligible overhead, and often led to effort reduction.

This paper proposes a framework for functional verification of shared memory that relies on reusable coverage-driven directed test generation. It reveals a new mechanism to improve the quality of non-deterministic tests. The generator exploits general properties of coherence protocols and cache memories for better control on transition coverage, which serves as a proxy for increasing the actual coverage metric adopted in a given verification environment. Being independent of coverage metric, coherence protocol, and cache parameters, the proposed generator is reusable across quite different designs and verification environments. We report the coverage for 8, 16, and 32-core designs and the effort required for exposing nine different types of errors. The proposed technique was always able to reach similar coverage as a state-of-the-art generator, and it always did it faster above a certain threshold. For instance, when executing tests with 1K operations for verifying 32-core designs, the former reached 65% coverage around 5 times faster than the latter. Besides, we identified challenging errors that could hardly be found by the latter within one hour, but were exposed by our technique in 5 to 30 minutes.

The coherent shared-memory abstraction is expected to keep its crucial role in Chip Multiprocessors even on the scale of hundreds of cores. As a result, the growing hardware complexity to support such abstraction makes the design of the memory system proner to error. Therefore, it is crucial to check for errors in shared-memory behavior as early as possible in the design flow. Given a design representation of a memory subsystem, this paper addresses the pre-silicon verification of its expected behavior, which is captured by the axioms that specify the coherence and consistency requirements of a memory model. As opposed to typical pseudorandom generation of test programs, this paper proposes the exploitation of significant operation orderings from aggressive memory model specifications for inducing load/store sequences that are more effective in uncovering design errors. The effectiveness of the novel technique was evaluated, for 8, 16, and 32-core architectures, when synthesizing 1200 distinct test programs for verifying 8 derivative designs containing errors (9600 use cases per architecture). The synthesized tests explored 5 program sizes, 4 levels of sharing, 4 instruction mixes, and 15 random seeds. Our results show that, as compared to typical pseudorandom generation, the proposed technique is more effective in exposing design errors whose sharing-level distributions are flat. For such design errors, our technique was more effective by 30% on average.