A crucial step in the design of multicore systems is to validate the interaction between cores. This involves test program generation and runtime analysis. We propose a novel reinforcement learning approach to directed test generation, where an agent induces a suite of programs, which are executed in a simulation environment for a multicore. It focuses on how to recover state information from raw observations of the environment such that the agent can learn from interaction how to improve coverage for any verification task. We evaluated our state representation for different verification tasks involving 16 and 32-core ARMv8 2-level MOESI designs.

The scope of this article is the design verification of a multicore chip or multichip multiprocessor by running concurrent test programs until coverage goals are reached. Interactions between multiple processors through shared memory must obey a memory consistency model, which specifies valid behaviors. We propose a canonical test-program representation that encodes primal shared-memory behaviors to be induced at runtime. It is intended as one of the main keys to the design of new test generators. We prove that our representation does not limit the search space, because it induces equivalence classes that can be completely and uniquely encoded. In particular, we show experimental evidence that our representation is also suitable to learning-based test generators, because it enables the design of effective actions. We have built a generator directed by a Reinforcement Learning agent, designed its actions based on our encoding, and compared it with three generators when targeting 32-core designs. For a given time limit, our generator reached the largest coverage and led to the fastest error diagnosis in 3/4 of the verification scenarios, despite our choice of a minimalist agent. The theoretical guarantees and the experimental evidence indicate that our representation provides proper grounds for defining effective actions, and it prevents them from either inducing redundant tests or limiting the test suite.