Formal Verification

Mayank Kumar

Cambridge, England, United Kingdom · Arm

I am a formal verification engineer at Arm, where I work on next-generation IPs with a focus on formal sign-off, property checking, scalable FPV environments, and complex hardware validation across compute and control-heavy designs. My background spans formal verification and product engineering roles at Arm, Intel, and CommScope, along with earlier research in wireless systems and 5G C-RAN at IIT Bhilai, IIT Hyderabad, and IIT Kanpur.

  • Formal sign-off
  • Property checking
  • FPV environments
  • RTL verification

Experience

Formal Verification Engineer

Applying formal verification on next-generation IP blocks for formal sign-off, with an emphasis on scalable verification strategy and high-confidence hardware validation.

2023 - Present

Formal Verification Engineer

Owned formal property verification for next-generation memory controller and hardware reset sequencer blocks, developed an end-to-end FPV environment for scheduler verification, and supported a 10+ engineer formal verification team.

2021 - 2023

Software Engineer

Added Multi RU support to the O-RAN compliant fronthaul of CommScope's ONECELL product and contributed to wireless infrastructure software in a production environment.

2020 - 2021

Research Intern

Worked on dynamic functional split selection in 5G C-RAN systems under traffic and fronthaul constraints, leading to a publication at IEEE NetSoft.

May 2019 - Jul 2019

Research Intern

Designed and simulated a MIMO antenna system using HFSS, and evaluated envelope correlation and related performance metrics using MATLAB.

May 2018 - Jul 2018

Project

Formal Property Verification of Memory Controller

Owned and executed formal property verification for Intel's next-generation memory controller IP, while helping scale verification across a broader team and delivery pipeline.

Nov 2021 - Nov 2023

Formal Property Verification of Hardware Reset Sequencer

Formally verified deadlock and livelock scenarios together with key functional requirements for a next-generation SoC reset sequence controller.

Jul 2021 - Nov 2021

Multi RU Support to ONECELL's O-RAN Fronthaul

Added multi-RU support to the O-RAN compliant fronthaul of CommScope's ONECELL product.

Aug 2020 - Jul 2021

Dynamic Functional Split in 5G C-RAN

Proposed a traffic-aware system that dynamically changes split options to keep a 5G C-RAN deployment as centralized as possible under fronthaul and traffic constraints.

May 2019 - Jul 2019

Education

Indian Institute of Technology, Bhilai

Bachelor of Technology (Honors)
Electrical Engineering and Computer Science

CGPA: 9.19/10

2016 - 2020

Skills

Core Areas
  • Formal verification, assertion-based verification, and sign-off quality validation
  • SoC and IP verification for memory, reset, scheduler, and hardware control blocks
  • Scalable FPV environment development, bug hunting, and deep property analysis
  • Wireless systems, O-RAN fronthaul, and 5G C-RAN research
Tools & Languages
  • Jasper Formal, property checking workflows, and modern formal verification tooling
  • Python, MATLAB, Octave, C, C++, Verilog
  • GNU Radio, HFSS, Simulink, PSCAD

Licenses & Certifications

Issued Feb 2023
Issued Nov 2022

Publications

Quiescent Formal Checks (QFC) for Detecting Deep Design Bugs - Sooner and Faster

DVCON · September 14, 2023
Presents a bug-hunting strategy for pre-silicon formal verification that uses quiescent-state checks and bounded model checking to expose deep control-design bugs without requiring a full formal specification.

Traffic-Aware Dynamic Functional Split for 5G Cloud Radio Access Networks

IEEE NetSoft
Proposed a dynamic functional split selection method for 5G C-RAN systems that balances centralization goals against midhaul bandwidth and traffic heterogeneity.

Uplink and Downlink Performance Bounds for Full Duplex Cellular Networks

IEEE BlackSeaCom
Studied uplink and downlink trade-offs in full duplex cellular systems and analyzed how interference shapes performance at realistic deployment densities.