Introduction to Hardware Verification

Modern world can not be imagined without a huge variety of electronic devices. Mobile phones, digital cameras and briefcase computers have become the integral parts of human life. Special devices manage household appliances, control airplanes and space satellites, regulate medical systems of life support. Practically all of such systems are based on digital semiconductor hardware.

To make sure that hardware works correctly, i.e. meets all functional requirements stipulated in documentation, functional verification is used. Requirements on thoroughness of hardware design verification are very strong. This is not only connected with the fact that hardware underlies all computer systems including safety-critical ones.

In contrast to software, where an error correction does not cost anything, a post-silicon error in hardware can cause reproduction of all erroneous devices. The well-known FDIV bug in Pentium microprocessor consisted in incorrect division of some floating-point numbers cost Intel about 475 millions dollars. Time constraints of testing are also very strong. It is crucially important to develop system in time while it is much in demand.

Currently, high-level hardware description languages (HDLs) are widely used in electronic design. The HDLs greatly speed up a development process by automated synthesis of a register-transfer-level (RTL) description into a gate-level netlist. However, they can not guarantee that system developed is faultless. Thus, a verification does remain an acute and very important task.

It is well known that functional verification is a major bottleneck in hardware design. According to Janick Bergeron, ensuring the functional correctness of hardware consumes about 70% of the design efforts; the number of verification engineers is usually twice the number of RTL designers; the code that implements the testbenches makes up to 80% of the total code volume. The situation is only going to get worse as hardware designs grow in size and complexity.

Two main approaches to ensure functional correctness of hardware designs are based on formal verification and simulation techniques. It is known that formal verification techniques are exhaustive but do not scale well; simulation-based techniques are scalable but are not exhaustive. Possible compromise is provided by so-called semi-formal or hybrid approaches combining formal specifications, test coverage definition, and simulation.

Our approaches to verification are based on simulation, but they use formal specifications and formal models to automate checking of design correctness and generation of test sequences. The methodology provides a good balance of exhaustiveness and scalability.