ABSTRACT
Formal property verification enjoys major advantages over simulation. It offers an exhaustive verification technology, which is orders of magnitude more efficient than scalar exhaustive simulation. Both hardware and software designs are experiencing a verification crisis since simulation-based logic verification is becoming less and less effective due to the growing complexity of the systems. The main deficiency of formal verification is its limited capacity compared with simulation. In a formal verification approach, a single symbolic simulation run provides full coverage of the input space and thus exhaustively verifies the program. In hardware design, formal property verification is used throughout the design cycle. Formal property verification of the register-transfer level was mostly carried out by validation teams around the early 2000s. In the early 2000s, formal property verification of software just started to move into the industry—most promising results were reported by the research team in Microsoft, verifying Windows NT drivers.
