Projeto digital de células via satisfatibilidade booleana em tecnologias convencionais e emergentes

Submitted by Aline Batista (alinehb.ufpel@gmail.com) on 2022-05-20T14:01:08Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Tese_Maicon_Cardoso.pdf: 14617294 bytes, checksum: 2b484066343da535e2acc22d0b408744 (MD5) Approved for entry into archive by Aline Batista (alinehb.ufpel@gmail.com) on 2022-05-20T14:24:58Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Tese_Maicon_Cardoso.pdf: 14617294 bytes, checksum: 2b484066343da535e2acc22d0b408744 (MD5) Made available in DSpace on 2022-05-20T14:24:58Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Tese_Maicon_Cardoso.pdf: 14617294 bytes, checksum: 2b484066343da535e2acc22d0b408744 (MD5) Previous issue date: 2022-02-15 Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES The electronic design automation (EDA) tools take a crucial role in the modern digital circuits and systems synthesis, where the design challenges are not only numerous but also complex. In this scenario, the Boolean satisfiability (SAT) solvers have been employed lately as a useful engine for computing the solutions on these EDA tools, producing circuits with good quality in a reasonable computing time. On a similar note, the versatility provided by the satisfiability paradigm can be explored for different design purposes ranging from conventional to emerging technologies. Thus, in this thesis, we employ this approach to generate area-optimized circuits in three different technologies: static CMOS complex gates (SCCG), quantum-dot cellular automata (QCA), and nanomagnetic logic (NML). Considering this, the proposed methods were able to encode all the design constraints into a discrete constraint model, using satisfiability solvers as the core of the optimization task. Regarding the SCCG synthesis, the experiments have shown that, besides providing improvements on layout area, the solutions produced using the proposed method also presented optimization in other geometrical parameters such as in wirelength and number of contacts when compared to a traditional meta-heuristic approach. Furthermore, following the experiments on the emerging technologies, the QCA and NML synthesis methodologies were able to provide solutions with less area when compared to other graph-based techniques available in the literature for most of the assessed cases. Moreover, the latency of these solutions also presented an optimization, thus providing a wide design exploration scenario where it is possible to choose whether to use smaller or faster circuits depending on the specifications. 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.