Hassert: Hardware Assertion-Based Verification Framework with FPGA Acceleration

Ziqing Zhang, Weijie Weng, Yaning Li, Lijia Cai, Haoyu Wang, David Boland and 2 others

Verifying a chip design is the slowest part of building it, because you run the design in a software simulator that crawls, and the assertions engineers write to catch bugs make it crawl even more — but running the design on an FPGA is fast yet nearly blind when something goes wrong; this paper (Institute of Computing Technology, CAS, with Sydney) builds Hassert, which compiles those assertions into real circuitry that runs on the FPGA alongside the design, swaps assertions in and out at runtime without recompiling, and, the moment an assertion fires, snapshots the whole hardware state and ships it to a software simulator so you get both the FPGA's speed and the simulator's full-visibility debugging.

The argument in one glance

Problem

Verifying a chip is slow, and the checks that find bugs make it slower

Before a chip is built, its design must be verified: run it on many inputs and confirm it behaves correctly. This verification is the bottleneck of the whole development cycle, eating a large fraction of the effort, and the reason is speed. The standard tool is a software simulator that executes the design at the register-transfer level, and for a large design it crawls — well under the speeds real hardware reaches. Engineers make the simulator smarter by adding assertions: small formal checks woven through the design that watch internal signals and fire the instant something unexpected happens, which is invaluable for catching and localizing bugs. But every assertion the simulator must evaluate slows it down further, so the very technique that improves observability deepens the speed problem. The result is a painful trade-off: thorough, assertion-rich verification is exactly the kind that takes the longest to run.
What people did

Run the design on an FPGA instead of a simulator

The obvious way to go faster is to stop simulating and start running: map the design onto an FPGA, a reconfigurable chip that executes the actual hardware, which is orders of magnitude faster than software simulation and can push far more test cases through the design.
Why it fell short

FPGAs are fast but nearly blind when a bug hits

The FPGA solves speed but loses visibility. Assertions are not synthesizable — they are checking constructs, not real circuits, so they cannot simply be dropped onto the FPGA. And when something does go wrong on hardware, the debugging tools are meager: a probe like an integrated logic analyzer can watch only a handful of signals, and testing a different signal means recompiling the entire FPGA design, which is slow. So engineers end up seeing that a test failed on the FPGA but not why, and have to reproduce the failure back in the slow software simulator to trace the root cause, forfeiting the speed they gained.
This paper's idea

Put the assertions on the FPGA, and snapshot into a simulator when one fires

Hassert combines the FPGA speed with the simulator visibility. A compiler turns the unsynthesizable assertions into equivalent real circuits that run on the FPGA next to the design, so checks execute at hardware speed. Assertions can be swapped in and out at runtime by partially reconfiguring the FPGA, without recompiling the design. And the moment an assertion fires, Hassert takes a snapshot of the entire FPGA hardware state and ships it to a software simulator, which replays from that point with full, fine-grained visibility — giving both the speed of hardware and the debuggability of simulation.

Why this problem is worth solving

The technique at the center is one the whole industry relies on, and its cost is exactly what limits it.

Assertion-based verification is the practice of embedding formal checks, called assertions, throughout a hardware design to state properties that must always hold — for example, that a request is always eventually acknowledged, or that two control signals are never high at once. Written in a language like SystemVerilog Assertions, they act as always-watching probes on internal signals, automatically flagging the moment a design violates an expected behavior, which gives engineers far better visibility into microarchitectural detail than watching outputs alone and helps pinpoint where a bug is. It is widely adopted because it turns silent, hard-to-find misbehavior into an immediate, localized alarm. The catch is where the assertions run. In a software simulator, every assertion is extra work the simulator performs each cycle, so a design rich in assertions — the kind that verifies thoroughly — simulates even more slowly than a bare design, and for large designs that is already the bottleneck. Assertions are also not synthesizable: they are checking constructs, not hardware, so they cannot be placed directly on an FPGA to run fast. That mismatch is the gap Hassert sets out to close.

The alternative to simulation trades one scarce resource for another.

An FPGA is a chip whose logic can be reconfigured to implement an arbitrary digital design, so a hardware design can be mapped onto it and run as real circuitry at speeds orders of magnitude faster than a software simulator managing the same design. This makes FPGA prototyping attractive for pushing large volumes of test cases through a design quickly. Its weakness is observability: when a test fails, you can see the failure but very little of the internal state that caused it. On-chip debug probes such as integrated logic analyzers can capture only a small number of signals chosen in advance, and changing which signals you watch requires recompiling the whole FPGA bitstream, a slow step. So FPGA prototyping is fast but nearly blind, and engineers routinely have to reproduce a hardware failure back in the slow simulator to actually diagnose it — losing the speed advantage exactly when they most need both speed and insight. Bridging that divide, keeping the FPGA’s speed while regaining the simulator’s visibility, is what makes a framework like Hassert valuable.

What people did before, and where it broke

Verify in a software RTL simulator. Run the design cycle-accurately in software, with full visibility into every signal and mature debugging tools. Where it broke. It is extremely slow for large designs, far below hardware speeds, and adding assertions to verify thoroughly makes it slower still, so verification becomes the development bottleneck.
Prototype the design on an FPGA. Map the real hardware onto an FPGA and run test cases at hardware speed. Where it broke. Assertions are not synthesizable so they cannot run there directly, and when a bug appears the FPGA offers almost no fine-grained visibility; probes see only a few preselected signals and changing them means a full recompile.
Add on-chip debug probes to the FPGA. Instrument the FPGA with a logic analyzer to capture selected signals during a run. Where it broke. The number of observable signals is small and fixed at compile time, so tracing an unexpected bug usually needs signals you did not capture, forcing a recompile or a fallback to software simulation to find the root cause.
Reproduce hardware failures in software. When the FPGA flags a failure, rerun the failing case in the software simulator to debug it with full visibility. Where it broke. It throws away the FPGA’s speed for the hardest part — diagnosis — and reproducing a deep or long-running failure in a slow simulator can itself take an impractically long time.
The gap. No framework let assertions run at FPGA speed and, when one fired, immediately hand a debugger the full internal state with software-simulation fidelity, while letting engineers change which assertions are active without recompiling the design. That combination — hardware speed for checking, simulator visibility for debugging, and agility in between — is what real assertion-based verification of large designs needs.

How Hassert works

Compiling assertions to hardware, then snapshotting into a simulator on a failure

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

The idea

Move the checking to where the speed is by compiling assertions into hardware. The reason assertions slow down verification is that they run in the software simulator, which was already the slow part; and the reason they cannot simply move to the fast FPGA is that assertions are checking constructs, not circuits — they are unsynthesizable. Hassert’s foundational move is a compiler that closes that gap: it parses each SystemVerilog Assertion, breaks it into atomic operations, and replaces those with equivalent hardware from a synthesizable operator library, then stitches the assertion circuits onto the design at the netlist level. Now the checks run on the FPGA at hardware speed, alongside the design, instead of dragging down a simulator. Pushing the slow, high-visibility verification work out of software and into fast, purpose-built hardware execution is the same acceleration the hardware-accelerated RTL-simulation work covered elsewhere on this site is built on, taking the punishing simulation loop off the general-purpose path and running it where it can go orders of magnitude faster.

Make assertions do double duty as coverage-driven probes you can reconfigure on the fly. An assertion is naturally a probe on the region of interest, watching microarchitectural state, so Hassert treats it as one: it tracks assertion coverage — a hit counter and a monitor of whether each sub-expression of an assertion has been triggered — turning the checks into a live map of what the tests have actually exercised. And because you cannot fit every assertion on the FPGA at once, and you want to change which you watch without paying a full recompile each time, Hassert splits the FPGA into a static region for the design and dynamic regions for assertions and uses partial reconfiguration to swap assertions in and out at runtime, scheduled by their coverage and area cost. Treating verification checks as reconfigurable, coverage-aware observation points rather than fixed instrumentation is the same philosophy the simulator-independent RTL-coverage work covered elsewhere on this site follows, making what the tests have covered a first-class, movable signal that drives where attention goes next.

Buy full visibility only at the moment of failure, with a guided snapshot into a simulator. The FPGA’s blindness is the price of its speed, and the naive fixes are bad: capture everything all the time and you drown the fast hardware, or snapshot on a periodic timer and you pay a constant performance tax while still landing far from the bug. Hassert instead uses the assertion coverage to decide when the internal state actually matters, and only then reads back the entire FPGA state as a snapshot, which it hands to a software simulator that replays from that point with full, signal-level fidelity. So the expensive, high-visibility debugging happens exactly once, at the firing, and lands close to the root cause rather than on an arbitrary clock tick. Recovering deep, fine-grained debuggability for reconfigurable hardware — capturing and reconstructing its state so a failure can be inspected as if in simulation — is the same problem the reconfigurable-hardware debugging work covered elsewhere on this site tackles, restoring the visibility that running on real fabric otherwise takes away.

Following a bug through Hassert

Catching and diagnosing a processor bug at FPGA speed

A trace, based on the paper's abstract and the authors' companion description of Hassert, of how a bug is caught fast and then debugged with full visibility. Some specifics come from the authors' companion material rather than the ASPLOS paper body, which was not available for this draft.

Step 1 of 5

Compile the design and its assertions for the FPGA

A RISC-V core is annotated with SystemVerilog Assertions about its microarchitecture. The Hassert compiler parses them, maps each to equivalent synthesizable hardware from its operator library, and connects the assertion circuits to the core at the netlist level, producing a bitstream with the design and checkers together.

The static region holds the core; dynamic regions hold assertions that can later be swapped by partial reconfiguration.

Why it works

Compiling assertions to hardware removes the software-simulation tax. Assertions are slow because the software simulator evaluates them each cycle, and unsynthesizable so they cannot move to the FPGA → but a compiler that maps each assertion to equivalent circuitry lets the checks run on the FPGA beside the design → so verification runs at hardware speed instead of dragging down a simulator.
Partial reconfiguration makes assertion changes cheap. Testing a different assertion normally means recompiling the whole FPGA bitstream, which is slow → but keeping the design in a static region and assertions in dynamic regions lets Hassert swap assertions at runtime → so many assertions can be exercised without repeated full builds.
Coverage turns assertions into a guide, not just alarms. Firing tells you a property was violated but not what the tests have actually exercised → but tracking a hit counter and sub-expression toggles makes coverage explicit → so Hassert can schedule which assertions to load and decide when the internal state is worth capturing.
Guided snapshots put full visibility exactly where it is needed. Capturing everything drowns the fast hardware and periodic snapshots tax performance while landing far from the bug → but reading back the whole state only when an assertion fires lands a high-fidelity snapshot near the root cause → so debugging is both cheap in the common case and precise at the failure.
Replaying a snapshot recovers simulation-grade debugging. An FPGA failure shows almost none of the internal state that caused it → but transferring the snapshot to a simulator reconstructs the design from that point with full signal visibility → so engineers get the speed of hardware and the debuggability of software together.

What it costs (trade-offs and scope)

This is a draft, and the ASPLOS paper body was not available. The full ASPLOS text was behind a publisher access wall for this draft (the publisher PDF was not retrievable, and there is no arXiv version). This explainer is written from the ASPLOS abstract together with the authors’ own companion extended abstract and poster describing the same Hassert system at another venue; the specific numbers quoted come from that companion material, and the ASPLOS paper’s own detailed results, figures, and full mechanism should be confirmed from the paper itself.
It adds hardware and a toolchain to the flow. Hassert requires compiling assertions into circuits, reserving dynamic FPGA regions for them, and running readback and a simulator for replay; the area overhead is reported as small (a fraction of a percent of look-up tables and registers and a little over one percent of block RAM in the companion evaluation, with no impact on design timing), but it is real, and the framework is more machinery than a plain simulator or a bare FPGA prototype.
Assertion coverage of the operator library bounds what can run on hardware. Compiling an assertion to hardware depends on the operator library covering the SystemVerilog Assertion constructs it uses; assertions using constructs outside the library, or ones whose hardware form is very costly, may not map cleanly, so the breadth of the operator library is a limit on what verifies at hardware speed.
Snapshot and replay depend on FPGA readback and a matching simulator. The debugging path relies on the FPGA’s ability to read back its full state and on a simulator that can reconstruct operation from that state; the fidelity and practicality of replay are tied to those capabilities, and transferring and replaying a large snapshot still costs time, even if far less than reproducing the failure from scratch.
Evaluation is on RISC-V cores and accelerators on one FPGA platform. The reported gains come from a RISC-V processor core and accelerator designs on a specific UltraScale-class FPGA board; this is a strong, realistic demonstration, but the magnitude of speedup and overhead will vary with the design, the assertions, the FPGA, and the simulator used for replay.

The evaluation

Three ways to verify a large hardware design

Property	Software RTL simulation	Plain FPGA prototyping	Hassert
Speed on large designs
Assertions
Visibility when a bug fires
Changing what is observed
Reported outcome		Fast but hard to debug

A comparison based on the paper's abstract and the authors' companion description of Hassert. The companion material reports speedups over software simulation ranging into the tens of thousands of times on RISC-V cores and accelerators, with only a fraction-of-a-percent area overhead and no design timing impact; the ASPLOS paper's own figures were not available for this draft and should be confirmed from the paper.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This is an honest draft. The full ASPLOS paper was not accessible, so the explainer is built from the ASPLOS abstract and the authors’ own companion extended abstract and poster describing the same Hassert system at another venue; the specific quantitative results cited (large speedups over software simulation and a small area overhead) come from that companion material, not the ASPLOS paper body, and should be confirmed from the paper. What is solid and consistent across the sources is the design: Hassert compiles unsynthesizable SystemVerilog Assertions into synthesizable hardware so they run on the FPGA beside the design, adds a system-level reference model for coarse-grained checking, uses partial reconfiguration to swap assertions at runtime without recompiling the design, tracks assertion coverage, and, on a firing, takes a microarchitecture-guided snapshot of the whole FPGA state and replays it in a software simulator for full-visibility debugging. The trade-offs are the added toolchain and hardware machinery, a dependence on the assertion operator library’s breadth and on FPGA readback, and results that will vary by design, FPGA, and simulator. Within those bounds, Hassert is a clean answer to a real dilemma: the speed of hardware and the debuggability of simulation in one flow.

Background

Why verification, not design, is the hard part

It helps to see why so much effort targets checking a chip rather than designing it. Building the logic of a processor is difficult, but making sure it is correct before committing it to silicon is harder and more expensive, because a bug discovered after fabrication can mean a costly respin or a recalled product, so teams verify exhaustively, and that verification is widely cited as the largest single share of chip-development effort. The trouble is that the most trustworthy way to verify — cycle-accurate software simulation with full visibility — is also the slowest, and modern designs are enormous, so simulation throughput becomes the wall the whole schedule hits. This is especially acute for open, configurable instruction sets like RISC-V, whose many variants and extensions each need verifying. Hardware prototyping promises to smash that wall with real-circuit speed, which is why FPGA-based platforms are so attractive for exercising a design at scale. That world, where getting a design onto reconfigurable fabric to test it fast is a central tool of modern hardware development, is the same one the multi-FPGA prototyping-platform work covered elsewhere on this site inhabits, standing up large designs on FPGAs to run them far faster than simulation allows. Hassert’s contribution is to make that fast path debuggable, so the speed of prototyping does not come at the price of flying blind.

If you remember only three things

1. Functional verification is the bottleneck of chip development because register-transfer-level software simulation is very slow for large designs, and assertion-based verification — embedding formal checks that fire on unexpected behavior — improves observability but makes software simulation slower still; running the design on an FPGA is orders of magnitude faster, but assertions are not synthesizable and FPGA prototypes give almost no fine-grained visibility when a bug occurs, forcing a fallback to slow simulation to find the cause.
2. Hassert combines FPGA speed with simulator visibility: a compiler translates unsynthesizable SystemVerilog Assertions into equivalent synthesizable hardware (via a parser, a transformer that maps assertion pieces to a hardware operator library, and a connector that stitches them to the design) so checks run on the FPGA beside the design, with a CPU reference model for coarse-grained checking; partial reconfiguration swaps assertions in and out at runtime without recompiling the design; and assertions double as coverage probes.
3. When an assertion fires, a microarchitecture-guided snapshot reads back the entire FPGA state at the failing moment (avoiding the cost of periodic snapshots) and transfers it to a software simulator that replays from that point with full signal-level fidelity, giving hardware-speed testing plus simulation-grade debugging. This explainer is a draft from the ASPLOS abstract and the authors' companion material; the companion reports large speedups over software simulation at small area overhead, but the ASPLOS paper's own figures should be confirmed from the paper.

Check yourself

Check your understanding

1. Why is verifying a large hardware design with assertions so slow, and why can't you just move to an FPGA?
2. How does Hassert get assertions to run at FPGA speed?
3. What is the microarchitecture-guided snapshot, and why is it better than the alternatives?
4. What should a reader keep in mind about this explainer and Hassert's results?

Sources

The paper is “Hassert: Hardware Assertion-Based Verification Framework with FPGA Acceleration” by Ziqing Zhang, Weijie Weng, Yaning Li, Lijia Cai, Haoyu Wang, David Boland, Yungang Bao, and Kan Shi (SKLP, Institute of Computing Technology, Chinese Academy of Sciences, and the University of Chinese Academy of Sciences, with the University of Sydney), published at ASPLOS 2024 (Volume 4), DOI 10.1145/3622781.3698899.

This explainer is a draft. The full ASPLOS paper text was not accessible at the time of writing (the ACM Digital Library PDF returned a bot-verification challenge, and there is no arXiv version), so it is written from the ASPLOS abstract together with the authors’ own companion material on the same Hassert system: their extended abstract and poster “Hassert: Hardware Assertion-Based Agile Verification Framework with FPGA Acceleration” from RISC-V Summit Europe 2025. The ASPLOS abstract supplies the problem framing (verification as the chip-development bottleneck due to slow software simulation, assertion-based verification improving observability but being confined to slow simulation, and FPGA prototyping being fast but lacking fine-grained debugging) and the core contributions (automating the scheduling and mapping of SystemVerilog Assertions onto the FPGA fabric with the design-under-test, dynamic switching of assertions via runtime partial reconfiguration without recompiling the design, and a microarchitecture-guided hardware snapshot scheme that captures the FPGA state on an assertion firing and transfers it to an external simulator for reconstruction and debugging, at small area overhead). The companion extended abstract and poster provide the mechanism details reflected here — the Hassert compiler’s parser, transformer, and connector and its synthesizable SVA operator library; the multi-level self-checking combining a system-level reference model with microarchitecture-level assertions; assertion coverage as a hit counter and sub-expression toggle monitor; the static-region versus dynamic-region partial-reconfiguration scheme; and the periodic-versus-microarchitecture-guided snapshot comparison — as well as the quantitative results cited (speedups over software simulation on RISC-V cores and accelerators ranging into the tens of thousands of times, with a fraction-of-a-percent area overhead in look-up tables and registers and a little over one percent in block RAM, and no impact on design timing). Those numbers come from the companion material, not the ASPLOS paper body; the ASPLOS paper’s own detailed results, figures, and full mechanism are not reproduced here and should be read from the paper itself.