Seven Ways That Formal Verification is Like a Team Sport
I recently started to develop an appreciation for the sport of cricket during our Oski company-wide, off-site meeting in beautiful Udaipur, India. Before that, if you had mentioned cricket, I would be more likely to think of the bugs I hear chirping on summer nights and that sometimes find their way into my garage.
John Wright presents to Oski employees.
However, that began to change on January 26, 2017, when Oski employees were treated to a talk by legendary cricket player and coach, John Wright. Wright was propelled to stardom when he enjoyed a successful 5-year stint as the first foreign coach of the Indian national team between 2000 and 2005. With the support of Indian captain, Sourav Ganguly , he transformed the Indian cricket team from a group of super-talented individuals, but under-achievers as a team, to consistent world champions. Highlights included beating the Australian juggernaut, who were on a run of sixteen consecutive test wins, and beating Pakistan on their home turf for the first time in more than 50 years.
Interestingly, it was not through a new team system nor by adding new individual skills that this was accomplished. As an outsider, he succeeded against all odds by a series of small, thoughtful behavioral changes. Let’s examine these changes and the lessons we can learn from them as formal verification engineers.
John Wright answers questions after his talk.
- Team First
“Don’t do anything to hurt the team”, says Wright. A winning team must have good chemistry. They must portray an image of being the model team. That means individuals must prioritize the team’s schedule and not keep everyone else waiting. It means warming up as a team before games; treating each other with respect; having a positive attitude, while not being afraid to deal with the negative. This is the responsibility of all team players, but the tone is set by the leaders, starting with the team captain and coach.
Application: Formal verification expertise across the industry is still developing. Talented team players are in short supply. The role of the formal program leader is an emerging one, but if done right, it can lead an entire organization to build an effective formal verification capability.
- Hard Work
According to Wright, “there aren’t any lazy, successful people.” He doesn’t tolerate lazy players. Everyone must pitch in and help the team meet its goals, even if it means that superstars carry their own equipment so the practice can start on time. Keep the flair, but work hard also.
Application: Successful formal deployment requires a lot of hard work, and it includes some less glamorous jobs, such as iteratively debugging to refine constraints, closing coverage holes and setting up regressions.
Performing at a world class level on a regular basis doesn’t come easy. Coach Wright likes a competitive style of practice, where skills are kept sharp by training with game level intensity all the time.
Application: Doing formal part-time is not easy. It requires specialized skills that must be honed and kept sharp through continuous use. It’s best if engineers are dedicated to formal full-time.
Wright found the team’s fitness to be lacking. He introduced team fitness goals, including for the number of workout sessions per week. He brought in a fitness trainer.
Application: Staying fit is akin to staying current with industry trends and best practices. Attending conferences and user group meetings, reading books and technical papers, signing up for a training class. These are all ways that help build our core abilities.
During the game, the players didn’t communicate with each other enough. Wright instituted a system of communication that they practiced until it became second nature.
Application: Have a process in place with clear deliverables so everyone knows how and when they are supposed to communicate information to the rest of the team. Use standard templates for documents such as the test plan and the sign-off criteria.
Willingness to change is key. “`This is just the way I play’, is not an acceptable attitude”, says Wright. The team needs results. Players have to be flexible, always looking to improve.
Application: Every successful formal engineer will tell you about the importance of staying humble. There is always some new technique to learn.
Coach Wright’s number one rule of team sports is, “Be honest”. If there are any problems, speak up so they can be dealt with.
Application: When contrasting formal with simulation, I’ve heard some say “No testbench required!”. That’s not correct. It is true that we don’t have to explicitly define the stimulus the same way that it is done in simulation. But, enough time needs to be allocated in the schedule to write the checkers, develop the constraints and overcome proof complexity with abstractions, if required.
Selfies with John Wright
As we strive to be among the best in the world in formal verification, it’s helpful to look at what worked for a winner in team sports. Searching for and embracing some of the lessons learnt from the stories of John Wright will help all of us in our development towards that goal.