ABSTRACT
The state-of-the-art formal property verification engines can handle models in the order of 10 K memory elements and with complementary automatic model reduction techniques properties are verified on hardware designs and software programs with 100 to 500 K memory elements. Formal property verification provides a means of ensuring that a hardware or software system satisfies certain key properties, regardless of the input presented. In hardware design, formal property verification is used throughout the design cycle. In the hardware electronic industry, tools for formal property verification have been developed since the early 1990s in internal Computer-aided design groups of big very Large Scale Integrated Circuit companies like Intel, IBM, Motorola, Siemens, and Bell-labs. Modern property specification languages used in electronic design automation (EDA) provide some additional features that are convenient for hardware specifications. The large EDA companies are also offering products for formal property verification.
