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:

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.