Um núcleo inteligente para processamento distribuído de resolvedores SAT em verificação por equivalências

AUTOR(ES)
DATA DE PUBLICAÇÃO

2006

RESUMO

Verificação por Equivalência é um dos componentes chave da metodologia de verificação formal atual para sistemas digitais. Ela é técnica de Verificação Formal mais utilizada atualmente pela indústria para verificação de igualdade entre duas descrições de um circuito. Diversas abordagens baseadas BDDs e SAT obtiveram um considerável sucesso nesta área. No entanto a crescente distância entre a capacidade dos resolvedores atuais e a complexidade das instâncias a serem verificadas motivam a exploração de novas alternativas, em busca de soluções melhores. Esta dissertação apresenta um núcleo inteligente para processamento distribuído de resolvedores SAT em Verificação por Equivalência. Especificamente, o núcleo proposto explora o processamento paralelo de resolvedores SAT e propõe uma nova técnica para a identificação de similaridades estruturais entre os circuitos a serem verificados. Ao final, são apresentados resultados que comprovam a eficiência da metodologia proposta.

ASSUNTO(S)

circuitos integrados verificação teses processamento eletrônico de dados processamento distribuído teses. circuitos eletronicos projetos processamento de dados teses computação teses.

ACESSO AO ARTIGO

Documentos Relacionados