Formally verifying a tiny cache with JasperGold

Lucca Rodrigues • August 8, 2026

asic hardware formal verification comp arch

This write-up is adapted from my End-of-Semester project for Carnegie Mellon’s 18-341: “Logic Design & Verification”. My goal was to explore industry-standard Formal Verification flows for ASICs: take a small design (a cache controller), exhaustively test it, constrain the formal environment, poke holes until I break it, and generate some formal proofs.

Special thanks to Prof. Bill Nace for vetting this article before it goes online.

Enjoy!

Iain Singleton’s guest lecture on FV was honestly one of the coolest guest lectures I’ve attended at CMU. The JasperGold demo on the FIFO was especially clever and well put together, and it really demystified what “formal verification” actually means in practice. It made me want to try doing the same thing on a small design of my own.

Since I’m really excited to take 18-447 (Intro to Computer Architecture) next semester, I decided to lean into that theme and build a tiny cache controller in RTL, then formally prove a few properties about how it behaves using SystemVerilog Assertions and JasperGold.

Given the time limit of ~4 hours for this mini-project, the goal was not to fully verify a production-ready cache, but to:

There’s still a lot more I’d like to explore (more interesting properties, deeper environment modeling, liveness, etc.), and I’m hoping to mess around with Jasper more over Winter break.

Caches, 213-style

This section is heavily inspired by the 18-213 (Introduction to Computer Systems) material, which I took about a year ago. I had to brush off some rust and re-learn the basics before I could sensibly design and reason about even a tiny cache.

Motivation

Consider a very simple computer system: a CPU core (ALU, register file, control, datapath, RISC-240 style) connected to main memory (RAM) over a memory bus. The CPU issues read/write requests over this bus:

A memory controller sits between the core and RAM. It:

The problem at hand is a classic one: fast memory is small and expensive; large memory is slow and cheap.

If every load and store has to hit main memory, the CPU spends a lot of time waiting around for data. That’s where caches come in: small, fast SRAM that sits between the CPU and main memory. The cache stores a subset of memory contents (hopefully “hot” ones) and services most accesses locally. This works well in practice because programs tend to exhibit:

The whole point of the cache is to exploit that locality and avoid going to slow memory on every single access.

How a cache works

Very roughly, a (set-associative) cache is organized using a few key concepts:

All of these knobs (associativity, line size, write policy) affect both performance and verification complexity. For a tiny 4-hour FV demo, I simplified aggressively.

Our cache

Here’s the exact configuration I used for this project:

From that:

So the address is split as: [ tag(3 bits) | index(2 bits) ]

In the RTL, each cache line is just a small struct:

typedef struct {
  logic       valid;
  logic [2:0] tag;
  logic [7:0] data;
} CacheLine_t;

CacheLine_t CACHE_LINES[4];  // one line per set

So the cache physically stores:

Cache RTL model

The cache controller is implemented as a small finite-state machine (FSM) that controls how CPU requests interact with the cache lines and the backing memory.

FSM

Testbench

I also wrote a simple testbench with directed tests to sanity check my implementation.

JasperGold

In the context of this project, I used JasperGold mainly to:

For this 4-hour mini-project, I focused on a handful of small, local properties to get hands-on experience with the FV flow.

Running JG

On the ECE machines, JasperGold is set up through the 18-224 class environment. To run it:

source /afs/ece.cmu.edu/class/ece224/setup_jasper

jg  <script.tcl>

TCL

Here is the simple Tcl script I used to analyze and prove properties on the cache:

clear -all

analyze -sv cache.sv

elaborate -disable_auto_bbox \
    -top cache

clock clock
reset reset -expression {reset}

set_engine_mode {B M G Hps Hts Tri}

prove -all

Assertions I’ve proved

  1. If we are in HIT_READ, then the response must be valid and equal to the cached data
  2. In MISS_READ_REQ we must send a read request to memory
  3. On a read-miss response, the cache line must be filled correctly

Debugging

The first couple of properties were very straightforward. After wiring them up and running JasperGold, both passed immediately:

The waveform and property summary confirmed that the RTL and the properties agreed.

When I added the third property:

property read_miss_fills_cache;
  @(posedge clock) disable iff (reset)
    (state == MISS_READ_WAIT && mem_resp_valid)
      |=> (CACHE_LINES[latched_req_addr[1:0]].valid &&
           CACHE_LINES[latched_req_addr[1:0]].tag   == latched_req_addr[4:2] &&
           CACHE_LINES[latched_req_addr[1:0]].data  == mem_resp_rdata);
endproperty

assert property (read_miss_fills_cache);

JasperGold reported a FAIL and generated a counterexample. Time to debug.

Let’s inspect the counter example:

Hmm, this is hard to read. let’s group the signals together in categories that make more sense:

At first, the waveform was a bit noisy, so I grouped signals by category (state, CPU interface, memory interface, cache line state) to make it easier to read. What I saw:

This turned out to be the key hint: Jasper had no idea how my memory controller behaves.

From Jasper’s perspective:

So it happily produced a counterexample where the memory’s response pattern violated what I was implicitly assuming in my property.

To fix this, I added assumptions that describe how the memory is allowed to behave. These are SVA properties written with assume property instead of assert property, and they constrain the environment:

  1. Memory responds exactly one cycle after a read request
  2. Memory only responds if there was a read request in the previous cycle

With these in place, JasperGold was no longer allowed to invent arbitrary mem_resp_valid behavior. The new traces showed mem_resp_valid cleanly following the requests, as intended.

However, the third property still failed. So the problem wasn’t just the environment.

However, the third property still failed. So the problem wasn’t just the environment.

Looking more closely at the waveform and the failing trace, I realized the issue was with when I was checking the cache contents.

In the RTL:

But in my property, I was checking:

(state == MISS_READ_WAIT && mem_resp_valid)
  |=> (CACHE_LINES[...] == mem_resp_rdata);

On the next cycle, the cache line reflects the data written on the previous edge. However, mem_resp_rdata in that next cycle is no longer guaranteed to hold the same value it had when the write occurred. It might change or be X/unconstrained.

What I actually want is:

On the cycle after the response, the cache line’s data equals the value of mem_resp_rdata from the cycle when the response happened.

That’s exactly what sampled value functions like $past are for. The corrected property:

property read_miss_fills_cache;
  @(posedge clock) disable iff (reset)
    (state == MISS_READ_WAIT && mem_resp_valid)
      |=> (CACHE_LINES[latched_req_addr[1:0]].valid &&
           CACHE_LINES[latched_req_addr[1:0]].tag   == latched_req_addr[4:2] &&
           CACHE_LINES[latched_req_addr[1:0]].data  == $past(mem_resp_rdata));
endproperty

assert property (read_miss_fills_cache);

After this fix, JasperGold proved the property, and the waveform lined up with my mental model of the cache’s behavior.

Et voilá!

What’s next?

Missing properties

There are several natural properties I didn’t have time to formalize in this 4-hour window, for example:

These would further increase confidence that the cache controller is behaving according to the intended policy.

Bounded proofs

All the properties I wrote are small, local safety properties that Jasper can prove exhaustively for this tiny design. For more complex designs, it’s common to:

If I extend this project over Winter break, a natural next step would be to write a few deeper, more “end-to-end” properties (like “every accepted request eventually produces a response”) and explore how far Jasper can push those with bounded or inductive proofs.

References