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.

Multicore chips are expected to rely on coherent shared memory. Albeit the coherence hardware can scale gracefully, the protocol state space grows exponentially with core count. That is why design verification requires directed test generation (DTG) for dynamic coverage control under the tight time constraints resulting from slow simulation and short verification budgets. Next generation EDA tools are expected to exploit Machine Learning for reaching high coverage in less time. We propose a technique that addresses DTG as a decision process and tries to find a decision-making policy for maximizing the cumulative coverage, as a result of successive actions taken by an agent. Instead of simply relying on learning, our technique builds upon the legacy from constrained random test generation (RTG). It casts DTG as coverage-driven RTG, and it explores distinct RTG engines subject to progressively tighter constraints. We compared three Reinforcement Learning generators with a state-of-the-art generator based on Genetic Programming. The experimental results show that the proper enforcement of constraints is more efficient for guiding learning towards higher coverage than simply letting the generator learn how to select the most promising memory events for increasing coverage. For a 3-level MESI 32-core design, the proposed approach led to the highest observed coverage (95.81%), and it was 2.4 times faster than the baseline generator to reach the latter's maximal coverage.

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.

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.

Microarchitectures often relax order constraints to meet performance requirements. However, the design of a module handling out-of-order behaviors is error prone, since order relaxation asks for sophisticated control. Besides, its functional verification is challenging, because the module does not preserve at its output the order corresponding to its input data, violating a basic assumption of conventional scoreboards. This paper discusses the verification guarantees of three classes of dynamic checkers and experimentally compares their effectiveness and effort. Results show that a well-designed relaxed scoreboard can achieve the same effectiveness as a complete post-mortem checker with an effort similar to a conventional scoreboard's.