Action and state representations for agent-directed test generation targeting multicore designs

Abstract

Processadores multicore estão no cerne da computação moderna, desde sistemas móveis e embarcados até servidores de alto desempenho e data centers. Sua eficiência depende de subsistemas complexos de memória compartilhada, regidos por Memory Consistency Models (MCMs) e protocolos de coerência. Garantir a correção desses subsistemas durante o projeto pré-silício é particularmente desafiador devido ao crescimento exponencial do espaço de estados com o aumento do número de núcleos e às regras de ordenação relaxadas de arquiteturas modernas como ARMv8, Power e RISC-V. A verificação funcional baseada em simulação continua sendo a metodologia predominante, na qual a geração de testes orientada por cobertura desempenha um papel crucial. No entanto, a Random Test Generation (RTG) convencional com restrições enfrenta limitações de eficiência sob as restrições impostas pela simulação, o que motiva o uso de técnicas de Directed Test Generation (DTG). Esta tese aborda esses desafios introduzindo duas contribuições complementares que exploram Reinforcement Learning (RL) para aprimorar a geração de testes na verificação de memória compartilhada. Primeiramente, propomos uma representação canônica de programas de teste que codifica comportamentos fundamentais de memória compartilhada, garantindo simultaneamente completude e unicidade. Essa representação possibilita o projeto eficiente de ações para agentes de RL e evita conjuntos de testes redundantes ou restritos. Garantias teóricas e resultados experimentais demonstram que nossa abordagem supera consistentemente três geradores de última geração em termos de cobertura e detecção de erros em projetos com até 32 núcleos. Em segundo lugar, apresentamos uma representação de estado de ambiente multicore para geração de testes dirigida por agentes. Essa contribuição define como observar e codificar o comportamento de um Design Under Verification (DUV) utilizando testemunhas de execução derivados da relação reads-from. Ao produzir assinaturas únicas para cada execução observável e reconstruir informações de estado a partir de históricos limitados de pares ação?observação, a representação proposta aprimora a observabilidade do ambiente e permite que agentes de RL generalizem entre diferentes tarefas de verificação. Experimentos conduzidos em arquiteturas SPARC e ARMv8, utilizando os protocolos Modified Exclusive Shared Invalid (MESI) e Modified Owned Exclusive Shared Invalid (MOESI), confirmam sua eficácia e reutilização. Ambas as contribuições foram validadas em um ambiente de verificação orientado por cobertura construído sobre o simulador gem5, integrado a verificadores de MCM e múltiplos analisadores de cobertura. Avaliações comparativas com geradores de última geração demonstram evolução mais rápida da cobertura e detecção antecipada de erros ao adotar as representações propostas. Em conjunto, esses resultados estabelecem novas bases para a aplicação de abordagens baseadas em aprendizado na verificação funcional de sistemas de memória compartilhada, abrindo oportunidades para uma validação pré-silício mais eficiente de arquiteturas multicore.Abstract: Multicore processors are at the core of modern co

Abstract: Multicore processors are at the core of modern computing, from mobile and embedded systems to high-performance servers and data centers. Their efficiency relies on complex shared-memory subsystems governed by Memory Consistency Models (MCMs) and coherence protocols. Ensuring the correctness of these subsystems during pre-silicon design is particularly challenging due to the exponential growth of states with the number of cores and the relaxed ordering rules of modern architectures such as ARMv8, Power, and RISC-V. Simulation-based functional verification remains the predominant methodology, where coverage-driven test generation plays a crucial role. However, conventional constrained Random Test Generation (RTG) struggles with efficiency under simulation constraints, motivating the use of Directed Test Generation (DTG) techniques. This thesis addresses these challenges by introducing two complementary contributions that leverage Reinforcement Learning (RL) to enhance test generation for shared-memory verification. First, we propose a canonical test-program representation that encodes fundamental shared-memory behaviors while ensuring both completeness and uniqueness. This representation enables effective action design for RL agents and avoids redundant or restricted test suites. Theoretical guarantees and experimental results demonstrate that our approach consistently outperforms three state-of-the-art generators in terms of coverage and error detection across 32-core designs. Second, we present a multicore environment state representation for agent-directed test generation. This contribution defines how to observe and encode the behavior of a Design Under Verification (DUV) using execution witnesses derived from the reads-from relation. By producing unique signatures for every observable execution and reconstructing state information from bounded histories of action-observation pairs, the proposed representation improves environment observability and enables RL agents to generalize across verification tasks. Experiments on SPARC and ARMv8 architectures, using Modified Exclusive Shared Invalid (MESI) and Modified Owned Exclusive Shared Invalid (MOESI) protocols, confirm its effectiveness and reusability. Both contributions were validated within a coverage-driven verification framework built on the gem5 simulator, integrated with MCM checkers and multiple coverage analyzers. Comparative evaluations against state-of-the-art generators demonstrate faster coverage evolution and earlier error diagnosis when adopting the proposed representations. Together, these results establish new foundations for applying learning-based approaches to functional verification of shared-memory systems, opening opportunities for more efficient pre-silicon validation of multicore architectures.