It is commonly believed that Formal property verification is the realm of PhDs and experts with many years of experience and have the magical solution and intellect to solve complex verification problems. I see the application of Formal verification solutions solving design bugs very much like the way supercomputers and artificial intelligence have evolved to beat human intellect and eventually become mainstream. In 1997, Gary Kasparov the chess Grand Master lost to IBM’s Deep Blue supercomputer. Kasparov and other chess masters blamed the defeat on a single move made by the IBM machine, where the computer made a sacrifice that seemed to hint at its long-term strategy. Kasparov thought the move was too sophisticated for a computer and got side tracked. Indeed, fifteen years later, the designers of Deep Blue acknowledged and attributed Gary’s loss to a software bug in Deep Blue that misled him. Either way, this was a lesson that as humans, we tend to blow things way out of proportion and could sometimes make wrong assumptions.
Posted in Automation