A Type System for Communication-Safe Hardware Design
Aditya Ranjan Jha, Jason Zhijingcheng Yu, Umang Mathur, Prateek Saxena
cs.PL
Oct 19, 2026 · v2
cs.AR cs.LO
TL;DR
The metatheory proofs of the Pact type system, including the constructor correspondence, are mechanized in Lean 4 and archived on Zenodo.
Abstract
Hardware components communicate through clock-cycle-sensitive protocols. Hardware Description Languages (HDLs), however, provide limited support for expressing these protocols or for checking that independently developed components agree on them. When components disagree, the composed design can perform unsynchronized exchanges or stop making progress. We call these failures communication-safety violations. Communication safety is thus a global property, determined by interactions between components. This makes it difficult to check modularly. This paper presents Pact, a typed extension of Anvil for modular verification of communication safety in synchronous hardware. Pact types describe message-passing, control-flow, and clock-cycle behaviour. Each component is checked against its type. Compatible types guarantee that the components compose into a communication-safe system. Pact also supports incremental design. It can check a subsystem before the rest of the system exists. The check produces a summary type that captures the communication behaviour left for future compositions. To reduce annotation burden, Pact infers types by abstracting payload values while preserving communication, timing, control, and fairness. These inferred types are optimal for the checker: whenever some checker-accepted types can prove compatibility, the inferred types can prove it as well. Type inference and type checking are decidable, and compatibility is decided by a sound and complete algorithm. We implement Pact by extending the Anvil compiler and evaluate it along five dimensions: detecting communication errors in incremental design, expressiveness on ten clock-cycle-accurate translations of open-source hardware IPs, compatibility-checking time, generated hardware overhead, and annotation burden. Pact expresses realistic protocols and verifies all ten benchmarks in reasonable time.
Problem
Hardware components communicate through clock-cycle-sensitive protocols. HDLs give little support for checking that independently developed components agree on these protocols. Disagreements cause unsynchronized exchanges or loss of progress, called communication-safety violations, and these are hard to check modularly.
Approach
Pact is a typed extension of the Anvil HDL whose types describe message-passing, control flow, clock cycles, and fairness. Types are inferred by abstracting away payload values. Compatibility is decided by reducing it to games on finite graphs, and checking partial subsystems produces summary types for incremental design. Proofs are mechanized in Lean 4.
Results
Type inference and checking are decidable, and compatibility is decided by a sound and complete algorithm. Inferred types are optimal for the checker. The prototype reproduces real AXI protocol errors and verifies ten clock-cycle-accurate translations of open-source hardware IPs in reasonable time.