Skip to main content

RISC-V Formal Verification Engineer (Contractor)

RISC-V Formal Verification Engineer (Contractor)

Website RISC-V International

Company Description

RISC-V is an Instruction Set Architecture (ISA) standard enabling a new era of processor innovation through open collaboration. RISC-V International enables the community to share technical investment, contribute to the strategic future, create more rapidly, enjoy unprecedented design freedom, and substantially reduce the cost of innovation.

RISC-V International, a non-profit organization controlled by its members, directs the future development and drives the adoption of the RISC-V ISA. Members of RISC-V International have access to and participate in the development of the RISC-V ISA specifications and related ecosystem.

This role is a full-time contract opportunity, dedicated to RISC-V International, a stand alone open standards collaboration organization.

To learn more about RISC-V, please visit: www.riscv.org

Job Description

RISC-V International is looking for a Sail Developer to help develop 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 the University of Cambridge as its formal modeling language. RISC-V Sail both uses and depends upon the associated tools including the simulator generator.

This role will develop the Sail formal model support for the RISC-V ISA extensions and augment the Sail infrastructure to support formal model development; work with the RISC-V ISA specification document creation so that the formal model is consistently integrated into the specification and in the formal model files. Collaborate with the RISC-V Staff,  with the Task Groups, Development Partners, and Cambridge Sail staff.

The expected salary range will be $12,000 to $15,000 per month based on experience.

Key responsibilities include:

  • Develop Sail Formal Model code for extensions and upstream to the RISC-V Sail repository
  • Develop assembly language tests to demonstrate proper Sail implementation of the extension and/or feature as compared to the text of the specification.
  • Enhance Sail infrastructure (e.g. simulator generator functionality) to support the RISC-V Formal Model
  • 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 develop 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
  • 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

Qualifications

The following qualifications are required for consideration:

  • 5+ years software or hardware development experience
  • BS/BA in a Electrical or Computer Engineering or equivalent years of experience
  • Understanding of computer architecture, privilege levels, virtual memory, formal verification, and design verification
  • Experience with strongly typed programming languages, such as Rust, Haskell, OCaml, F#, Scala.
  • Experience developing open source code
  • 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
  • Experience with a scripting language (preferably Python) is required.
  • Experience with SW development tools and processes (assemblers, compilers, revision control systems). Experience with git and github is required.
  • Experience with measuring coverage (functional and code) of a software application.
  • 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 in a remote team environment
  • High level of written and verbal skills, must be concise, articulate and understandable
  • High level of attention to detail, content, and form

The following skills are preferred:

  • 10+ years software development experience
  • 5+ years developing open source code
  • Experience as an open source code base maintainer
  • Experience with the Sail programming language (the ISA specification language)
  • Advanced degree in CS / ECE / EE or equivalent
  • Understanding of compilers
  • Understanding of modern, automated, constrained random  testing
  • Understanding of modern verification tools like Z3
  • Proficient with GitHub, Google/MSFT Suites, and Atlassian tools
  • Experience with assertion-based verification methodologies (SystemVerilog Assertions etc.)

Additional Information

All your information will be kept confidential according to EEO guidelines.

To apply for this job please visit jobs.smartrecruiters.com.

View All Jobs

Stay Connected With RISC-V

We send occasional news about RISC-V technical progress, news, and events.