Aumentando a eficiência da verificação dinâmica de propriedades em sistemas descritos em alto nível de abstração por meio da utilização de funções de classificação heurística derivadas das propriedades do sistema

• Main Author: Alair Dias Junior
• Other Authors: Diogenes Cecilio da Silva Junior
• Format: Others
• Language: Portuguese
• Published: Universidade Federal de Minas Gerais 2012
• Online Access: http://hdl.handle.net/1843/BUOS-95GRM9

=== Over the last decade, the integrated circuit (IC) production ow has gradually shifted from design centric to verification centric, as the design methodologies, tools and techniques evolved. It is a well known fact that on the modern IC design cycle more than 70% of the total development resources are spent on verification. In recent years, several techniques have been proposed to address this issue. Among them, assertion-based verification has been regarded as the most promising approach. However, current assertion-based verification methods for high-level designs either heavily depend on the internal structure of the model, requiring the entire source code to be available during the verification, or completely ignore the system, disregarding important information that can be derived from its behaviour. The method proposed in this work conjoins the assertions with the black-box model of the system in order to derive heuristic functions that can be used by an optimization algorithm to generate counterexamples of the design properties. Differently from other dynamic property checking approaches, the method does not focus on increasing the coverage of the test set, but iteratively searches for property violations. Experiments show that our method is orders of magnitude more time eficient in nding property violations than random simulation. === A evolução das técnicas de projeto de circuitos integrados ocorrida nas duas últimas décadas permitiu um aumento expressivo na produtividade das equipes de projeto. O gap de produtividade, que foi durante muito tempo o principal obstáculo a ser vencido pela indústria de microeletrônica, deixou de ser o foco das atenções e o ciclo de desenvolvi-mento se deslocou de uma abordagem centrada no projeto para uma abordagem centrada na verificação. Hoje, mais de 70% dos recursos de um projeto de CI são gastos com a verificação. Diversas técnicas foram propostas para aumentar a e ciência e a eficácia do processo de verificação, entre elas, a verificação baseada em asserções tem ganhado uma posição de destaque. No entanto, métodos atuais de verificação baseada em asserções para descrições de alto nível de abstração dependem fortemente da estrutura interna do modelo, necessitando que todo o seu código fonte esteja disponível durante a verificação, ou ignoram completamente o sistema, não levando em conta informações importantes que podem ser inferidas a partir do seu comportamento. O método proposto neste traba-lho combina as asserções com o modelo caixa-preta do sistema sob verificação de forma a criar funções heurísticas que podem ser utilizadas, juntamente com um algoritmo de otimização numérica, para gerar contraexemplos das propriedades do sistema. Diferen-temente de outras abordagens de verificação dinâmica de propriedades, o método não se foca em aumentar a cobertura do conjunto de testes, mas realiza uma busca iterativa por vetores que violam a propriedade sob verificação, acelerando a busca por contraexemplos. Resultados experimentais mostram que a busca por contraexemplos utilizando o método proposto é ordens de magnitude mais e ciente em relação ao tempo do que averificação baseada em vetores aleatôrios.