Playing at computing<\/strong><\/h3>\nComputers 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\u2019s 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\u2019s first analog and digital computers in the early 1960s. Those were used at several national universities for teaching digital electronics.<\/p>\n
My first interaction with computers happened when I was about 11. We acquired a Color Genie<\/a>. My excitement knew no bounds as I played my first computer video game \u2014 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.<\/p>\n![\"Who](\"https:\/\/www.techdesignforums.com\/practicefiles\/2017\/05\/ColorGenie_FrankSeger-1024x708.jpg\")
<\/a>Who cares if it took 45 minutes to boot? The Color Genie had games (Frank Seger)<\/p><\/div>\n
Living in Allahabad afforded me the opportunity to attend St. Joseph\u2019s 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)<\/a>. My results qualified me to study electrical and electronics engineering at Birla Institute of Technology, Mesra<\/a>.<\/p>\nA\u00a0university or two\u2026 or five<\/strong><\/h3>\nBirla\u2019s 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.<\/p>\n
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\u2019s degree. However, I had not chosen an easy road. The transition from \u2018double E\u2019 to majoring in computing is tough.<\/p>\n
I pursued a master\u2019s 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\u2019s) with a German 1.7 (\u2018good\u2019), and my thesis was awarded a 1.1 (\u2018excellent\u2019). I discovered a new aspect of learning: We can learn whatever we want, even if it feels alien in the beginning.<\/p>\n
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<\/a> 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\u2019s very hard to say no to a full scholarship.<\/p>\nIn 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\u2019s 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\u2019s Strategic CAD Labs (SCL) in Oregon, US. At the time, symbolic model checking was making headlines due to Kenneth McMillan\u2019s work<\/a> and Randall Bryant\u2019s invention of BDDs<\/a>. SCL was the powerhouse in high-end innovation of formal solutions.<\/p>\n![\"Doc](\"https:\/\/www.techdesignforums.com\/practicefiles\/2017\/05\/Oxford_-_Balliol_College_-_PeterTrimming.jpg\")
<\/a>Doc Formal earned his DPhil at Oxford’s Balliol College (Peter Trimming)<\/p><\/div>\n
My DPhil work<\/a> 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<\/a> of finding bugs and building exhaustive proofs.<\/p>\nMy work took me closer to mastering some of the hardest but also most satisfying aspects of formal, theorem proving with LCF-style theorem<\/a> provers such as the higher-order logic (HOL) family<\/a>. 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.<\/p>\nDoc Formal branches out<\/h3>\n
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<\/a>. These are massively more efficient when compared to traditional fault injection methods.<\/p>\nI 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.\u00a0Our main finding<\/a> 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.<\/p>\nToward the end of my project with Bashir, I was contacted by Professor Joao Marques Silva<\/a>, one of the best-known names in the field of SAT solvers<\/a>. He had an interesting problem centred on designing certified SAT solvers.<\/p>\nSAT 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 \u2014 and potentially dangerous \u2014 if the tool is used for verifying safety-critical systems.<\/p>\n
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<\/em> 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.<\/p>\nI 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.<\/p>\n
Moving into industry (and all over the world)<\/strong><\/h3>\nAfter 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.<\/p>\n
At the time, ARM\u2019s 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 \u2014 about 18 months \u2014 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\u2019s first formal verification roadmap.<\/p>\n
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\u2019 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\u2019s infrastructural growing pains, we decided to move back to Europe. But where?<\/p>\n
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.<\/p>\n
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\u2019s 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\u2014an 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.<\/p>\n
Within three years, my team and I had trained nearly 100 engineers across Imagination\u2019s 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.<\/p>\n
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.<\/p>\n
![\"Teaching](\"https:\/\/www.techdesignforums.com\/practicefiles\/2017\/05\/ECS_Southampton-1024x576.jpg\")
<\/a>Teaching at Southampton University\u00a0offers\u00a0a chance to return the favors of academia (ECSD Soton)<\/p><\/div>\n
At the time, Imagination was on a high\u2014or 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.<\/p>\n
The future is formal<\/strong><\/h3>\n
<\/a>Who cares if it took 45 minutes to boot? The Color Genie had games (Frank Seger)<\/p><\/div>\n
Living in Allahabad afforded me the opportunity to attend St. Joseph\u2019s 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)<\/a>. My results qualified me to study electrical and electronics engineering at Birla Institute of Technology, Mesra<\/a>.<\/p>\n Birla\u2019s 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.<\/p>\n 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\u2019s degree. However, I had not chosen an easy road. The transition from \u2018double E\u2019 to majoring in computing is tough.<\/p>\n I pursued a master\u2019s 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\u2019s) with a German 1.7 (\u2018good\u2019), and my thesis was awarded a 1.1 (\u2018excellent\u2019). I discovered a new aspect of learning: We can learn whatever we want, even if it feels alien in the beginning.<\/p>\n 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<\/a> 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\u2019s very hard to say no to a full scholarship.<\/p>\n 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\u2019s 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\u2019s Strategic CAD Labs (SCL) in Oregon, US. At the time, symbolic model checking was making headlines due to Kenneth McMillan\u2019s work<\/a> and Randall Bryant\u2019s invention of BDDs<\/a>. SCL was the powerhouse in high-end innovation of formal solutions.<\/p>\n Doc Formal earned his DPhil at Oxford’s Balliol College (Peter Trimming)<\/p><\/div>\n My DPhil work<\/a> 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<\/a> of finding bugs and building exhaustive proofs.<\/p>\n My work took me closer to mastering some of the hardest but also most satisfying aspects of formal, theorem proving with LCF-style theorem<\/a> provers such as the higher-order logic (HOL) family<\/a>. 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.<\/p>\n 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<\/a>. These are massively more efficient when compared to traditional fault injection methods.<\/p>\n 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.\u00a0Our main finding<\/a> 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.<\/p>\n Toward the end of my project with Bashir, I was contacted by Professor Joao Marques Silva<\/a>, one of the best-known names in the field of SAT solvers<\/a>. He had an interesting problem centred on designing certified SAT solvers.<\/p>\n 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 \u2014 and potentially dangerous \u2014 if the tool is used for verifying safety-critical systems.<\/p>\n 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<\/em> 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.<\/p>\n 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.<\/p>\n 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.<\/p>\n At the time, ARM\u2019s 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 \u2014 about 18 months \u2014 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\u2019s first formal verification roadmap.<\/p>\n 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\u2019 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\u2019s infrastructural growing pains, we decided to move back to Europe. But where?<\/p>\n 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.<\/p>\n 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\u2019s 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\u2014an 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.<\/p>\n Within three years, my team and I had trained nearly 100 engineers across Imagination\u2019s 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.<\/p>\n 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.<\/p>\n Teaching at Southampton University\u00a0offers\u00a0a chance to return the favors of academia (ECSD Soton)<\/p><\/div>\n At the time, Imagination was on a high\u2014or 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.<\/p>\nA\u00a0university or two\u2026 or five<\/strong><\/h3>\n
<\/a>Doc Formal branches out<\/h3>\n
Moving into industry (and all over the world)<\/strong><\/h3>\n
<\/a>The future is formal<\/strong><\/h3>\n