Cost-efficient block verification for a UMTS up-link chip-rate coprocessor

ASIC designs for future communication applications cannot be simulated exhaustively. Formal property checking is a powerful technology to overcome the limitations of current functional verification approaches. The paper reports on a large-scale experiment employing the CVE property checker for verifying the block-level functional correctness of a large ASIC. This new verification methodology achieves substantial quality and productivity gains. The two biggest advantages are: 1) coding and verification can be done in parallel; and 2) the whole state space of a test case will be verified in a single run. Formal property checking simplifies and shortens the functional verification of large-scale ASICs at least in the same order of magnitude as static timing analysis did for timing verification.