Background
I was in the final year of my undergraduate degree in Electronics and Communication Engineering when I learnt out about the RISC-V Mentorship program from the RISC-V Careers page. Having a strong interest in Computer Architecture and Formal Verification, I was eager to contribute to open source hardware engineering projects to gain experience in this field.
Mr. Matt Venn of Symbiotic EDA provided an academic licensed Symbiotic EDA tool to me at no cost, after I requested for this on Symbiotic EDA’s website. This licensed tool allows me to formally verify designs written in SystemVerilog, such as the SweRV EL2 processor. After learning the basics of Formal Verification from Mr. Matt Venn’s excellent videos on Formal Verification using SymbiYosys, and setting up and running formal checks on small Verilog desigs using Symbiotic EDA, I was raring to perform formal verification on larger designs. I selected the SweRV EL2 processor because it was lacking an open-source formal verification testbench, and the core looked small enough to formally verify it using RISC-V Formal in about 3 months time, along with my undergrad work.
Application and Selection in the RISC-V Mentorship Program
I first created an issue on the GitHub repository of SweRV EL2 processor to let the project contributors know of my interest to work on this project under the RISC-V Mentorship Program. I also sent an email about my interest in working on this project to the RISC-V Mentorship team. I got a reply that Mr. Joe Rahmeh of Western Digital volunteered to mentor me for this project. I was very excited to learn that I would be working on processor formal verification over the next few months. I was given a few tasks like uploading my resume on the page of my mentorship on the LFX Mentorship portal, which I completed immediately.
Mentorship Experience
- I referred to the Ibex processor’s source code to learn how to connect and drive the RVFI (RISC-V Formal Interface) ports to a pipelined processor. Searching for a particular signal in thousands of lines of code, is not very different from searching for a needle in a haystack.
- I decided to get help from my mentor for this work. He connected me to his colleague, Mr. Ajay Nath who told me where to search for the relevant signals in the source code and also offered to help me should I have other questions. With his help, and some pre-existing trace signals in the processor’s code base, I completed the process of driving all the RVFI ports.
- In the midst of this process, my mentor evaluated my performance and I was glad to know that I had passed the midterm evaluation.
- The next step was to create a wrapper file and connect the processor to the wrapper file. After that, I had to create a simple configuration file and run the tool.
- There were a few issues that I ran into when running the tool. Debugging and fixing these issues took a few days.
- Finally, all the issues were resolved and I successfully formally verified that for a bound of 20 cycles, the SweRV EL2 processor correctly implements the RV32I instruction set in the non-interrupt mode. The formal run completed in a few hours.
- I submitted documentation of my work to my mentor, and the final evaluation was complete.
Learning
- The project provided hands-on experience in RISC-V instruction set architecture and Formal verification using RISC-V Formal.
- I got a good understanding of the microarchitecture of the SweRV EL2 processor and learnt the best practices for writing processor RTL code by looking at the source code of this processor.
Conclusion
- The completion of this project would not have been possible without the guidance of my mentor and Mr. Ajay Nath. The RISC-V Mentorship program provides an excellent platform for students to get mentored by professionals in the industry to work on real life projects.
- This experience has been positive and has inspired me to participate in more RISC-V projects in the future.
Suggestions for Aspiring Mentees
- Do take up this project only if you are willing to allocate the required amount of hours for this work.
- Choose a project of your interest and skill set, or propose a project.
- Choose a project of the right complexity for your experience level.
- Get in touch with your future mentor early and understand what is required of you in the project.
- Be professional and respectful in your communication with the open source community and the RISC-V team.