Cell implementation through boolean satisfiability for conventional and emerging technologies

Abstract

As ferramentas de apoio ao projeto eletrônico (EDA) desempenham um papel fundamental na síntese de circuitos e sistemas digitais modernos, em que os desafios de projeto envolvidos são numerosos e complexos. Nesse cenário, os resolvedores de satisfatibilidade Booleana (SAT) vêm sendo amplamente empregados nos núcleos de ferramentas de EDA, gerando soluções com boa qualidade em um tempo de computação viável. Dada a versatilidade dessa abordagem, o projeto de circuitos via modelagem SAT pode ser explorado para atender a diferentes propósitos, incluindo o uso tecnologias convencionais e emergentes. Nessa tese utilizamos a modelagem e os resolvedores SAT para o propósito de gerar soluções com otimização em área em três diferentes tecnologias: static CMOS complex gates (SCCG), quantum-dot cellular automata (QCA) e nanomagnetic logic (NML). Para tanto, os métodos propostos apoiam-se na descrição formal das regras de projeto de cada tecnologia, utilizando-se dos resolvedores SAT como protagonistas no processo de síntese. Em relação ao projeto para SCCGs, os experimentos apontam que a abordagem proposta, além de apresentar ganhos em área, também demonstrou-se eficiente considerando outros aspectos geométricos do leiaute como o comprimento de fio utilizado para roteamento (wirelength) e o número de contatos necessários para conectar as partes da célula. Ademais, considerando os experimentos conduzidos para as tecnologias emergentes, tanto a síntese voltada QCA quanto para NML também apresentaram bons resultados quanto à diminuição de área do circuito para boa parte do benchmark utilizado. Por fim, a latência dessas soluções também apresentou otimizações, propiciando um cenário onde o projetista pode escolher qual circuito atende melhor as suas necessidades de acordo com o perfil de área e latência especificados.