When we launched SystemVerilog support for Aristotle, our compiler supported designs with a single ungated clock. Today we drop this restriction. Aristotle now supports multiple clock domains, latches and clock gating.
Large designs run on different clocks and exchange data asynchronously. Clock gates, often built with latches, save power. Aristotle can now verify these designs with their clocking logic faithfully modeled.
An asynchronous FIFO shows all three features. We start with a working design, change its clocks and then introduce two bugs.
A working FIFO
An asynchronous FIFO connects a writer and reader on separate clocks. Synchronized pointers tell each side whether there is room to write or data to read.
Our starting FIFO holds four 8-bit words and uses Gray-coded pointers. Aristotle proves that it never overflows or underflows, returns the correct data and eventually makes queued data visible to the reader. All properties are proved in ~20 minutes.
View the full FIFO code
// Complete presentation example: FIFO, separate synchronizer, SVA checker
// and a wrapper that connects the checker.
// Two-stage destination-clock synchronizer. Digital capture model.
module cdc_sync #(
parameter int WIDTH = 3,
parameter logic [WIDTH-1:0] RESET_VALUE = '0
) (
input logic clk,
input logic rst_n,
input logic [WIDTH-1:0] din,
output logic [WIDTH-1:0] dout
);
(* ASYNC_REG = "TRUE" *) logic [WIDTH-1:0] stage1, stage2;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) begin
stage1 <= RESET_VALUE;
stage2 <= RESET_VALUE;
end else begin
stage1 <= din;
stage2 <= stage1;
end
assign dout = stage2;
endmodule
// Dual-clock FIFO with registered Gray pointers. A >= 2.
// Baseline: W=8, A=2. Large configuration: W=32, A=12 (4096 words).
// Handshakes occur on their local rising clock edges.
module async_fifo_gray #(
// data width
parameter int W = 8,
// address width: the FIFO holds 2**A words
parameter int A = 2
) (
input logic wclk,
input logic wrst_n,
input logic wvalid,
output logic wready,
input logic [W-1:0] wdata,
input logic rclk,
input logic rrst_n,
output logic rvalid,
input logic rready,
output logic [W-1:0] rdata,
output logic [A:0] rcount
);
logic [W-1:0] mem [2**A];
// The pointers have one extra bit, so that a full FIFO and an empty FIFO
// differ.
// write pointer (wclk)
logic [A:0] wbin, wgray;
// read pointer (rclk)
logic [A:0] rbin, rgray;
// read pointer, synchronized to wclk
logic [A:0] wq2_rgray;
// write pointer, synchronized to rclk
logic [A:0] rq2_wgray;
logic wfull, rempty;
// Write side
wire wpush = wvalid && wready;
wire [A:0] wbin_next = wbin + wpush;
wire [A:0] wgray_next = (wbin_next >> 1) ^ wbin_next;
// Full when the next write pointer is one lap ahead of the read pointer. In
// Gray code, the two top bits then differ and the other bits are equal.
wire wfull_next = wgray_next == {~wq2_rgray[A:A-1], wq2_rgray[A-2:0]};
always_ff @(posedge wclk or negedge wrst_n)
if (!wrst_n) begin
wbin <= '0;
wgray <= '0;
wfull <= 1'b0;
end else begin
wbin <= wbin_next;
wgray <= wgray_next;
wfull <= wfull_next;
end
always_ff @(posedge wclk)
if (wpush) mem[wbin[A-1:0]] <= wdata;
assign wready = !wfull;
// Read side
wire rpop = rvalid && rready;
wire [A:0] rbin_next = rbin + rpop;
wire [A:0] rgray_next = (rbin_next >> 1) ^ rbin_next;
wire rempty_next = rgray_next == rq2_wgray;
always_ff @(posedge rclk or negedge rrst_n)
if (!rrst_n) begin
rbin <= '0;
rgray <= '0;
rempty <= 1'b1;
end else begin
rbin <= rbin_next;
rgray <= rgray_next;
rempty <= rempty_next;
end
assign rvalid = !rempty;
assign rdata = mem[rbin[A-1:0]];
// Read data count: the synchronized write pointer minus the read pointer, in
// binary.
// Bit i of the binary value is the XOR of Gray bits i to A.
logic [A:0] rq2_wbin;
always_comb
for (int i = 0; i <= A; i++) rq2_wbin[i] = ^(rq2_wgray >> i);
assign rcount = rq2_wbin - rbin;
// Each crossing has its own two-stage synchronizer module.
cdc_sync #(.WIDTH(A+1)) sync_r2w (
.clk(wclk), .rst_n(wrst_n), .din(rgray), .dout(wq2_rgray)
);
cdc_sync #(.WIDTH(A+1)) sync_w2r (
.clk(rclk), .rst_n(rrst_n), .din(wgray), .dout(rq2_wgray)
);
endmodule
// Interface contract for a FIFO with DEPTH = 2**A.
// Harness: coordinated reset, no transfers during reset and then no more resets.
// Root clocks may have unrelated periods and phase; each continues to rise.
// Accepted-transfer counters are verification state, not hardware crossings.
module fifo_contract #(
parameter int W = 8,
parameter int A = 2,
parameter bit CHECK_COUNT = 1'b0
) (
input logic wclk, wrst_n, wvalid, wready,
input logic [W-1:0] wdata,
input logic rclk, rrst_n, rvalid, rready,
input logic [W-1:0] rdata,
input logic [A:0] rcount
);
localparam int DEPTH = 1 << A;
wire wpush = wvalid && wready;
wire rpop = rvalid && rready;
logic [A:0] write_count, read_count;
always_ff @(posedge wclk or negedge wrst_n)
if (!wrst_n) write_count <= '0;
else if (wpush) write_count <= write_count + 1'b1;
always_ff @(posedge rclk or negedge rrst_n)
if (!rrst_n) read_count <= '0;
else if (rpop) read_count <= read_count + 1'b1;
wire [A:0] occupancy = write_count - read_count;
// An arbitrary fixed transfer index: prove the same statement for every word.
logic [A:0] tracked_index;
always_ff @(posedge wclk) tracked_index <= tracked_index;
logic [W-1:0] expected_data;
always_ff @(posedge wclk)
if (wpush && write_count == tracked_index) expected_data <= wdata;
m_hold: assume property (@(posedge wclk)
disable iff (!wrst_n)
wvalid && !wready |=> wvalid && $stable(wdata));
a_no_overflow: assert property (@(posedge wclk)
disable iff (!wrst_n) occupancy <= DEPTH);
a_no_underflow: assert property (@(posedge rclk)
disable iff (!rrst_n) rpop |-> occupancy != 0);
a_data: assert property (@(posedge rclk)
disable iff (!rrst_n)
rpop && read_count == tracked_index |-> rdata == expected_data);
ready_is_safe: assert property (@(posedge wclk)
disable iff (!wrst_n) wready |-> occupancy < DEPTH);
valid_is_safe: assert property (@(posedge rclk)
disable iff (!rrst_n) rvalid |-> occupancy != 0);
// Becoming visible must not depend on the consumer already being ready.
l_visible: assert property (@(posedge rclk)
disable iff (!rrst_n) occupancy != 0 |-> s_eventually rvalid);
if (CHECK_COUNT) begin : count_contract
a_count: assert property (@(posedge rclk)
disable iff (!rrst_n) rcount <= occupancy);
end
endmodule
// Explicit DUT/checker connections for this example.
module fifo_example (
input logic wclk, wrst_n, wvalid,
output logic wready,
input logic [7:0] wdata,
input logic rclk, rrst_n, rready,
output logic rvalid,
output logic [7:0] rdata,
output logic [2:0] rcount
);
async_fifo_gray #(.W(8), .A(2)) dut (
.wclk(wclk), .wrst_n(wrst_n), .wvalid(wvalid), .wready(wready), .wdata(wdata),
.rclk(rclk), .rrst_n(rrst_n), .rvalid(rvalid), .rready(rready),
.rdata(rdata), .rcount(rcount)
);
fifo_contract #(.W(8), .A(2), .CHECK_COUNT(1'b0)) checks (
.wclk(wclk), .wrst_n(wrst_n), .wvalid(wvalid), .wready(wready), .wdata(wdata),
.rclk(rclk), .rrst_n(rrst_n), .rvalid(rvalid), .rready(rready),
.rdata(rdata), .rcount(rcount)
);
endmoduleWe make assumptions about the reset-release sequence and require the producer to hold its request and data stable while stalled. We assume both clocks keep running.
Aristotle’s symbolic clocks let us leave clocks independent, require them to keep running or specify periods and phases. One proof covers every clock schedule allowed by its assumptions.
Here are two checks from the example:
a_no_overflow: assert property (
@(posedge wclk) disable iff (!wrst_n)
occupancy <= DEPTH
);
a_data: assert property (
@(posedge rclk) disable iff (!rrst_n)
rpop && read_count == tracked_index |->
rdata == expected_data
);The checker counts accepted transfers and tracks an arbitrary word. The capacity check runs on the write clock; the data check runs on the read clock.
Change the clocks, depth and width
Let’s now move from four 8-bit words to 4096 32-bit words:
async_fifo_gray #(
- .W(8), .A(2)
+ .W(32), .A(12)
) dut (...);We keep the same properties and give the clocks fixed periods in a 2000:3 write-to-read ratio. Their phases remain independent. Aristotle proves every property for the larger FIFO as well, in about 10 minutes.
The larger memory and extreme clock periods do not cause a blowup in proof complexity here. That is the power of theorem proving: Aristotle builds a deductive proof that has strong scaling properties that are not directly related to the number of state-bits in the design or the sequential depth of the design.
One-hot pointers and metastability
Next, let’s explore a common source of bugs in multiclock designs: sampling a signal as it changes. We replace the FIFO’s Gray-coded pointers with one-hot pointers and ask Aristotle to check the design with an explicit digital metastability model.
A Gray-code pointer changes one bit per increment, while a one-hot pointer changes two.
We model metastability by introducing nondeterminism into the first synchronizer stage. When a pointer changes as it is sampled, each changing bit can independently take its old or new value.
Aristotle refutes the claim that the read count never exceeds occupancy:
a_count: assert property (
@(posedge rclk) disable iff (!rrst_n)
rcount <= occupancy
);In the counterexample, the synchronizer captures two set pointer bits during a transition. The read side interprets that invalid pointer as more queued data than the FIFO holds. With a Gray-code pointer, this capture model gives the receiver either the old pointer or the new one.
A clock gate that never wakes up
Another common optimization that can hide subtle bugs is clock gating. In this case, we try to save power by stopping the read-side clock when the FIFO appears empty. We use a level-sensitive latch to control the gate:
always_latch begin
if (!rclk)
rgate_latched <= !rst_n || awake || !empty;
end
assign rgclk = rclk && rgate_latched;The latch updates the gate’s enable while rclk is low and holds it steady while high.
The mistake is gating the incoming write-pointer synchronizer. A wake detector on the root clock watches a notification bit that toggles on each accepted write.
Aristotle finds a missed wakeup and refutes the property that queued data eventually becomes visible:
l_visible: assert property (
@(posedge rclk) disable iff (!rst_n)
occupancy != 0 |-> s_eventually rvalid
);This property samples on the root read clock. Stopping the gated clock cannot hide the failure.
Keeping the pointer synchronizer on the ungated read clock repairs the missed wakeup:
cdc_sync #(.WIDTH(3)) sync_w2r (
- .clk(rgclk), .rst_n(rst_n),
+ .clk(rclk), .rst_n(rst_n),
.din(wgray), .dout(rq2_wgray)
);The pointer copy can now update while the read side sleeps. In this design, the combinational empty flag then reopens the gate. This restores progress in the failing example.
Try it on your own design
Give Aristotle your SystemVerilog and SVA, or describe the properties in English. State the clock and reset assumptions. For an asynchronous FIFO:
Verify this async FIFO for no overflow, no underflow, correct data and eventual visibility. The two root clocks are independent and keep running. Assume coordinated initial reset, no transfers during reset and no later resets. The producer holds its request and data steady while stalled.
You can inspect the properties, their assumptions and the results in Aristotle. Get started at aristotle.harmonic.fun.
Press inquiries: pr@harmonic.fun
