Parallel algorithms for scalable logic synthesis & verification

• Ano de defesa: 2019
• Autor(a) principal: Possani, Vinícius Neves
• Orientador(a): Reis, Andre Inacio
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Palavras-chave em Português: Microeletrônica; Circuitos digitais; Processamento paralelo
• Palavras-chave em Inglês: AIG rewriting; Tech mapping; Equivalence checking
• Link de acesso: http://hdl.handle.net/10183/195698

O projeto de circuitos integrados digitais consiste em gradualmente compilar um circuito especificado em uma linguagem de descrição de hardware em seu leiaute de implementação física. Este fluxo de projeto é fortemente dependente de uma cadeia de ferramentas conhecidas como ferramentas de automação de projetos eletrônicos (do inglês EDA). Atualmente, a alta complexidade de sistemas integrados em um chip e a crescente demanda por aceleradores de hardware estão impondo novos desafios no campo de EDA. Computação paralela é uma tendência para aumentar a escalabilidade de ferramentas de EDA usando plataformas multicore. Com o objetivo de usufruir do paralelismo, algoritmos de EDA bem estabelecidos precisam ser reformulados. O objetivo deste trabalho é viabilizar o paralelismo durante a fase de síntese lógica e verificação do fluxo de EDA, a fim de melhor o tempo de execuç ao manipular circuitos grandes. Neste trabalho, algoritmos para otimização lógica multi-nível, mapeamento tecnológico e checagem de equivalência combinacional (CEC) estão sendo repensados para viabilizar paralelismo massivo. Tais algoritmos estão correlacionados e operam sobre grafos acíclicos direcionados chamados AIGs (AND-inverter graphs), os quais são estruturas irregular e esparsas. O tempo gasto durante a síntese e verificação de grandes projetos com milhões de nodos e AIG está se tornando mais crítico, requerendo horas para a síntese e até mesmo mais de um dia para a verificação. Este trabalho propõe um fluxo paralelo baseado reescrita de AIG e mapeamento tecnológico baseado em LUTs, ambos com um grão fino de paralelismo, os quais viabilizam resultados rápidos sem sacrificar a qualidade dos resultados. Além disso, este trabalho explora compartilhamento de dados e independência de dados para habilitar paralelismo em um módulo moderno de CEC, permitindo a verificação mais rápida de circuitos grandes. Resultados experimentais demonstram que os métodos paralelos propostos têm potencial para acelerar o fluxo de projeto quando comparado a ferramenta ABC, a qual é uma ferramenta acadêmica com capacidade industrial para síntese lógica e verificação. Quando aplicados a circuitos compostos por milhões de nodos de AIG e executados em 40 núcleos de processamento, os métodos paralelos propostos para reescrita de AIG e mapeamento tecnológico são até 36x e 25x mais rápida do que o os respectivos comandos rewrite e &if da ferramenta ABC, com qualidade de resultados similares. O método proposto para CEC paralelo é capaz de reduzir significativamente o tempo de verificação comparado ao método de CEC da ferramenta ABC e a uma ferramenta comercial de verificação. Por exemplo, foram observados melhorias expressivas onde o tempo de execução foi reduzido de 19h para apenas 18min, representando uma aceleração de 63x.