This document describes a successful application of a semi-formal test generation technique to the verification of 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, 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.
展开▼
