Pedro Pontes García, Kevin Laeufer, Adrian Sampson

Project in progress

Bitvector equivalences are crucial for software and hardware verification through satisfiability modulo the theory of bitvectors (SMT-BV), as well as electronic design automation (EDA). Prior work toward bitvector reasoning is largely constrained to fixed-width and single-parameter applications, despite the pervasiveness of multi-width parametric bitvector operations in EDA and SMT-BV. We develop a domain-specific language for expressing bitvector rewrites, with the goals of automatic generation of compilation passes for MLIR-based EDA toolchains, and production of correctness certificates via SMT.

Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, Adrian Sampson

In Object-Oriented Programming, Systems, Languages & Applications (OOPSLA 2026)

Accelerator design languages (ADLs), high-level languages that compile to hardware units, help domain experts quickly design efficient application-specific hardware. We introduce Petal, a cycle-level profiler for ADLs that compile to the Calyx intermediate language (IL). Petal produces traces of call trees, and constructs an ADL-level profile. We demonstrate that Petal's cycle-level profiles can identify performance problems in existing accelerator designs and guide compiler developers toward optimizations, including a reduction by 46.9% of total cycles for a large-scale application.

Equinor Research Center, Trondheim, Norway

Summer 2024

• Worked on the development of a software tool for model predictive control in offshore energy production and carbon capture.
• Rebuilt frontend using TypeScript, React, and D3.js, and developed comprehensive types in a previously untyped codebase.
• Built a functional-style Python middleware server with gRPC to connect the frontend to a legacy C++ backend.
• Rotated through leadership within a six-person international team.