This interview presents the first steps of Robert Simpson (R.S.), a Maths graduate who found an unexpected, but natural home in Formal Verification (FV) at Axiomise. Drawn by a desire to apply rigorous logic to real-world problems, he shares how abstract mathematical thinking translates into ensuring hardware correctness at the silicon level. From the excitement of spotting elusive bugs missed by traditional methods to collaborating with experts on complex designs, Robert reflects on the mindset, surprises, and rewards of working in a field that blends philosophy, engineering, and detective work—revealing how precise reasoning can have a tangible impact on the technology that shapes our world.
What initially drew you from the world of Maths into the field of FV?
R.S.: – In the final few years of my degree, I thought a lot about what I wanted to do going forward with my career. The focus of my final year was understanding how proof and logic could be used and applied to solve a huge range of problems, and I knew that I wanted to continue to problem solve in a mathematically rigorous way. When I found Axiomise at a careers fair, I was immediately interested by the need for formal proof in silicon verification and wanted to learn more.
How did you fare stepping into the job market with that fresh degree in hand?
R.S.: Starting work in the industry after finishing my degree was very exciting. After lots of studying, it was refreshing to try something new and see how the skills which I had learnt could be applied to real-world problems.
What’s one habit from your Maths degree that turned out to be unexpectedly valuable on the job?
R.S.: I think that the habit which I learnt from my degree, which has been the most useful, is my reaction to always carefully think through the consequences of any assumption or requirement. In both mathematics and FV, this is important because the precise definition of the problem space is critical to the answer to the problem, or whether a bug can be found. In technical research, the importance of methodical accuracy is clearer because of the need for critical thinking when reading papers and reaching sound conclusions; however, I was quite surprised by how useful this turned out to be for reading design specifications and constructing formal checks. The experience with this that I gained during my degree certainly helped me to pick up formal quicker and make more useful contributions.
What surprised you most about applying abstract mathematical thinking to something as tangible—and consequential—as hardware correctness?
R.S.: Whilst working at Axiomise, I have been impressed by how rigorous the field of hardware correctness can get at times. Before starting, I would have guessed that in the important physical industry of hardware, formal mathematical analysis would be limited or bound by approximations, but in fact formal verification has a long history of solid logical foundations. I have really enjoyed this aspect of the hardware industry, as it combines the logical reasoning which really interests me, and knowledge of different designs to produce effective and logically sound results.
What is the most fulfilling part of working at Axiomise?
R.S.: For me, the most fulfilling part of working at Axiomise has been the ability to work alongside experts in formal verification using cutting edge techniques in order to find intricate bugs, get correctness proofs for massively complex designs or research new techniques to further develop the field of FV. Being able to bounce ideas back and forth and have innovative discussions with people with so much knowledge and experience is really rewarding, and this collaborative environment makes solving problems that would otherwise not be resolved particularly enjoyable. It’s great to be able to learn so much and build upon existing methods within an amazing team.
What’s a moment at the company where you realized: “This isn’t just theory anymore—this actually changes how the world works”?
R.S.: I think the first moment I realized the importance of formal hardware verification was when I first saw a bug that had been missed by all non-formal verification. This made it clear to me that the theoretical advantages of formal actually translate into practical results when applied to real designs.
How does a day in the life of an Axiomiser look? How do you find the collaboration with engineers and researchers?
R.S.: What happens during a day at Axiomise varies a lot depending on the state of the current project. The first thing I do will typically be checking if there was any new progress in my checks overnight, raising some new potential failures which need to be debugged. I will look carefully into the flagged situation and use my knowledge of the design or work with a colleague to determine if there is an actual error in the design. Once we work out the cause, the next step could be a meeting with the customer to raise the issue and try to find a fix, or returning to tweak the tests to find a different case. Alongside this, I might also be running some experiments with the researchers in the R&D team, testing out different methods in order to find new ways to find bugs and correctness proofs for more complex designs. Working with different teams is always exciting as it often means we are thinking about a tricky problem and there are always many different clever ideas and potential solutions to get stuck into.
What mindset is required to do FV?
R.S.: I think a key aspect of doing formal verification is the ability to carefully think through a problem. This comes up over and over: when ensuring that all cases of a requirement are going to be considered, understanding what possible edge cases could occur, or when thinking through safe constraints to be put on a system. This ability to be methodical and understand all possibilities is important in many areas of research and industry, but is an invaluable part of doing FV.
After eight months at Axiomise, is FV closer to philosophy, engineering, or detective work in disguise?
R.S.: I think after working at Axiomise for several months, I would say that FV is really a mix of all three. There is an aspect of detective work when trying to carefully figure out why certain behaviours are occurring and looking for the root cause, but also one of engineering the best and most accurate checks to ensure that the specification is met. I would say there is even a bit of philosophy involved when trying to understand the proof construction methods and develop the best ways to utilise their advantages to be able to create new techniques.
What makes a new joiner succeed at Axiomise? What piece of advice would you give young people interested in this field?
R.S.: I think what makes people successful at Axiomise or working on formal verification in general is always having an interest to learn more about the really interesting elements of hardware design. Computers are so complex now, and there are so many cool ideas that go into making them as efficient as possible, that – if you are interested – there are always more interesting parts to learn about. Knowing everything is impossible, but learning as much as possible helps so much when finding out about something new and enables a deeper understanding sooner.
If you’re keen to delve further into formal verification, Axiomise’s website is an excellent place to start—offering both resources and career opportunities. The company’s semi-annual Graduate Program provides a welcoming pathway for aspiring candidates, with applications open directly via the website or Handshake.
Robert Simpson is a Formal Verification Engineer at Axiomise, bringing his problem-solving and logical reasoning to both customer projects and innovation research work aimed at improving the ability of formal methods to reach conclusive proofs. He works on verification of digital hardware designs through the use of formal methods to find design bugs and produce proofs of correctness. Before Axiomise, Robert studied Mathematics at Churchill college, with focusses on Foundations, Quantum computation and topology. Whilst at Cambridge, Robert enjoyed time with societies such as board games, Ultimate Frisbee and bridge. He also took part in a summer research project through the mathematics department, investigating whether a particular technique could be applied to a similar but subtly different problem. Robert learnt about Axiomise at a University Careers fair, and their work using mathematical approaches to the verification of cutting-edge hardware encouraged him to learn more and eventually apply for a position where he uses the skills and knowledge he built during his degree to effective use in an important field in our digital world.
Also Read:
Axiomise Introduces nocProve to Transform NoC Design Verification
Akeana Partners with Axiomise for Formal Verification of Its Super-Scalar RISC-V Cores
IP Surgery and the Redundant Logic Problem
Share this post via:
Solving the EDA tool fragmentation crisis