Test generation for shared-memory verification of multicore chips

Tese (doutorado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2021.Multiprocessadores consistem de processadores fortemente acoplados que compartilham um espaço de endereçamento de memória e são construídos com um ou múltiplos multicore chips. O susbsistema de memória compartilhada envolve componentes de hardware complexos que implementam um sofisticado protocolo de coerência cujo projeto em RTL é propenso a erros. Esta tese contribui para a verificação funcional do comportamento da memória compartilhada durante o projeto de multicore chips. Uma vez que o comportamento não determinístico é chave para expor erros de memória compartilhada, programas paralelos não sincronizados são frequentemente utilizados para a verificação do projeto e para o teste do protótipo. No entanto, durante a etapa de verificação, a lenta execução em um simulador requer o uso de técnicas não convencionais para expor erros e prover alta cobertura com programas mais curtos. Neste contexto, esta tese faz três contribuições. A primeira contribuição consiste em duas técnicas que impõem restrições à geração aleatória convencional de programas de teste para viabilizar a verificação eficiente da memória compartilhada. Uma delas explora cadeias canônicas de dependências para restringir a geração aleatória de sequências de instruções (de forma a aumentar a cobertura de transições entre estados que são induzidas por eventos de conflito em um mesmo endereço), outra explora restrições sobre o espaço de endereçamento para restringir o assinalamento aleatório de endereços distintos (de forma a aumentar a cobertura de transições entre estados devidas a eventos de evicção). Quando comparada a um gerador convencional, a combinação destas técnicas reduziu o esforço médio de verificação em uma ordem de magnitude em vários casos. A segunda contribuição é um novo mecanismo de geração dirigida por modelo de cobertura para melhorar a qualidade de testes não determinísticos. O mecanismo explora propriedades gerais de protocolos de coerência e de memórias cache para melhor controlar a cobertura de transições entre estados (a qual serve como proxy para aumentar a cobertura de acordo com a métrica que vier a ser adotada em um dado ambiente de verificação). Por ser independente de métrica de cobertura, de protocolo de coerência, e de parâmetros de cache, o mecanismo é reusável em projetos e ambientes de verificação bem diferentes. Este gerador baseado em modelo foi mais rápido para atingir valores de cobertura similares aos de um gerador dirigido por dados baseado em Programação Genética, reportado em trabalho correlato. Por exemplo, ao executar testes com 1K operações para verificar projetos de 32 núcleos, este nosso gerador alcançou 60% da cobertura dez vezes mais rápido. A terceira contribuição é uma abordagem híbrida, a qual não é uma simples combinação de uma técnica dirigida por dados com outra dirigida por modelo. A abordagem reformula a geração dirigida de testes como um problema de otimização com dois objetivos e explora vizinhanças para evitar a enumeração explícita do espaço de estados do protocolo de coerência, sem excluir soluções ótimas do espaço de pesquisa. Comparada com um gerador puramente dirigido por dados e com outro baseado em modelo, a abordagem híbrida levou a uma melhor evolução da cobertura ao longo do tempo, quando avaliada para 32 núcleos e para diferentes protocolos de coerência. Por exemplo, para um protocolo MOESI de dois níveis, a abordagem foi 2,7 vezes mais rápida do que o gerador baseado em modelo e cerca de 5 a 19 vezes mais rápido do que o gerador dirigido por dados. Finalmente, a abordagem híbrida também foi comparada com um gerador dirigido por dados baseado em Aprendizado por Reforço. Os resultados experimentais mostraram que a abordagem híbrida proposta é de 2 a 3 vezes mais rápida para obter a máxima cobertura atingida por aquele gerador.Abstract: Multiprocessors consist of tightly coupled processors that share some memory address space and are built with a single or multiple multicore chips. The shared-memory subsystem involves complex hardware components implementing a sophisticated coherence protocol whose RTL design is prone to errors. This thesis contributes to the functional verification of shared-memory behavior during the design of multicore chips. Since non-deterministic behavior is key to exposing shared-memory errors, non-synchronized parallel programs are often used for design verification and prototype test. However, in the verification phase, the slow execution in a simulator requires non-conventional techniques for enabling error exposure and high coverage with shorter programs. In this context, this thesis makes three contributions. The first contribution consists of two techniques that build upon conventional random test generation for efficient shared-memory verification. One technique exploits canonical dependence chains for constraining the random generation of instruction sequences (to raise the coverage of state transitions due to memory events conflicting at a same shared location), another exploits address space constraints for biasing random address assignment (to raise the coverage of state transitions due to eviction events). As compared to a conventional generator, their combination reduced the average verification effort by one order of magnitude in many cases. The second contribution is a new mechanism for directed generation that improves the quality of non-deterministic racy tests. The mechanism 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 mechanism is reusable across quite different designs and verification environments. Such a model-based generator was faster to reach similar coverage as obtained by a data-driven generator (based on Genetic Programming), reported in a related work. For instance, when executing tests with 1K operations for verifying 32-core designs, our test generator reached 60% coverage ten times faster. The third contribution consists of an hybrid approach that is not a simple combination of data-driven and model-based techniques. It reformulates directed test generation as a double-objective optimization problem, and it explores neighborhoods to avoid explicit enumeration of the coherence state space without excluding optimal solutions from the search space. As compared to purely data-driven and model-based generators, the hybrid approach led to superior coverage evolution with time, when targeting 32-core designs relying on different protocols. For instance, for a MOESI 2-level protocol, the approach was up to 2.7 faster than the model-based generator and around 5 to 19 times faster than the data-driven generator. Finally, the hybrid approach was also compared to a data-driven generator based on Reinforcement Learning. The experimental results showed that the proposed hybrid approach was 2 to 3 times faster to obtain the maximal coverage reached by that generator