Introducing Doc Formal: the journey so far
Ashish Darbari is CEO of formal verification consultancy and training provider Axiomise. Welcome, intrepid readers, to the Doc Formal column. Since this is my first post, let me introduce myself and describe how formal verification became my life’s passion. After all, when you are selecting a medical doctor, an initial peek at his/her credentials is wise. Your sources for technical insight should face the same scrutiny.
I would also argue that my journey shows how formal techniques have evolved over roughly the last two decades. This is not just about me, but also about why you can – and should – place greater confidence in formal as a mainstay of our response to the ever-growing verification challenge.
Between nature and nurture, it is difficult to say what plays a more important role in life. 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. Our pedigree destined me for a life devoted to the sciences. However I had no inkling back then that my career path would lead me to Intel, ARM, Imagination, and today OneSpin Solutions. How did I go from being a kid in India to becoming 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 our household. My dad runs the family business in mechanical, electrical, and electronics manufacturing. It was founded by my late grandfather in the 1920s. Among the many things that he designed and built were the first pontoons for Allahabad’s floating bridge across the Ganges and Yamuna rivers. Some of the first electrical computing machines were built by my late uncle, who also designed one of India’s first analog and digital computers in the early 1960s. Those were used at several national universities for teaching digital electronics.
My first interaction with computers happened when I was about 11. We acquired a Color Genie. My excitement knew no bounds as I played my first computer video game — never mind that it took 45 minutes to boot the OS out of a cassette. It was not long before we had one of the first x86 machines at home with floppy disks booting DOS. We were sharing in the computing revolution of the mid-1980s. But it was not until the early 1990s when my mom also got addicted and started to learn programming, that my interest spread beyond gaming.
Who cares if it took 45 minutes to boot? The Color Genie had games (Frank Seger)
Living in Allahabad afforded me the opportunity to attend St. Joseph’s College, a top school, where I began exploring my career choices. It was thought at the time in India that if you did not pursue an engineering or medical degree, there must be something wrong with you. I had the luxury of consuming engineering bites of different flavours at home. The most challenging question then was not whether to study engineering, but whether I could get into a decent school. The litmus test was the All India Engineering Entrance Examination (AIEEE), now called the Joint Entrance Examination (Main). My results qualified me to study electrical and electronics engineering at Birla Institute of Technology, Mesra.
A university or two… or five
Birla’s curriculum was heavy on electrical control and power systems but still had a fair share of electronics and computing, including programming in Pascal, Fortan, C, and x86 assembly. My path took a decisive turn when I started working on a project to design a power-frequency controller based on fuzzy logic and AI. We were tasked with researching a technique to find voltage and current correlations on a heavily-loaded electrical system. The goal was to find variance and perform fuzzy set classification for fast decision making for load-shedding, thereby providing timely power frequency correction and preventing electrical turbine failure. As it turned out, our study had a negative result. There was no strong evidence to suggest that V-I variance was a good predictor; in fact, df/dt-based prediction and control was better.
We were praised 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; negative results are not necessarily bad. This project drew me closer to AI as a subject and was the impetus for my studying it for my master’s degree. However, I had not chosen an easy road. The transition from ‘double E’ to majoring in computing is tough.
I pursued a master’s in computational logic at TU Dresden, Germany. The course focused on the basics of formal methods, formal logic, and their application to real world problems. It dove deeply into theoretical aspects of computer science. For someone who did not hold a CS degree, it was a significant challenge. Were it not for the helpful instructors who spent time clarifying concepts and providing tips to help me get on top of the advanced courses, I do not 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 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, mostly in machine learning. Only one was in formal hardware verification, and I selected it for two reasons. First, it made perfect sense for me to combine my undergraduate and graduate studies by applying formal methods to hardware design verification. Second, Professor Tom Melham of Glasgow University, UK who offered me the opportunity, was a leader in the field. He also had a donation from Intel to pursue my research. It’s very hard to say no to a full scholarship.
In my second year at Glasgow, Tom was offered a position at Oxford University. I moved with him though the transfer meant that I was instead working toward a DPhil, Oxford’s equivalent of a PhD. I was also 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, US. At the time, symbolic model checking was making headlines due to Kenneth McMillan’s work and Randall Bryant’s invention of BDDs. SCL was the powerhouse in high-end innovation of formal solutions.
Doc Formal earned his DPhil at Oxford’s Balliol College (Peter Trimming)
My DPhil work was tied to one of the hardest problems then and even today, reducing complexity for large-scale model checking. In simple terms, this explores how to verify huge hardware designs in a reasonable timeframe and with comprehensive rigor so that you find bugs before fabrication in silicon. 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 that were 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 took me closer to mastering some of the hardest but also most satisfying aspects of formal, theorem proving with LCF-style theorem provers such as the higher-order logic (HOL) family. Using theorem proving and model checking together, I saw how the best of both worlds provides powerful solutions for scalable and rigorous verification. All told, I got to spend six months with Intel SCL during my doctoral research. That time gave me unique insights into a world one cannot appreciate solely through university study, even when that university is Oxford: There is no substitute for practical experience.
Doc Formal branches out
After completing my DPhil at Balliol, I had the option of either transitioning into industry or pursuing further academic research. Professor Bashir Al Hashimi at the University of Southampton, UK 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. These are massively more efficient when compared to traditional fault injection methods.
I also had the good fortune to work with two luminaries from ARM, John Biggs and David Flynn, with whom I collaborated on developing a method for estimating empirically how much selective state retention needs to be built in for CPUs. Our main finding was that the programmer-visible state or the architectural state of the CPU must be implemented using retention registers, while other micro-architectural enhancements (e.g., pipeline registers, TLBs, caches) can be implemented using normal registers without retention. This has a profound impact on power and area savings.
Toward the end of my project with Bashir, I was contacted by Professor Joao Marques Silva, one of the best-known names in the field of SAT solvers. He had an interesting problem centred on designing certified SAT solvers.
SAT solvers have been around for nearly four decades but in the last 15 years or so they have become instrumental in increasing the performance of formal solvers and driving the adoption of formal tools. As with most things algorithm-based, they can have bugs. However, the ramifications of a buggy SAT solver can be severe, as one will likely produce an incorrect outcome when used in a formal tool. This is especially problematic — and potentially dangerous — if the tool is used for verifying safety-critical systems.
Joao explained that there had been earlier research into SAT proof checkers that could validate the outcome of a SAT solver. But to complicate matters, these checkers could themselves have bugs: A still higher degree of assurance was needed. This could only be provided by generating a 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 our research, we discovered a corner case bug in a famous SAT proof checker. It goes to show that in the sciences, there is always room for improvement.
Moving into industry (and all over the world)
After four years at Southampton, I realized that I had spent nearly 16 years in academia. Perhaps it was time I switched to industry. I joined ARM as a verification engineer and started to see where the industry was in its use of formal. I had seen formal in action at Intel, so my assumption was that ARM would be using these techniques extensively as well. I was not entirely correct.
At the time, ARM’s was using formal on only a few projects and management was not generally open to resourcing formal verification. Despite this, I was given the opportunity to work on multiple projects to show how formal can deliver more rigor and find more bugs, saving valuable time and cost. My stay at ARM was relatively short — about 18 months — but I worked on some interesting projects. One addressed the lock-step verification of an R-class CPU; another the verification of a cache-coherency block. I was also instrumental in developing ARM’s first formal verification roadmap.
In 2011, my wife accepted a job as a lecturer at the Indian Institute of Science Bangalore, so I found myself moving back to India. I joined General Motors’ India Science Lab, which was one of the best R&D labs for formal rigorous control software verification. But just when I was hitting my stride there, GM announced in 2012 that the lab would close. Almost 90 researchers, mostly 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 was not having the best time dealing with Bangalore’s infrastructural growing pains, we decided to move back to Europe. But where?
Since 1993, I had lived, studied, and travelled in five countries on three 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 Imagination Technologies in the UK to work on building a consistent formal verification strategy that could show real value-added benefits.
I worked initially in its PowerVR unit but three months into the job, my boss, Colin McKellar, and I moved to a central team to serve the needs of the wider company. Verification was part of Colin’s remit and I was given the chance to steer a consistent roadmap for formal verification deployment. There was no existing plan, so I had the freedom to dream and execute whatever made sense—an opportunity not many people get. I formed a methodology group called Advanced Verification Methodology (AVM) in January 2013 and hired three people who reported to me, along with one additional engineer who reported to Colin and was responsible for UVM adoption.
Within three years, my team and I had trained nearly 100 engineers across Imagination’s global business units and delivered on more than 50 projects. I ensured that my team was not only the best in formal verification at Imagination, but also stood out as one of the best in the world. To achieve this, it was important to establish a culture of thought leadership, innovation, and peer-reviewed publication. I filed 15 patents in three years, and was lucky to have had seven issued in the UK and three in the US. We published numerous papers at conferences and industrial forums and gave countless keynotes.
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. This gives me a chance to interact with the students on a regular basis and to share my excitement and experience of formal. I am delighted to have the opportunity. It is a chance to give back something to the institutions that supported me.
Teaching at Southampton University offers a chance to return the favors of academia (ECSD Soton)
At the time, Imagination was on a high—or so we thought. The world discovered in February 2016 that its finances were not looking good and a big shakeup was imminent. I started to lose team members as part of a large-scale exodus. Sadly, morale was dropping even more sharply than our numbers. Once again, it was time to check my compass.
The future is formal
In October 2016, I took the plunge and moved to the EDA industry. As I began to prospect, I learned that one of the best verification companies, OneSpin Solutions, was hiring. I joined as director of product management to shape the next steps in the company’s technology.
Seven months in, I can say with confidence that this has been a terrific opportunity. As a longstanding user of different formal tools, I have found it fascinating to swap roles and see the world from 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 still lean enough to be agile and dynamic, it is orders of magnitude faster—and therefore more fun!
I have been globetrotting for the last 25 years. I now live in North London with my wife and son. I have the pleasure of working for a company solely focused on formal verification. I make regular trips to our headquarters in Munich, Germany, and enjoy traveling the world to share my passion for formal. I very much look forward to establishing Doc Formal as a forum where everyone—from formal verification novices to expert-level formal tool users—can come together and learn from one another.
I never thought that I would leave my hometown, never mind India. My travels have allowed me to meet many 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, differences in nationalities, languages, and views do not 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.
Join the conversation! Send your questions and comments to @ashishdarbari on Twitter using the hashtag #DocFormal.
