From cloud to edge, Arm provides the compute platforms behind today’s most advanced AI, trusted by innovators worldwide. Backed by SoftBank VF.
About the role
The Theorem Proving Engineering role, you will analyze new data path RTL designs and underlying algorithms, develop abstract C models of these designs, establish equivalence between RTL and C with a commercial checker (SLEC), and formally verify correctness of the models with respect to a high-level architectural specification using the ACL2 theorem prover. You will work closely with designers and verification engineers in various Arm projects, to enable our verification methodology throughout the company. Found on 1752vc Careers, the job board for startup and VC roles.
What they're looking for
- MS or PhD in Computer Science or Mathematics
- Demonstrated strong ability for rigorous mathematical reasoning and familiarity with floating-point arithmetic
- Understanding of standard algorithms and techniques used in the implementation of elementary arithmetic operations
- C programming experience and a reading knowledge of basic Verilog
- Ability to collaborate and contribute in a remote working environment
- Demonstrated ability to develop complex mathematical proofs
More about this role
The Theorem Proving Engineering role, you will analyze new data path RTL designs and underlying algorithms, develop abstract C models of these designs, establish equivalence between RTL and C with a commercial checker (SLEC), and formally verify correctness of the models with respect to a high-level architectural specification using the ACL2 theorem prover.
You will work closely with designers and verification engineers in various Arm projects, to enable our verification methodology throughout the company.
You will contribute to the infrastructure of our verification effort, e.g., by improving interfaces with SLEC and ACL2.
You will consider and potentially pursue applications of interactive theorem proving to other components of Arm processors.
* MS or PhD in Computer Science or Mathematics.
* Demonstrated strong ability for rigorous mathematical reasoning and familiarity with floating-point arithmetic.
* Understanding of standard algorithms and techniques used in the implementation of elementary arithmetic operations
* C programming experience and a reading knowledge of basic Verilog.
* Ability to collaborate and contribute in a remote working environment.
* Demonstrated ability...
Browse similar: Startup jobs · Remote jobs