Anvil: A General-Purpose Timing-Safe Hardware Description Language

Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson and Prateek Saxena

In a hardware description language, a signal is stateless — its value follows the registers it depends on — so if a designer needs a value (say a memory address) to stay constant while a multi-cycle operation runs, they must manually make sure nothing changes the underlying register in the meantime; forgetting is a timing hazard, a bug mainstream languages like Verilog and Chisel never catch until simulation, which can even open time-of-check-to-time-of-use security holes; this paper (National University of Singapore — Jason Zhijingcheng Yu, Prateek Saxena, and colleagues) presents Anvil, a general-purpose HDL whose novel type system statically guarantees timing safety — using Rust-like ownership so a register cannot be mutated while a value it feeds is still needed — without giving up cycle-level control or data-dependent timing, at only about 4.50 percent area and 3.75 percent power overhead versus SystemVerilog.

The argument in one glance

Problem

A value that is supposed to hold still can silently change underneath you

Hardware is described in a hardware description language (HDL) such as Verilog or Chisel, and hardware has two kinds of values that software does not distinguish. A register stores a persistent value and can be given a new value every clock cycle. A signal is stateless: it has no memory of its own, and its value is simply whatever its underlying registers currently produce. This matters because designers often need a value to stay constant for several cycles — for example, a memory address must hold still while a lookup that takes two cycles completes. But a signal carrying that address will change the instant its underlying register is written. So the designer must manually guarantee that nothing mutates the register during the whole window the value is needed. Forgetting to do so is a timing hazard: the value the hardware uses at the end is not the value it started with. These hazards are common even among expert designers, they hide in widely used open-source hardware, and they can even be exploited like a time-of-check-to-time-of-use flaw, where a value is checked and then changed before it is used.
What people did

Track timing by hand, or verify designs after the fact

The usual defenses are manual care and after-the-fact checking. Designers reason carefully about which registers must stay stable and when, keeping the timing in their heads or in comments. When bugs slip through, they hunt them down in simulation, or apply separate formal verification tools to a finished design to try to prove particular timing properties hold.
Why it fell short

HDLs give no help at compile time, and verification trades away flexibility

None of this is caught by the language itself. Mainstream HDLs — Verilog, VHDL, Chisel — lack any abstraction for a value that must remain unchanged over multiple cycles, so they delegate the entire responsibility to the designer and do not flag timing hazards at compile time. Bugs are discovered only in simulation, if at all, which is why designers so often ask for help with these issues and why the hazards persist in shipped hardware. The problem is made worse by concurrency: a hardware design is many modules running in parallel and communicating, so one module can mutate a register while another still depends on it. Separate verification tools can check a specific design, but they are effortful, applied after the fact, and to make the analysis tractable they often assume worst-case fixed delays — sacrificing the flexibility of data-dependent, dynamic timing that real designs use. What is missing is a language that rules out timing hazards by construction, at compile time, while still allowing precise cycle-level control and dynamic timing.
This paper's idea

A type system that forbids mutating a register while its value is still needed

Anvil is a general-purpose hardware description language whose novel type system statically guarantees timing safety — the absence of timing hazards — without sacrificing expressiveness for cycle-level timing control or dynamic timing behaviour. It is, as far as the authors know, the only HDL to guarantee this. Rather than hiding the difference between signals and registers the way many high-level synthesis languages do, Anvil's type system exposes it and captures the timing relationship between register mutations and signal uses. The key idea is to give every value carried by a signal a lifetime, bounded by a start event and an end event, during which the value must stay unchanged. The type system then enforces, in the spirit of Rust's ownership and borrowing, that a register cannot be assigned a new value while a value depending on it is still within its lifetime — attempting to do so is a compile-time error ("assignment to a loaned register"). Modules communicate over channels governed by timing contracts that encode when shared values are valid, and these contracts can be parametric on abstract time points that vary at run time, so the type system can statically express dynamic, data-dependent timing rather than only fixed cycle counts. Everything is checked statically and compiles to ordinary hardware; Anvil is open-source, has been used to build timing-sensitive designs including a RISC-V CPU, and on a commercial 22-nanometer process costs only about 4.50 percent more area and 3.75 percent more power than SystemVerilog.

Why this problem is worth solving

Timing hazards are a whole class of hardware bugs that current languages simply do not help with, and hardware bugs are permanent once a chip is made.

In software, values are persistent: a variable holds what you stored until you change it. Hardware is different, and hardware description languages make a distinction with no software equivalent. A register is like a memory cell — it holds a value and can be overwritten each clock cycle. A signal is stateless — it is just a wire whose value is continuously whatever its source registers currently drive, so it changes the moment those registers change. Designs constantly need a value to stay put for a while: an address held steady across a multi-cycle memory access, an operand kept constant while a multi-cycle computation runs, a request valid until it is acknowledged. But because a signal has no memory, keeping its value stable really means keeping every register it depends on unmutated for the whole duration — a duty the language places entirely on the designer. Get the window wrong by even one cycle and the hardware quietly uses a value that changed mid-operation. Because a fabricated chip cannot be patched, and because these hazards are subtle, concurrent, and invisible to the compiler, catching them matters far more than the equivalent slip would in software.

The reason existing tools fall short is that the language stays silent and verification comes too late and too rigid.

Mainstream HDLs such as Verilog, VHDL, and Chisel have no built-in notion of a value that must remain unchanged over multiple cycles, so they cannot warn you when you violate that expectation; the design compiles, and the hazard only shows up as wrong behaviour in simulation — or never, if the simulation does not happen to exercise it. This is why timing hazards are common even among experienced designers and end up in widely used open-source components. Concurrency compounds the danger: a real design is a swarm of modules executing in parallel and exchanging signals, so a register you assumed was stable can be mutated by another module while you still depend on it, much like a data race. The alternative, applying formal verification after the design is written, does catch specific properties, but it is a separate, effortful step layered onto a finished design, and to keep the analysis feasible it commonly assumes worst-case fixed timing — which forces designers to give up the data-dependent, dynamic latencies that make hardware efficient. What is genuinely needed is for the design language itself to prevent the hazard as you write, while still letting you express precise and dynamic timing, which is the gap Anvil fills.

What people did before, and where it broke

Track timing by hand in mainstream HDLs. Reason carefully about which registers must stay stable and for how long, keeping the timing discipline in the designer’s head. Where it broke. Verilog, VHDL, and Chisel offer no abstraction for a multi-cycle-stable value and no compile-time check, so a one-cycle mistake becomes a silent timing hazard that appears only in simulation, if at all.
Find the bugs in simulation. Run the design in a simulator and watch for wrong results caused by mistimed values. Where it broke. Simulation only catches hazards it happens to exercise, so many slip through into shipped hardware, and concurrency makes the triggering interleavings easy to miss.
Verify the finished design formally. Apply a separate verification tool to prove particular timing properties of a completed design. Where it broke. It is effortful and after-the-fact, and to stay tractable it often assumes worst-case fixed delays, sacrificing the dynamic, data-dependent timing that efficient hardware relies on.
Hide the signal/register difference (high-level synthesis). Use a higher-level language that abstracts away registers versus signals entirely. Where it broke. Abstracting the distinction away removes the designer’s cycle-level timing control, which many performance-critical designs need, and it does not expose the timing relationships needed to reason about safety precisely.
The gap. No general-purpose HDL prevented timing hazards by construction at compile time while still exposing signals and registers and supporting precise, dynamic, cycle-level timing.

How Anvil works

Making register mutations and signal lifetimes checkable at compile time

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

The idea

Guarantee the property at compile time with a type system, not by discipline. Anvil’s foundational choice is to make timing safety a static property the compiler enforces, so a timing hazard becomes a type error you cannot ignore rather than a bug you hope to catch later. Turning a safety property into something a type system proves at compile time, so whole classes of errors are ruled out by construction, is the same philosophy the work on verifying a Rust implementation of page tables in a software enclave hypervisor covered elsewhere on this site is built on, using static guarantees to make a critical component correct rather than merely tested. Anvil brings that guarantee-by-construction mindset into hardware description, and even borrows Rust’s ownership idea directly to do it.

Catch the bug as you design, not in simulation afterward. The whole point of Anvil is to move detection from late, incidental discovery to the moment of writing, refusing to compile a design that could suffer a timing hazard. Shifting the discovery of hardware bugs earlier and making it systematic, instead of relying on simulation to stumble onto them, is the same goal the work on scaling symbolic execution of hardware designs covered elsewhere on this site pursues, exploring a design to surface its bugs before it is trusted. Where that approach analyzes a design after it exists, Anvil prevents the class of bug in the language itself, so the hazard never reaches simulation at all.

Improve the hardware design language so correctness is built in. Anvil is fundamentally a language-level answer: it argues that the right place to fix timing hazards is the HDL, by adding the missing abstraction for multi-cycle-stable values. Treating the correctness of hardware design code as something to address at the source-language level rather than downstream is the same instinct the work on automatically repairing defects in hardware design code covered elsewhere on this site follows, targeting the design description where the bugs live. Anvil does it preventively — designing the language so the defect cannot be written in the first place, instead of repairing it afterward.

Following a two-cycle memory lookup through Anvil

Keeping an address stable while a memory access completes

A trace, drawn from the paper's examples, of how Anvil catches a timing hazard that mainstream HDLs would miss.

Step 1 of 5

A design issues a memory request that takes two cycles

A module sends an address to a memory subsystem and expects the result two cycles later. For the lookup to be correct, the address value must stay constant across both cycles — but the address is a signal driven by an underlying register.

The address must remain unchanged for the whole request-to-response window.

Why it works

A lifetime makes the must-hold-still window visible to the compiler. A signal’s stability requirement is normally implicit → but tagging each carried value with a start and end event makes it explicit → so the type system can reason about exactly when a register must not change.
Ownership turns a timing hazard into a type error. The hazard is caused by mutating a register whose value is still needed → but treating that register as loaned during the value’s lifetime forbids the mutation → so the dangerous action is a compile-time error rather than a silent bug.
Exposing signals versus registers enables precise reasoning. Hiding the distinction would lose the information needed to check timing → but Anvil keeps registers and signals distinct and tracks their dependencies → so it can pinpoint the exact mutation that would break a value in use.
Timing contracts make dynamic latency statically checkable. Fixed worst-case delays sacrifice efficiency → but contracts parametric on abstract, run-time-varying time points express data-dependent timing → so Anvil verifies safety without giving up dynamic behaviour.
Static checking means no run-time cost to the guarantee. The safety is proven before synthesis → so the generated hardware needs no run-time checks → so timing safety adds only about 4.50 percent area and 3.75 percent power versus SystemVerilog.

What it costs (trade-offs and scope)

The type system constrains how you write hardware. Guaranteeing timing safety statically means Anvil must reject some designs it cannot prove safe, and designers must express lifetimes and timing contracts explicitly; this is more upfront structure than an unchecked HDL demands, in exchange for the guarantee.
It is a new language, not an extension of Verilog. Adopting Anvil means writing in a new HDL with a novel type system, though its output integrates into existing codebases in other HDLs; teams still face a learning curve and the cost of introducing another language.
Timing safety is not full functional correctness. Anvil rules out timing hazards specifically — values changing when they should stay stable — but a design can still be functionally wrong in ways the type system does not address; it is one important safety property, not a proof the hardware does the right thing.
The compiler is an early-stage prototype. The authors describe Anvil’s compiler as an early prototype; the reported small area and power overheads (about 4.50 percent and 3.75 percent on a 22-nanometer process versus SystemVerilog) are promising but come from that prototype on the designs evaluated, and may change as the tooling matures.
Benefits depend on the designs and baselines measured. The overhead and expressiveness results come from implementing timing-sensitive designs, including a RISC-V CPU, and comparing against open-source SystemVerilog; other designs, styles, or baselines could behave differently.

The evaluation

Preventing timing hazards in hardware design

Property	Mainstream HDL (Verilog, Chisel)	Post-hoc formal verification	Anvil
Catches timing hazards at compile time
Exposes cycle-level timing control
Supports dynamic, data-dependent timing
Effort model
Synthesis cost

A comparison of ways to avoid timing hazards. Anvil is, to the authors' knowledge, the only HDL that guarantees timing safety statically while keeping cycle-level and dynamic timing control, adding only about 4.50 percent area and 3.75 percent power over SystemVerilog on a commercial 22-nanometer process, demonstrated on timing-sensitive designs including a RISC-V CPU.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 (arXiv:2503.19447). The mechanism described is the paper’s: Anvil is a general-purpose hardware description language whose novel type system statically guarantees timing safety (the absence of timing hazards) without sacrificing expressiveness for cycle-level or dynamic timing. Timing hazards arise because HDLs distinguish stateless signals from persistent registers, and a signal expected to remain constant across cycles can change if its underlying register is mutated; mainstream HDLs (Verilog, VHDL, Chisel) do not catch these at compile time and they can behave like time-of-check-to-time-of-use flaws. Anvil exposes the signal/register distinction rather than hiding it, gives each value carried by a signal a lifetime bounded by a start and end event during which it must stay unchanged, and enforces (in the spirit of Rust’s ownership and borrowing) that a register cannot be mutated while a value depending on it is still within its lifetime, reporting a compile-time error otherwise. Modules communicate over channels with timing contracts that can be parametric on abstract, run-time-varying time points, allowing dynamic timing to be expressed and checked statically. The authors implemented Anvil (an early-stage prototype compiler), used it for timing-sensitive designs including a RISC-V CPU, synthesized on a commercial 22-nanometer ASIC process, and report about 4.50 percent area and 3.75 percent power overhead versus SystemVerilog, with no cycle-level latency overhead; Anvil is open-source. Exact type-system rules, the full design set, and complete results should be read from the paper.

Background

Why hardware design is borrowing ideas from programming languages

It helps to see Anvil as part of a broader movement to bring modern programming-language ideas — strong type systems, static guarantees, ownership — into hardware design, a field long dominated by low-level languages that catch almost nothing at compile time. Software went through this shift decades ago: type systems, memory-safe languages, and ownership models like Rust’s turned entire categories of bugs from run-time disasters into compile-time errors. Hardware has been slower to follow, partly because its concurrent, cycle-accurate, stateful nature is genuinely harder to reason about, and partly because the incumbent languages are entrenched. Yet the stakes are higher: a hardware bug cannot be hot-fixed once silicon is fabricated, and hardware increasingly sits at the root of security. So there is growing effort to make hardware design languages and tools enforce correctness rather than merely describe circuits, whether by verification, by better intermediate representations, or by richer type systems. The broader push to bring rigorous, formal correctness guarantees to hardware circuits, rather than trusting simulation, is the same direction the work on formally verified dataflow circuit rewrites covered elsewhere on this site takes, proving hardware transformations correct instead of testing them. Anvil pushes this into the design language itself, showing that a Rust-inspired type system can eliminate a pervasive class of hardware bugs by construction, cheaply enough to be practical.

If you remember only three things

1. Hardware description languages distinguish registers (persistent, writable each cycle) from signals (stateless, following their registers). When a designer needs a signal value to stay constant across several cycles — like a memory address during a multi-cycle lookup — they must manually ensure the underlying register is not mutated in that window. Forgetting is a timing hazard: the hardware silently uses a value that changed mid-operation. Mainstream HDLs (Verilog, VHDL, Chisel) offer no abstraction for this and do not catch it at compile time, so it surfaces only in simulation, persists in real hardware, and can act like a time-of-check-to-time-of-use security flaw.
2. Anvil is a general-purpose HDL whose novel type system statically guarantees timing safety without giving up cycle-level or dynamic timing control — the only HDL the authors know of to do so. It exposes the signal-versus-register distinction, gives each carried value a lifetime bounded by a start and end event during which it must stay unchanged, and, borrowing Rust's ownership and borrowing, forbids mutating a register while a value it feeds is still live (a compile-time "assignment to a loaned register" error). Modules compose via channels with timing contracts that can be parametric on run-time-varying time points, so dynamic, data-dependent timing is expressed and checked statically.
3. All checks are static and Anvil compiles to ordinary synthesizable hardware. It is open-source, was used to build timing-sensitive designs including a RISC-V CPU, and on a commercial 22-nanometer process adds only about 4.50 percent area and 3.75 percent power over SystemVerilog with no cycle-level latency penalty. The trade-offs: it is a new language with a learning curve, its type system rejects some designs it cannot prove safe, timing safety is not full functional correctness, and the compiler is an early-stage prototype.

Check yourself

Check your understanding

1. What is a timing hazard, and why do mainstream HDLs make it easy to introduce?
2. How does Anvil guarantee timing safety?
3. How does Anvil support dynamic (data-dependent) timing without giving up its static guarantee?
4. Predict: a designer writes an Anvil module that sends a request and, to save a cycle, updates the request register before the acknowledgement comes back. What happens, and why?

Sources

The paper is “Anvil: A General-Purpose Timing-Safe Hardware Description Language” by Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson, and Prateek Saxena (National University of Singapore), published at ASPLOS 2026, DOI 10.1145/3779212.3790125.

This explainer is written from the paper’s full text (arXiv:2503.19447). Expressing hardware in HDLs involves stateless signals whose values follow their underlying registers, and unintended behaviour (a timing hazard) arises when a register is mutated while a dependent signal is expected to remain constant across cycles; such hazards are common because existing HDLs lack abstractions for values that stay unchanged over multiple clock cycles, delegating the responsibility to designers, and can even expose time-of-check-to-time-of-use attacks. Anvil is a general-purpose HDL whose novel type system statically guarantees timing safety (absence of timing hazards) without sacrificing expressiveness for cycle-level or dynamic timing. Unlike high-level synthesis languages that abstract away the difference between registers and signals, Anvil exposes it and captures the timing relationships between register mutations and signal uses; it assigns each value carried by a signal a lifetime bounded by a start and end event during which the value must stay unchanged, and enforces, in the spirit of Rust’s ownership and borrowing, that a register cannot be assigned while a value depending on it is still within its lifetime (a compile-time error). Timing contracts on channels can be parametric on abstract, run-time-varying time points, allowing dynamic timing to be expressed and statically checked, and enabling safe composition of communicating modules. The authors implemented Anvil (an early-stage prototype), used it for timing-sensitive designs including a RISC-V CPU, synthesized on a commercial 22-nanometer ASIC process, and report about 4.50 percent area and 3.75 percent power overhead versus SystemVerilog, with no cycle-level latency overhead; Anvil is open-source at github.com/jasonyu1996/anvil. No numbers beyond the paper’s own have been introduced; exact type-system rules, the full design set, and complete results should be confirmed in the paper.