Yahya Sohail

Tenstorrent

Sr. Engineer, Design Verification — Apr 2026 - Present

Design Verification Engineer — Jan 2025 - Apr 2026

Austin, TX

• Develop test generators including the open source RiESCUE suite and CoreTP. RiescueC and CoreTP will be used to generate many of the official compliance tests for the RISC-V architecture.
• Develop internal core level test generators and a RISC-V page table generator.
• Develop a micro-architecture agnostic memory ordering stimulus generator and checker that require no internal core instrumentation, suitable for use in emulation where instrumentation is expensive, and on any RISC-V core with minimal testbench support.
• Support several internal customers of these test generators and open source users.
• Verified the implementation of the hypervisor feature on Ascalon, a high performance out-of-order superscalar core.
• Wrote architectural coverage, tests, and debugged RTL test failures for the hypervisor feature.
• Found many bugs across the core, our open source instruction set simulator Whisper, and the testbench.

Intel Corporation

Formal Verification Intern — May 2024 - Aug 2024

Austin, TX

• Contributed to the formal model of the x86 ISA written in ACL2.
• Proved theorems in ACL2 regarding the behavior of the model, with a particular focus on address translation using a new TLB (Translation Lookaside Buffer).
• Identified and fixed several bugs in the x86 model.
• Proved the correctness of an x86 program called "zeroCopy," which involved moving data within the virtual address space by modifying page tables.
• Thoroughly documented the changes made to the model, ensuring clarity and ease of understanding for future contributors.
• The work is now publicly available under a BSD style license as part of the ACL2 Community Books.

UT Austin

Undergraduate Research Assistant — May 2023 - Aug 2023

Austin, TX (Remote)

• Supervised by Dr. Warren A. Hunt, Jr.
• Expanded the formal model of the x86 ISA written in ACL2 to make it capable of booting a modified Linux kernel, including modeling timer and TTY peripherals, modeling interrupt and exception behavior, and implementing additional instructions.
• Worked toward being able to prove theorems about arbitrary x86 code using the ACL2 theorem prover.
• Continued work on this project as part of undergraduate research courses and defended an honors thesis on it.

SIC Digital

Full Stack Developer — Oct 2020 - Jul 2022

Austin, TX (Remote)

• Worked on More Pickups, a service used by organizations to manage picking up donated items from donors' homes.
• Designed and implemented a prototype microservice-based backend architecture.
• Worked with JavaScript, Express, and PostgreSQL on the backend and HTML, CSS, JavaScript, and React on the web-based frontend.
• Created a React Native-based cross-platform mobile app.

Freelance Work

Web Developer — Jun 2016 - May 2022

Houston, TX

• Worked on websites built with WordPress and Drupal content management systems.
• Used PHP, HTML, CSS, and JavaScript to add functionality that clients requested.