Formal Verification Engineer, RISC-V

  • Full-time

Company Description

RISC-V International is a global nonprofit association based in Switzerland. Founded in 2015 as the RISC-V Foundation with 29 members, RISC-V is now a truly global organization with 2k+ members in more than 70 countries. The RISC-V technical team is responsible for developing and ratifying standards and specifications for the RISC-V ISA, community outreach through talking with prospects, evangelizing at meetup conferences and individual interaction as well as recruiting, mentoring and helping leaders for our 40+ groups (and growing).

Job Description

RISC-V International is looking for a Sail Developer to help build out the RISC-V Formal Model codebase. Part of the acceptance criteria for ratification of a RISC-V hardware specification includes the completion of the formal model deliverables for the extension seeking ratification. RISC-V has chosen Sail from Cambridge as it’s formal modeling language. RISC-V Sail both uses and depends upon the associated tools including the simulator generator.

This role will lead development of the formal model for extensions and augment the Sail infrastructure to support formal model development. Work with specification document creation so that the formal model is consistently integrated into the specification and in the formal model files. Provide leadership, oversight, and coordination for efforts with the Task Groups, Development Partners, and Cambridge Sail staff.

 Key Responsibilities

  • Work with the RISC-V Sail ecosystem including: the RISC-V Sail maintainer, Cambridge Sail staff, RISC-V Architectural Tests efforts, RISC-V Task Groups, and RISC-V Development Partners to ensure the success of the RISC-V Sail Formal Model.
  • Work with the RISC-V Sail repository maintainer to provide priorities and oversight of RISC-V Sail development throughout the ecosystem
  • Develop Sail Formal Model code for extensions and upstream to the RISC-V Sail repository
  • Enhance Sail infrastructure (e.g. simulator generator functionality) to support the RISC-V Formal Model
  • Define a strategy for integrating Sail example code into the specifications and implement that strategy on formerly ratified specifications
  • Maintain the RISC-V Sail Formal Model community including mailing lists, informational meetings, and developer training
  • Communicate status to the RISC-V Task Group Chairs and inform the greater RISC-V community of updates as appropriate
  • Support onsite or virtual events including RISC-V conferences with regards to RISC-V Sail Formal Model training and status updates

Qualifications

  • 5+ years software development experience
  • Experience developing open source code
  • BS/BA in a computer science related field or equivalent years of experience
  • History of successful completion and maintenance of software projects
  • Experience as a hardware or software products developer with knowledge of assembly language, HDL code, and RTL abstractions
  • The ability to respond and adapt to a highly interrupt driven environment while maintaining focus on long term objectives
  • Effectively manages time, sets goals, and effectively communicates status
  • Adept at interacting with technical leaders to communicate goals, track status, and resolve roadblocks
  • Must have a service oriented outlook: makes all RISC-V members feel they are valued
  • Ability to understand and operate within complex, multi-stakeholder environment
  • Knows how to follow up and drive projects to closure in a timely manner and get results
  • Experience releasing hardware or software products to customers through multiple releases
  • High level of written and verbal skills, must be concise, articulate and understandable
  • High level of attention to detail, content, and form

Additional Information

Preferred

  • 10+ years software development experience
  • 5+ years developing open source code
  • Experience as an open source code base maintainer
  • Advanced degree in CS / ECE / EE or equivalent
  • Understanding of computer architecture, privilege levels, virtual memory, formal verification, and design verification
  • Experience with Rust, Haskell, OCaml, F#, Scala
  • Understanding of compilers
  • Understanding of modern, automated testing
  • Understanding of modern verification tools like Z3
  • Experience giving presentations at corporate events
  • Proficient with GitHub, Google/MSFT Suites, and Atlassian tools