Parallel algorithms for scalable logic synthesis & verification

Abstract

The design of digital integrated circuits relies on gradually compiling a circuit specified by hardware description language into its physical implementation layout. Such a design flow is strongly dependent of a tool chain known as electronic design automation (EDA) tools. Currently, the high complexity of system-on-chips and the increasing demand for hardware accelerators are imposing new challenges on the EDA field. Parallel computing is a trend to enhance scalability of EDA tools using widely available multicore platforms. In order to benefit from parallelism, well-known EDA algorithms have to be reformulated and optimized for massive parallel environments. This work aims to enable parallelism during logic synthesis and verification phases of EDA flow, in order to significantly improve runtime while handling very large designs. We are rethinking algorithms such as multi-level logic optimization, technology mapping and combinational equivalence checking (CEC) to achieve extensive parallelism. Such algorithms are strongly correlated to each other in the design flow and work on directed-acyclic graphs called AIGs (ANDinverter graphs), which are irregular and sparse structures. The time spent for synthesis and verification of large design comprising millions of AIG nodes is becoming more critical, requiring several hour for synthesis and even more than a day for verification. Therefore, we are proposing a parallel flow based on a fine-grain parallel AIG rewriting method for multi-level logic optimization and a fine-grain parallel LUT-based technology mapping that enable fast solutions with competitive quality-of-results (QoR). Moreover, we are exploiting data sharing and data independence to enable parallelism in a modern CEC engine for faster verification. Experimental results have demonstrated that the proposed parallel methods are able to accelerate the design flow when compared to the ABC tool, which is an industrial-strength academic tool comprising state-of-the-art algorithms for logic synthesis and verification. When optimizing designs comprising millions of AIG nodes and running at 40 processor cores, the proposed parallel methods for AIG rewriting and technology mapping are up to 36x and 25x faster than the respective ABC commands rewrite and &if , with similar QoR. The proposed parallel CEC is able to significantly reduce the verification runtime when compared to the ABC CEC engine and to a commercial verification tool. For example, we observed some expressive improvements where the CEC runtime went down from 19h to only 18min, representing a speedup of 63x.

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.