Automatic verification of RT-level microprocessor cores using behavioral specifications: a case study

International audienceThe massive diffusion of custom system-on-a-chipand the growing obsolescence problems pushes the need for fast, automatic and reliable verification mechanisms. The paper shows an automatic methodology for verifying the correctness of a microprocessor core by generating appropriate test program and comparing the behavior of the model with a reference. The methodology exploits the RT-level design to drive the search process, and the reference as a mere black box. Therefore, it can be used whenever a new core is obtained by modifying an obsolete one and only little information are available on the original design. As a case study a customized 68hc11 is examined and experimental results show the effectiveness of the proposed approach