Defesa de Tese de Doutorado (PPGCC/UFSC) - Bruno Dourado Miranda

Defesa de Tese de Doutorado
Programa de Pós-Graduação em Ciência da Computação (PPGCC)
Universidade Federal de Santa Catarina (UFSC)

Título do Trabalho: Action and State Representations for Agent-Directed Test Generation Targeting Multicore Designs
Autor: Bruno Dourado Miranda
Orientadores: Prof. Dr. Márcio Castro, Prof. Dr. Luiz C. V. dos Santos

Resumo:

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 repre-
sentations. 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.

Palavras-chave: Shared Memory. Directed Test Generation. Test Representation. State Representation.