Semi-formal test generation and resolving a temporal abstraction problem in practice: industrial application

This document describes a successful application of a semi-formal test generation technique to the verification of the direct memory access controller (DMAC) of ST50, a new general purpose RISC microprocessor developed by STMicroelectronics and Hitachi. Like other memory-related devices, the DMA controller challenges formal techniques because of the state explosion problem. To cope with the challenge, an abstraction mechanism is applied during test generation: several abstract models are created in order to verify different functional aspects of the design. We also propose a practical solution to overcome a temporal abstraction problem that arises when tests issued from an abstract model have to be applied during real design simulation.