Formal verification techniques: industrial status and perspectives

Research in applied formal verification has become a hot topic in circuit and system design due to rising circuit complexity. Design verification presents the biggest bottleneck in digital hardware design. Major hardware bugs found in ASIC design may cause expensive project delays when they are discovered during system test on the real silicon chip. The consequences are severe, from cost overruns to lost market opportunity. Simulation and emulation tools, which are traditionally used to find bugs in a design, often cannot find the corner cases or hard-to-find bugs that may occur only after hundreds of thousands of cycles, and are well beyond the reach of conventional simulation and emulation technologies. Formal methods have emerged as an alternative approach to ensure the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing.