The Formal Man-vs-Machine Showdown
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.
Around the same time Kasparov lost to Deep Blue, Formal technology was adopted in semiconductor design to prove post synthesis logical equivalency between RTL and gates. However, other solutions based on Formal technology were inadequate and lacked ease of use for mainstream designers to solve property verification problems and find bugs early in the design. Today, the leading-edge solutions like Synopsys’ VC Formal, are indeed more intelligent and understand the usage of complex Formal engines to get better out-of-the-box performance and proofs with less human intervention to deliver exhaustive verification.
After Gary Kasparov’s loss in chess to a computer, it took almost twenty years for Google’s DeepMind computer AlphaGo to defeat the global champion Lee Se-dol in the ancient Chinese game of Go in March 2016. This was something that seemed impossible a few years ago. Considering the extreme complexity of Go—there are more potential positions in the game than atoms in the universe—the win was a turning point in the progress of artificial intelligence, according to Demis Hassabis, CEO of Google DeepMind, which developed AlphaGo. This feat was repeated in May 2017, when AlphaGo defeated the current champion Ke Jie of China in the city of Wuzhen.
Google’s team has decided to retire AlphaGo and put their energy into challenges like finding cure for cancer, renewal energy and other important aspects of human endeavor. However, Formal technology has just crossed the chasm and is ready to tackle the world of mainstream verification to go hand in hand with static and dynamic verification.
In June 2017, at Design Automation Conference in Austin, Manish Pandey and Claudionor Coelho presented a tutorial on Machine Learning and Systems for Building the Next Generation EDA Tools. The tutorial described several ways in which machine learning can be applied to solve common optimization and classification problems encountered in the traditional CAD flows, including logic optimization, functional verification, and debug. Stay tuned to the exciting InFormal Chat blogs for more information on using the latest techniques in Formal with advanced engines, machine learning, artificial intelligence and easy to use apps on tackling today’s SoC design and verification challenges.
