Sequential Specifications for Precise Hardware Exceptions

A pipelined CPU runs many instructions at once, so it is fiendishly hard to design correctly — a language called PDL lets you instead describe the processor as if one instruction ran at a time and compiles that into a real parallel pipeline, but it could not handle interrupts and traps, the messy events an operating system depends on; this paper (Cornell and NVIDIA — Yulun Yao, Andrew Myers, Ed Suh, and Drew Zagieboylo) presents XPDL, which adds a familiar try-throw-catch style abstraction so precise hardware exceptions can be written simply and compiled correctly, with essentially no performance cost.

The argument in one glance

Problem

Pipelined processors are parallel, but their meaning is sequential

A pipelined processor is hard to design because it is inherently parallel: in any given cycle it is working on several instructions at once, each at a different stage — one being fetched while another executes and a third writes back. Yet the contract the processor must honor, its Instruction Set Architecture (ISA), is essentially sequential: it defines what happens as if instructions ran one at a time, in order. Traditional hardware description languages (like Verilog) describe the concurrent, register-transfer-level behavior directly — flexible enough for high performance, but very hard to reason about when you are hand-managing all the parallelism, forwarding, and stalls of a real pipeline. A recent language, PDL, bridges this gap: you write a high-level, sequential specification of the processor — describing one instruction flowing through, one at a time — and the PDL compiler turns it into an efficient pipelined implementation, automatically handling the hazards. PDL guarantees "one-instruction-at-a-time" (OIAT) semantics: the parallel pipeline it generates behaves exactly as if instructions ran sequentially. That makes designs easy to write and reason about, at performance comparable to hand-written RTL. But there is a catch that keeps PDL from being usable for real systems.
What people did

Encode exceptions in a sequential language not built for them

Real ISAs are not fully sequential. Operating systems depend on hardware exceptions — interrupts from devices, traps from system calls, faults like illegal instructions or page faults, aborts — and a processor must handle them. To be usable by an OS, a PDL design would need to express these. Lacking a dedicated feature, a designer could try to encode exception behavior using PDL's existing sequential constructs, threading the control signals and state manipulations through the normal instruction flow, and hope the compiler still produces a correct pipeline.
Why it fell short

Exceptions are non-sequential and do not fit the model

The problem is that hardware exceptions are inherently non-sequential, and they interact with the pipeline in exactly the ways a clean one-instruction-at-a-time model does not anticipate. Handling an exception typically means flushing the pipeline (discarding the younger instructions that were speculatively in flight), writing to Control and Status Registers (CSRs) that hold processor state like the cause and the return address, rolling back transient effects that should not have happened, and resetting pipeline state before jumping to a handler. None of this is the smooth, in-order progression of one instruction after another; it is an abrupt, global, atomic intervention on the whole pipeline. Trying to express it with PDL's sequential constructs is awkward and inefficient, because those constructs were designed for the normal flow, not for an out-of-band event that reaches across all the in-flight instructions at once. And getting it wrong is dangerous: modern processors must provide precise exceptions, meaning the machine is left in a well-defined state — as if it had cleanly stopped at the faulting instruction — so the OS can handle the exception and safely resume. What was missing was a way to describe these non-sequential exception behaviors at PDL's high level, easily and safely, while still compiling to an efficient pipeline that preserves the OIAT guarantee and makes the exceptions precise.
This paper's idea

Add pipeline exceptions, like try-throw-catch, checked statically

XPDL extends PDL with a new language feature, pipeline exceptions, that gives hardware exceptions a first-class, high-level abstraction. A pipeline exception can describe the final, atomic, exception-handling operations of a pipeline — the flush, the CSR writes, the rollback — as one coherent construct rather than logic smeared through the normal instruction flow. Crucially, its syntax is deliberately familiar: it looks like the try, throw, and catch of software exception handling, which programmers already understand, even though nothing like it existed in hardware languages before (high-level synthesis languages ignore complex control paths, and low-level HDLs cannot reason about high-level behaviors like exceptions). From this one abstraction, a designer can implement the whole variety of real hardware exceptions — traps, interrupts, and the rest. The key to making this safe is that the XPDL compiler preserves PDL's one-instruction-at-a-time semantics through static checking: a set of checking rules ensures that even with exceptions, the generated pipeline still behaves as if instructions ran sequentially, which in turn makes it easy to implement exceptions that are precise. XPDL is built on the open-source PDL compiler and evaluated on RISC-V processor designs. The generated pipelines support exceptions with no impact on cycles per instruction, less than a 3.3 percent decrease in maximum clock frequency, and reasonable area overhead — so the abstraction costs essentially nothing in performance.

Why this problem is worth solving

Raising the level of abstraction for processor design only matters if the resulting designs can run real software, and real software means an operating system, which means exceptions.

The promise of a language like PDL is enormous: hardware design is notoriously error-prone precisely because pipelines are parallel and the designer must manually keep a parallel implementation consistent with a sequential architecture. A high-level sequential language that compiles to an efficient pipeline removes a whole class of bugs and makes exploring design alternatives far easier, at little performance cost. But a processor that cannot handle interrupts, traps, and faults is not a real processor — it cannot run an operating system, cannot be preempted, cannot recover from a page fault or a system call, cannot be used for anything beyond a toy. So exceptions are not a peripheral feature; they are the boundary between a research demonstration and a design that could actually be deployed. Bringing them into the high-level language is therefore what makes the whole approach viable, because it lets the productivity and correctness benefits of sequential specification extend to the parts of a processor that are hardest to get right and most essential for systems software. And because exceptions must be precise for an OS to function safely, doing this in a way that guarantees precision — rather than leaving it to error-prone manual encoding — directly attacks one of the trickiest correctness problems in processor design. The value is unlocking high-level, reason-about-able CPU design for machines that can actually run real code.

The key realization is that an inherently non-sequential event can still be given a clean sequential meaning if the language provides the right atomic abstraction and the compiler enforces it.

Exceptions look like the natural enemy of a one-instruction-at-a-time model: they are global, abrupt, and reach across all the in-flight instructions to flush and reset the pipeline. It is tempting to conclude they simply cannot be expressed sequentially. XPDL’s insight is that they can, if you introduce an abstraction whose job is precisely to capture “this is the final, atomic thing that happens, out of band.” A pipeline exception is that abstraction: it names the exceptional, all-at-once behavior as a distinct construct rather than trying to disguise it as ordinary instruction flow, and it borrows the try-throw-catch shape from software because that shape is exactly designed to describe control that leaps out of the normal path to a handler. This gives the designer something intuitive to write. But intuition is not enough for correctness, and here the compiler does the heavy lifting: static checking rules verify that, however the designer uses pipeline exceptions, the generated hardware still preserves OIAT semantics. That is what makes precision fall out almost for free — if the pipeline provably behaves as if instructions ran one at a time, then an exception cleanly delimits which instructions completed and which did not, which is the definition of a precise exception. The deep move is to keep the reasoning sequential even for a non-sequential feature, by making the language express the exception atomically and the compiler guarantee the semantics. That is what turns a feature that was awkward and unsafe to encode by hand into one that is easy and correct by construction.

What people did before, and where it broke

Write pipelines in RTL (Verilog). Describe the concurrent hardware directly. Where it broke. Manually keeping a parallel pipeline consistent with a sequential ISA is error-prone and hard to reason about, especially for exceptions.
Use PDL’s sequential specification. Write one-instruction-at-a-time and let the compiler build the pipeline. Where it broke. PDL has no feature for hardware exceptions, which operating systems require.
Encode exceptions with PDL’s existing constructs. Thread the flush, CSR writes, and rollback through the normal instruction flow. Where it broke. Exceptions are non-sequential and global, so encoding them this way is awkward, inefficient, and easy to get wrong.
Use high-level synthesis or low-level HDLs for the exception logic. Borrow tools from other hardware-design flows. Where it broke. High-level synthesis languages do not handle complex control paths, and low-level HDLs cannot reason about high-level behaviors like exceptions.
The gap. No high-level sequential hardware language offered a safe, expressive abstraction for hardware exceptions that compiles to an efficient pipeline while guaranteeing the exceptions are precise.

How XPDL works

From a sequential spec with no exceptions to precise, checked pipeline exceptions

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Describe the processor at a high, sequential level and let the compiler build the pipeline. XPDL inherits PDL’s foundation: the designer writes a sequential, reason-about-able specification, and the tool synthesizes the parallel hardware, so the productivity and clarity of a high-level language reach processor design. Raising hardware description above the concurrent register-transfer level to a higher-level, more analyzable language that the compiler lowers to efficient hardware is the same enterprise the work on functional hardware description with latency-insensitive interfaces (ShakeFlow) covered elsewhere on this site pursues, letting designers think at a higher level while the compiler handles the timing. XPDL extends that high-level approach to the exception behavior that such languages had left out.

Give a hard hardware feature a safe abstraction the compiler enforces. XPDL wraps the messy, non-sequential business of exceptions in a clean try-throw-catch construct and uses static-checking rules to guarantee the design stays correct, so a dangerous feature becomes easy and safe to write. Providing a high-level language abstraction for a subtle hardware behavior and using static checking to prevent the designer from violating its correctness invariants is the same principle the work on type-stated hardware peripherals for driver correctness (Abacus) covered elsewhere on this site is built on, turning a hazardous low-level concern into a compile-time-checked one. XPDL applies this to precise exceptions, where the invariant is one-instruction-at-a-time semantics.

Get a strong correctness guarantee statically, without heavyweight proof. XPDL’s static-checking rules deliver the OIAT guarantee — and hence precise exceptions — by construction, rather than requiring the designer to verify the pipeline after the fact. Obtaining a real correctness guarantee through lightweight, compiler-integrated static checking instead of a separate, expensive verification effort is the same trade-off the work on lightweight modular verification for compiled code (lightweight modular verification) covered elsewhere on this site strikes, making rigorous guarantees practical to obtain. XPDL bakes the precision guarantee into the compilation of the high-level specification.

Following an exception through XPDL

Compiling and handling a precise hardware exception

A trace, drawn from the paper, of how XPDL turns a high-level pipeline exception into correct pipeline hardware.

Step 1 of 5

The designer writes the processor sequentially

In XPDL, the processor is specified one instruction at a time, as in PDL, with the pipeline stages described as a straight-line flow through fetch, decode, execute, memory, and writeback.

The compiler will generate the parallel pipeline from this.

Why it works

An atomic construct captures what sequential flow cannot. Exceptions are global and abrupt, unlike ordinary instruction flow → but naming them as a distinct final, atomic pipeline-exception construct → so the non-sequential behavior is expressed directly instead of awkwardly disguised.
A familiar shape makes a hard feature writable. Hardware languages had no abstraction for exceptions → but borrowing software’s try-throw-catch form → so designers can express traps and interrupts intuitively at a high level.
Static checking keeps the reasoning sequential. Adding exceptions could break the one-at-a-time guarantee → but compiler rules that verify OIAT is preserved → so the design stays reason-about-able even with exceptions.
OIAT preservation makes precision almost automatic. Getting precise exceptions by hand is error-prone → but a pipeline that provably behaves sequentially → so an exception cleanly delimits completed and un-executed instructions, which is precision.
The abstraction compiles to efficient hardware. A high-level feature could add overhead → but the compiler synthesizes tight pipeline logic → so exceptions cost no extra cycles per instruction and under 3.3 percent frequency.

What it costs (trade-offs and scope)

There is minor frequency and area overhead. Supporting exceptions adds hardware, so XPDL pays under a 3.3 percent decrease in maximum frequency and some area, though no cycles-per-instruction penalty.
It extends a specific language and toolchain. XPDL builds on PDL and its open-source compiler; the benefits accrue to designs written in this high-level sequential language, not to arbitrary RTL codebases.
The guarantee is scoped to what the checking rules cover. Precision follows from the static preservation of one-instruction-at-a-time semantics; the strength of the guarantee is bounded by the rules and the semantics they enforce.
It targets processor pipelines. The abstraction is about hardware exceptions in pipelined processors; it is not a general hardware-design methodology for arbitrary accelerators, and its value is tied to CPU design usable by operating systems.
Reported figures are on RISC-V designs. The no-CPI-impact, sub-3.3-percent-frequency, and area results are measured on the paper’s RISC-V processor designs; other ISAs, pipelines, or exception mixes may differ.

The comparison

Expressing hardware exceptions in a processor design

Property	RTL (Verilog)	PDL without exceptions	XPDL
Design level
Supports hardware exceptions
How exceptions are written
Precision guarantee
Performance cost

A comparison of ways to express hardware exceptions in a processor design. RTL supports them but by error-prone hand-written control; PDL raises the abstraction to a sequential specification but has no exception feature at all. XPDL adds pipeline exceptions with a familiar try-throw-catch syntax and static checking that preserves one-instruction-at-a-time semantics, so precise exceptions are synthesized from a high-level spec with no cycles-per-instruction penalty and under 3.3 percent frequency overhead on RISC-V. Exact figures should be read from the paper.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ hosted copy at cs.cornell.edu). The described system is the paper’s: XPDL extends the PDL hardware description language to support hardware exceptions. PDL compiles a high-level sequential specification of a processor into an efficient pipelined implementation while guaranteeing one-instruction-at-a-time (OIAT) semantics. XPDL adds “pipeline exceptions,” a language feature that describes the final, atomic, exception-handling operations of a pipeline (flushing, writing Control and Status Registers, rolling back transient effects, resetting pipeline state), with a lightweight syntax similar to software try-throw-catch; from this abstraction a designer can implement traps, interrupts, and other hardware exceptions. The XPDL compiler preserves OIAT semantics through static-checking rules, which makes it easy to implement precise exceptions (leaving the processor in a well-defined, resumable state). XPDL is implemented on the open-source PDL compiler and evaluated on RISC-V processor designs; the paper reports that pipelines with exceptions have the same cycles per instruction, less than a 3.3 percent decrease in maximum frequency, and reasonable area overhead, and argues the implementation preserves PDL’s OIAT semantics. The background above on pipelining, ISAs, RTL versus high-level HDLs, OIAT semantics, precise exceptions, and CSRs is standard context provided to make the approach intuitive. The step-by-step walkthrough is an illustration of the described mechanism. The exact language design, the static-checking rules, and the full evaluation should be read from the paper.

Background

Why hardware design keeps borrowing the abstractions of programming languages

It helps to see XPDL within a long-running convergence between hardware design and programming languages. Designing hardware has traditionally meant thinking at the register-transfer level, wiring up concurrent logic by hand — powerful but punishing, because the human must hold the whole parallel behavior in mind and keep it consistent with a much simpler intended meaning. The recurring insight, borrowed from decades of software language design, is that raising the level of abstraction and letting a compiler bridge down to the hardware removes whole classes of bugs and makes designs easier to explore and to trust. This has produced higher-level hardware languages, high-level synthesis, and type systems and static checks that enforce correctness properties by construction rather than by after-the-fact verification. XPDL is a striking instance because it imports one of software’s most familiar control abstractions — exception handling with try, throw, and catch — into hardware, for the very feature that most resists a clean sequential description. What makes it work is the same thing that makes such borrowings work in general: pairing an intuitive high-level construct with a compiler that statically guarantees the low-level implementation respects the intended semantics. This effort to make hardware description more like high-level programming, with the compiler synthesizing efficient circuits from an abstract, checkable description, is the same terrain the work on a hierarchical dataflow compiler for high-level synthesis (HIDA) covered elsewhere on this site occupies, lifting hardware design toward software-like abstraction. XPDL’s particular contribution is to bring precise hardware exceptions — the gateway to operating-system support — into a high-level sequential language, safely and at almost no performance cost.

If you remember only three things

1. Pipelined processors are inherently parallel — several instructions in flight per cycle — yet the ISA they implement is sequential, which makes them hard to design and reason about in a traditional register-transfer-level language. PDL bridges this by letting designers write a high-level, one-instruction-at-a-time sequential specification and compiling it into an efficient pipeline that provably behaves sequentially (one-instruction-at-a-time, or OIAT, semantics), with performance comparable to hand-written RTL. But PDL could not express hardware exceptions — interrupts, traps, faults — which operating systems require, because these are inherently non-sequential: they flush the pipeline, write control and status registers, roll back transient effects, and reset state, none of which fits the smooth one-at-a-time flow. Encoding them with PDL's existing constructs was awkward and inefficient, and getting them wrong is dangerous because modern processors must provide precise exceptions.
2. XPDL extends PDL with pipeline exceptions, a first-class language feature that names the final, atomic, exception-handling operations of the pipeline as one coherent construct, with a lightweight syntax modeled on software's familiar try-throw-catch — an abstraction novel in hardware languages. From it, designers implement the full range of hardware exceptions at the high level without hand-wiring the flush and rollback. The key to safety is that the XPDL compiler preserves OIAT semantics through static-checking rules: because the generated pipeline provably still behaves as if instructions ran one at a time, precise exceptions (which leave the machine in a well-defined, resumable state) follow almost for free. The deep move is to keep the reasoning sequential even for a non-sequential feature, by expressing the exception atomically and having the compiler guarantee the semantics.
3. Implemented on the open-source PDL compiler and evaluated on RISC-V designs, XPDL generates pipelines that support exceptions with no change in cycles per instruction, less than a 3.3 percent decrease in maximum clock frequency, and reasonable area overhead, while preserving PDL's OIAT semantics — so the high-level abstraction costs essentially nothing in performance. The trade-offs and scope: there is minor frequency and area overhead, it extends the specific PDL language and toolchain rather than arbitrary RTL, its precision guarantee is scoped to what the static-checking rules enforce, and it targets pipelined-processor design usable by operating systems. This explainer is based on the paper's full text.

Check yourself

Check your understanding

1. What does PDL do, and why is it appealing for processor design?
2. Why are hardware exceptions hard to express in a sequential language like PDL?
3. What is XPDL's key idea, and how does it keep exceptions correct?
4. What does XPDL achieve, and what are the limits of the approach?

Sources

The paper is “Sequential Specifications for Precise Hardware Exceptions” by Yulun Yao, Drew Zagieboylo, Andrew C. Myers, and G. Edward Suh (Cornell University and NVIDIA), published at ASPLOS 2026, DOI 10.1145/3760250.3762233. A full-text copy is hosted by the authors at cs.cornell.edu.

This explainer is written from the paper’s full text (the authors’ hosted copy). XPDL extends the PDL hardware description language — which compiles a high-level sequential processor specification into an efficient pipeline while guaranteeing one-instruction-at-a-time (OIAT) semantics — to support hardware exceptions. It introduces “pipeline exceptions,” a language feature with a lightweight try-throw-catch syntax that describes the atomic exception-handling operations of a pipeline, from which designers implement traps, interrupts, and other hardware exceptions. The XPDL compiler preserves OIAT semantics through static-checking rules, making it easy to implement precise exceptions. Evaluated on RISC-V, the paper reports no change in cycles per instruction, under a 3.3 percent decrease in maximum frequency, and reasonable area overhead. Background on pipelining, OIAT semantics, precise exceptions, and CSRs is standard context. The numbers are the paper’s own; exact mechanisms and full results should be confirmed in the paper.