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

Abstract

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.