O objetivo geral desta proposta é a construção ...o objetivo geral desta proposta é a construção de um framework para a verificação funcional de multicore chips com foco no subsistema de memória compartilhada, o qual costuma ser especificado através de um modelo de consistência de memória. o framework deverá incluir múltiplos módulos de geração dirigida de testes (directed test generators), de verificação dinâmica (runtime checkers) e de análise de cobertura (coverage analyzers), além de um simulador associado à representação de projeto do multicore chip sob ve- rificação. três objetivos específicos deverão ser alcançados para viabilizar o objetivo geral: (1) a concepção de novos algoritmos para a geração dirigida de testes, (2) a criação de especificações formais e de novos algoritmos para verificação dinâmica e (3) o desen- volvimento de métricas complementares de cobertura. a originalidade esperada deverá resultar das limitações identificadas em trabalhos correlatos, da adoção de abordagens de machine-learning nunca antes aplicadas ao problema de geração de testes e da concepção de algoritmos originais – orientados a eventos – jamais aplicados ao problema de verificação dinâmica. a metodologia adotada é baseada no reuso de uma infraestrutura em domínio público (para a representação de projeto e simulação), no reuso de módulos pré-existentes, na comparação de cada novo módulo com artefatos congêneres e na avaliação experimental em termos de cobertura (de estados e transições), de eficácia (na detecção de erros de projeto) e no esforço de verificação. a relevância da proposta é amparada no fato de que multicore chips são essenciais para a plataforma de tecnologia de informação, na tendência à heterogeneidade (em socs e microprocessadores) e em indícios de que também a comunicação entre cores heterogêneos tende a adotar memória compartilhada coerente. nesta proposta, o impacto do desenvolvimento tecnológico advém de dois fatos: (1) o projeto de socs é um mercado promissor, diversificado e estratégico; (2) a formação de recursos humanos na aplicação de aprendizado de máquina tem potencial de impacto para além do escopo específico desta proposta. entre os resultados esperados estão a concepção, validação e avaliação comparativa de 3 novos geradores, 4 variantes de um novo checker e 6 métricas de cobertura. a exequibilidade da proposta resulta da massa crítica de artefatos correlatos, acumulada ao longo de 9 anos. por isso, no próximo triênio, espera-se a publicação em veículos da mais alta qualificação na área de cad/eda (pelo menos 2 trabalhos em eventos e 7 artigos em periódicos)