O Departamento de Ciência da Computação (DCC) da UFMG, em parceria com a Cadence Brasil, ofereceu, no segundo semestre de 2024, a disciplina optativa “Verificação formal de hardware”. Valendo dois créditos e com um total de 30 horas, foi aberta aos alunos dos cursos de Ciência da Computação, Sistemas de Informação, Ciência de Dados e Matemática Computacional, além dos alunos da pós-graduação em Ciência da Computação da UFMG. Já os demais alunos da UFMG, puderam se matricular como disciplina eletiva ou isolada.
A ideia de oferecer a disciplina partiu da Cadence, parceira do departamento por meio do Laboratório de Computadores já há algum tempo. “Essa parceria surgiu no contexto de um projeto de pesquisa que a Cadence Design Systems desenvolve com o Laboratório de Compiladores do DCC/UFMG. O projeto financia alunos de iniciação científica e mestrado, com o objetivo de desenvolver uma ferramenta que gere código Verilog. Essa ferramenta, o ChiGen (https://github.com/lac-dcc/chimera), está sendo usada para encontrar bugs em ferramentas de EDA. Temos tido bastante sucesso nesse sentido: já identificamos bugs em várias ferramentas populares, como o Yosys, o Verilator e o Verible”, explicou o professor do DCC e coordenador do laboratório, Fernando Magno Quintão Pereira.
O objetivo da disciplina é mostrar aos alunos como técnicas de verificação de hardware são aplicadas na prática. Eles terão contato com lógica formal e verificação de modelos, além de linguagens de descrição de hardware, como Verilog e VHDL. “Um aspecto que considero muito valioso é a oportunidade de os alunos verem, neste curso, como ferramentas de verificação e simulação, como o Jasper e o Xcelium, são usadas para resolver problemas reais da indústria de hardware”, esclareceu Fernando.
Segundo o professor, a grade da disciplina foi proposta pelos profissionais da Cadence. Muitos deles, inclusive, possuem experiência em pesquisa e ensino. “A Mirlaine Crepalde, gerente de Engenharia de Software da empresa, por exemplo, é mestre em Ciência da Computação pelo Programa de Pós-graduação em Ciência da Computação (PPGCC) da UFMG, e o Augusto Mafra está em vias de obter o mesmo título, na área de verificação de software. Acredito que devemos a existência dessa disciplina à boa vontade dos profissionais da empresa, que se dispuseram a ministrá-la, e à gerência, que permitiu que isso acontecesse. Nesse sentido, temos que agradecer especialmente à Mirlaine por ter organizado a disciplina, e ao Fabiano Peixoto, diretor de Pesquisa e Desenvolvimento da Cadence Brasil, por autorizar seus profissionais a dedicarem tempo à preparação e oferta da disciplina”, contou.
De acordo com o Fernando, tanto ele quanto os outros colegas do departamento desejam que a disciplina seja oferecida nos demais semestres. “Eu e meus colegas do departamento ficaríamos muito felizes se a disciplina pudesse ser oferecida regularmente. No entanto, sabemos que isso não é simples: a oferta da disciplina envolve muito preparo e uma grande dedicação de tempo. Até mesmo a logística é complicada, uma vez que o curso é 100% presencial. Então, o que posso dizer é que os profissionais da Cadence serão sempre bem-vindos a continuar oferecendo a disciplina em nosso departamento, mas entendemos perfeitamente as dificuldades que isso implica”, falou.
Para o professor, interações como estas são de grande valia não só para os alunos, mas também para as empresas. “Seria excelente termos cursos semelhantes oferecidos por outras empresas. Isso nem precisa ser restrito ao DCC. Imagine o que profissionais da Fiat, Gerdau, Petrobras e Vale, por exemplo, poderiam oferecer nas Engenharias Mecânica, Elétrica, Metalúrgica, etc. Temos muitas indústrias de ponta no Brasil: laboratórios farmacêuticos, centros de desenvolvimento de software, empresas mineradoras, entre outros. Todas elas geram conhecimento que seria extremamente útil para os profissionais que a universidade federal se propõe a formar. Tenho certeza de que os profissionais dessas empresas serão muito bem recebidos na UFMG, caso desejem compartilhar esse conhecimento com nossos alunos”, concluiu.
Também para a professora e chefe do DCC, Raquel Prates, esta iniciativa é muito enriquecedora tanto para os alunos quanto para as empresas. “A oferta dessa disciplina foi uma oportunidade de estreitarmos os laços entre a academia e o mercado, criando uma ponte com resultados positivos para ambos os lados. Agradecemos à Cadence pela disponibilidade e esperamos poder contar outras vezes com esta parceria”, afirmou.
