Between nature and nurture, it’s difficult to say what plays a more important part in a person’s life. For me, I was fortunate to reap the benefits of both. I grew up in Allahabad and belong to the third generation of engineers and scientists in one of the well-known twenty-one royal families of India—the Darbari family—and the family pedigree more or less guaranteed that I was destined for a life devoted to the sciences. I had no inkling back then, however, that my career path would lead me to Intel, ARM, Imagination, and eventually OneSpin, where I am today. How, then, did I go from being a kid in India to a formal verification fanatic? The truth is, I had a long way to go—and so did formal.

Playing at Computing

Computers were not a novelty in family. My dad runs a family business in mechanical, electrical, and electronics manufacturing. It was founded by my late grandfather in the 1920s, and among the many things that he designed and built were the first pontoons for Allahabad’s floating bridge over the Ganges and Yamuna rivers. Some of the first electrical computing machines were built by my late uncle, who also designed one of the first analog and digital computers in India in the early 1960s. These were used in several universities in India for teaching digital electronics.

My first interaction with computers happened when I was about 11 years old. We had a Color Genie at home. As you can imagine, my excitement knew no bounds as I played my first computer video game—never mind that it would take up to 45 minutes to boot the operating system out of a cassette. It was not long before we had the first x86 machines at home with floppy disks booting the DOS operating system. We were decidedly sharing the computing excitement of the mid-‘80s. It was not until the early ‘90s, however, when my mom got addicted to computing and started to learn programming in Cobol, Fortran, and Basic, that I started to get interested in computing beyond video games.

My hometown of Allahabad afforded me the opportunity to attend St. Joseph’s College, a top school, where I began exploring career choices. It was typical in India at the time that if you didn’t pursue an engineering or medical degree, then there must be something wrong with you. In my case, I had enjoyed the luxury of having engineering bites of different flavours at home, so the most challenging question was not whether or not I wanted to study engineering, but whether I could obtain a place at a decent engineering school. The grand litmus test in India is to pass the All India Engineering Entrance Examination (AIEEE), now called the Joint Entrance Examination (Main), to obtain a place with the top programs. I qualified for a place to study electrical and electronics engineering at Birla Institute of Technology, Mesra.

A University or Two … or Five

Birla Institute of Technology’s program was fairly heavy in electrical control and power systems, but we had our fair share of electronics and computing in the four-year course, including programming in Pascal, Fortan, C, and x86 assembly. My path took a more definite turn towards computing when I started working on a project to design a power-frequency controller based on fuzzy logic and artificial intelligence. We were tasked with researching a new technique to find voltage and current correlations on a heavily-loaded electrical system, to find variance and perform fuzzy set classification for fast decision making for load-shedding, thereby providing timely power frequency correction and prevention of electrical turbine failure. As it turns out, our study revealed a negative result. There was no strong evidence to suggest that V-I variance was a good predictor; in fact, the best one was df/dt-based prediction and control.

We were rewarded for our work and I became acquainted with the brighter side of research—it is the process that counts and the honesty of investigation that matters, and negative results are not necessarily bad. This project drew me closer to the subject of artificial intelligence and was the impetus for studying AI for my master’s degree. This is not to say that I had an easy road ahead of me; transitioning from electrical and electronics to a major in computing is not as easy as it appears, and it took me some time to figure out how to make it happen.

I pursued my master’s in computational logic at TU Dresden, Germany. The course was designed to focus on the basics of formal methods, formal logic, and their applications to real world problems. The two-year course was fairly heavy in several aspects of theoretical computer science, and for someone who did not hold a CS degree, it was a significant challenge. Were it not for the helpful instructors who were happy to spend time clarifying concepts and providing tips to help me get on top of the advanced courses, I don’t believe I would have made it. I manged to complete my Diplom (Master’s) with a German 1.7 (‘good’), and my thesis was awarded a 1.1 (‘excellent’). I was indeed very proud of myself and discovered a new aspect of learning: we can learn whatever we want, even if it feels alien in the beginning.

I received several PhD offers after my master’s, most in machine learning. Only one offer was in an area of formal verification, and I ultimately selected it for two reasons. First, it made perfect sense for me to amalgamate my fields of undergraduate and graduate study by applying formal methods to hardware design verification. Second, Professor Tom Melham of Glasgow University, who offered me the PhD opportunity in formal, was a well-known figure in the field. He also had a donation from Intel to pursue my research, and it’s very hard to say no to a full scholarship!

In the second year of my PhD, Tom Melham was offered a position at Oxford University, so I moved with him to Oxford. My studies continued to progress, though the transfer meant that I was instead working toward a DPhil, Oxford’s equivalent of a PhD. I was fortunate to have an opportunity to work not only with Tom, but also with some of the finest minds in formal verification at Intel’s Strategic CAD Labs (SCL) in Oregon, USA. At the time, symbolic model checking was making big news due to Kenneth McMillan’s work and Randall Bryant’s invention of BDDs. Intel’s SCL was the powerhouse in high-end innovation of formal solutions. Unfortunately, this was a little late to have prevented the famous Intel FDIV bug in 1994, which had surfaced a few years before SCL was founded.

My DPhil work was closely tied to one of the hardest problems then and even today: complexity reduction for large-scale model checking. In simple terms, this is an investigation of how we can verify huge hardware designs, in a reasonable timeframe, with comprehensive rigor, and find the bugs before the hardware ends up being fabricated in silicon, when it is too late (or incredibly costly) to make corrections. I used symbolic trajectory evaluation (STE) model checking and devised a framework for detecting symmetries in hardware as a basis for complexity reduction. I designed a polynomial time type checking-based solution to detect symmetries in circuits used to reduce state-space search during STE model checking. This enabled a more expedient and scalable method of finding bugs and building exhaustive proofs.

My work in this area took me closer to mastering some of the hardest, but also the most satisfying, aspects of formal: theorem proving with LCF-style theorem provers, such as the higher-order logic (HOL) family. Using a combination of theorem proving and model checking, I saw how the best of both the worlds could be combined to provide some very powerful solutions for scalable and rigorous verification of hardware designs. All told, I got to spend six months with Intel SCL during my doctoral research, which provided me with unique insights into a world that one cannot appreciate solely through university study—even if that university is Oxford! There is no substitute for practical experience in the industry.

After my DPhil was complete, I found myself with the option of transitioning into the industry or pursuing further academic research. Professor Bashir Al Hashimi at the University of Southampton had a research grant to investigate the effects of single-event upsets on designs that undergo dynamic scaling of voltage and frequency. This project was in collaboration with ARM in Cambridge, England, and the problem required a line of investigation slightly outside traditional methods. Bashir and I talked it over, and I decided to take advantage of the opportunity. For about three years, I worked with him on this topic and devised formal-based fault injection techniques, which are massively more efficient when compared to traditional fault injection methods. I also had the good fortune to work with two other luminaries from ARM, John Biggs and David Flynn, with whom I worked on developing a method for estimating empirically how much selective state retention needs to be built in for CPUs. The main finding of our study was that the programmer-visible state or the architectural state of the CPU needs to be implemented using retention registers, while other micro-architectural enhancements, such as pipeline registers, TLBs, and caches, can be implemented using normal registers without retention. This has a profound impact on power and area savings for chip design.

I was nearing the end of my project with Bashir when I was contacted by Professor Joao Marques Silva, one of the best-known names in the field of SAT solvers. He had a very interesting problem centred on designing certified SAT solvers.

Now, SAT solvers themselves have been around for nearly four decades, and in the last fifteen years or so, they’ve been instrumental in increasing the performance of formal solvers and in driving the adoption of formal tools. As with most things that are algorithm-based, they can have bugs. In this case, however, the ramifications can be quite severe, as a buggy SAT solver is likely to produce an incorrect outcome when used in a formal tool, thereby creating catastrophic outcomes for the end user. This is especially problematic—and potentially dangerous—if that formal tool is used in the verification of safety-critical systems.

Joao explained that there had been some prior work done on designing SAT proof checkers that were able to validate the outcome of a SAT solver to provide higher assurance. To complicate matters, these proof checkers themselves can have bugs, hence you need an even higher degree of assurance. This can only be provided by generating a SAT proof checker that has been designed correct-by-construction, and that correctness must be guaranteed by a mechanically-reproducible mathematical proof in a theorem prover. I used the Coq theorem prover to build such a certified SAT proof checker and extracted a high-performance OCaml binary that could execute at comparable speeds to a C-based implementation of an uncertified SAT proof checker. Interestingly, during the course of our research, we also happened to discover a corner case bug in a famous SAT proof checker. It just goes to show that in the sciences, there is always room for improvement!

Moving into the Industry (and All Over the World)

After four years at Southampton University as a postdoc, I realized that I had spent nearly sixteen years in academia, and perhaps it was time I switched to industry to experience the other side. I joined ARM in Cambridge, England as a verification engineer and started to see where the industry was in terms of using formal. Given that I had seen formal in action at Intel, my assumption was that ARM would be using formal extensively as well. It turned out that I was not entirely correct. At the time, ARM’s was using formal on only a few projects and the management was generally not very open to resourcing for formal verification. Despite this, I was given the opportunity to work on multiple projects to show how formal verification can produce a higher quality of rigor and find more bugs, thus saving management valuable time and cost. My stay at ARM was relatively short—about eighteen months—but I worked on a couple of very interesting projects: one on lock-step verification of an R-class CPU and another on verifying a cache-coherency block using formal. I was also instrumental in developing the first formal verification roadmap for ARM.

In 2011, my wife accepted a job as a lecturer at the Indian Institute of Science Bangalore, so after thirteen years in Europe and the West, I found myself moving back to India. I joined General Motors’ India Science Lab, which I would call one of the best R&D labs for formal rigorous control software verification. Just when I was hitting my stride professionally, GM announced in 2012 that the India Science Lab would close its doors in two months’ time. Almost 90 researchers, mostly with PhDs, were left in search of a new home. My three new patent applications would never see the light of the day. Given that I wasn’t having the best time dealing with Bangalore’s infrastructural growing pains, we decided to move back to Europe. The question was: where?

I reminded myself that, since 1993, I had lived, studied, and travelled in five different countries on three different continents. Life sometimes moves faster than you can grasp. I had only two months to get a new job and fortunately found one before too long. In 2012, I joined the team at Imagination Technologies in North London, UK, to work on building a consistent formal verification story that could show some real value-add on the ground.

I was hired into the PowerVR business unit initially, but three months into my job, my boss, Colin Mckellar, and I moved to a central team to serve the business needs of the wider company. Verification was one of the topics which fell in Colin’s remit, and I was given the chance to steer a consistent roadmap for formal verification deployment. There was no plan in place whatsoever, so I was given the freedom to dream and execute whatever made sense for Imagination—an opportunity not many people get. I formed a methodology group called Advanced Verification Methodology (AVM) in January 2013 and hired three people who directly reported to me, along with one additional engineer who reported to Colin and was responsible for UVM adoption.

Within three years of starting the AVM group, my three-person team and I had trained nearly 100 engineers in Imagination across most business units in Asia, Europe, and North America, and had delivered on more than 50 projects to teams spread over Australia, India, the UK, and the USA. I ensured that my team was not only the best in formal verification at Imagination, but also that it should stand out as one of the best anywhere in the world. To achieve this, it was important to establish a culture of thought leadership, innovation, and peer-reviewed publications. I filed fifteen patents in three years, and was lucky to have had seven issued in the UK and three issued in the US. We published numerous papers in conferences and industrial forums and gave countless keynote talks.

In 2015, I was appointed a Royal Academy of Engineering Visiting Professor for three years in the Electronics and Computer Science Department at the University of Southampton, UK. I got a chance to interact with the students on a regular basis and to share my excitement and experience of formal in the industry. I continue to be delighted to have this opportunity, as it gives me a chance to give back something to the institutions that supported me.

At the time, Imagination Technologies was enjoying a great phase—or so we thought. We came to know in February 2016 that the business’s finances were not looking good and a big shakeup was imminent. I started to lose members of my team as part of the large-scale exodus of employees. Sadly, morale was dropping even more sharply than our numbers. I knew that it was time, once again, to check my compass and reevaluate my path.

The Future is Formal

By October 2016, after four years with Imagination, I took the plunge and moved to the EDA industry. As I began to prospect, it turned out that one of the best companies in the verification market, OneSpin Solutions, was looking for new people. I joined the team as director of product management to shape the next steps in technology at OneSpin. Six months in, I can say with confidence that this has been a terrific opportunity for me. Given that I am a longstanding user of different formal tools, I have found it fascinating to swap roles and see the other side: how tools are made, why they work, and what makes one exceptional. I thought life at Imagination moved fast, but at OneSpin, a company that is still lean enough to be agile and dynamic, it is orders of magnitude faster—and therefore more fun!

I’ve been globetrotting for the last 25 years. Having lived, studied, and worked in twelve cities, in five different countries, spread over three continents, I now live in North London with my wife and son. I have the pleasure of working for the only company in the world that is solely focused on formal verification. I make regular trips to our headquarters in Munich, Germany, and enjoy the opportunity to travel the world and share my passion for formal. I very much look forward to establishing the Doctor Formal blog as a forum for everyone—from formal verification novices, all the way up to expert-level formal tool users—to come together and learn from one another.

Looking back, I never thought that I’d be leaving my hometown at all, never mind leaving India. My travels over the years have allowed me to meet lovely and smart people from all parts of the world. Technology brings people together, and the more I do this, the more I feel that I live in one global village where, after a point, the differences in nationalities, languages, and views don’t matter—at an abstract level, we have more similarities than differences. I feel well-qualified to judge this, given how much abstraction I use in formal verification! There is a saying in Sanskrit: “Vasudhaiva Kutumbakam,” which means, “The world is one family.” It certainly feels that way to me.

This article was first published on the Tech Design Forum. It is reproduced here in its original form for informational and archival purposes, with appropriate acknowledgment to the original publisher.