San Mateo, CA
Formal Verification Engineer (Coq Hacker)
SiFive is the leading provider of market-ready processor core IP, development tools and silicon solutions based on the free and open RISC-V instruction set architecture. Led by a team of seasoned silicon executives and the RISC-V inventors, SiFive helps SoC designers reduce time-to-market and realize cost savings with customized, open-architecture processor cores, and democratizes access to optimized silicon by enabling system designers in all market verticals to build customized RISC-V based semiconductors.
We are excited to announce opportunities for Coq hackers at SiFive. SiFive offers a platform to help their customers create new hardware solutions, combining off-the-shelf components like CPUs with application-specific components. We are very interested in assurance about the correctness of such integration. Our library of standard components is centered on the very cool open instruction set RISC-V, which was created by our founders. The job is going to be in our San Mateo office in California.
We are currently looking to hire a few Coq engineers to prove correctness of processors and other crucial pieces of digital hardware. A big chunk of these components will even be open-source. The verification is being done using the Coq library Kami that began its life in the PLV group at MIT, partly under the umbrella of the DeepSpec project.
I would encourage anyone interested in learning more to apply. Please be aware that these positions are only open to people with nontrivial Coq experience, though experience with hardware engineering is not required. (It all turns out to be functional programming, anyway :) !) In applying, please start by summarizing your experience using Coq, ideally to demonstrate correctness of (semi-)realistic systems. The approximate bar is Coq familiarity at the level we'd expect from doing a related master's thesis. However, there are also internship opportunities that may be open to people with slightly less Coq experience.
- Strong background in formal reasoning
- 5+ years of experience in functional programming
- 2+ years of experience using Coq in building (semi-)realistic systems
- Background in Computer Architecture could be useful but not required
- Background in Compiler Verification (like CompCert) is a plus
SiFive is proud to be an equal employment opportunity workplace. We offer a competitive compensation package that includes flexible paid time off, health, vision and dental benefits, 401(k) plan, employee stock option program, and much more. If you yearn to be challenged and wish to work in an environment where the boundaries of your creativity and skills will be tested, then SiFive is place for you!
SiFive is proud to be an equal employment opportunity workplace. We offer a competitive compensation package that includes flexible paid time off, health, vision and dental benefits, 401(k) plan, employee stock option program, and much more. If you yearn to be challenged and wish to work in an environment where the boundaries of your creativity and skills will be tested, then SiFive is place for you. Collaborate | Innovate | Empower