The FIFO testbench
You will learn
What a testbench discipline looks like when it is real, and why this lesson opens the FIFO spec and a mutation recording instead.
A testbench for the asynchronous FIFO would drive both clocks, tear the pointers on purpose and check that the flags never lie. The testbench spec in this tree is not that yet: it does not compile in the browser compiler and native runs are blocked on it, so this lesson opens fifo.t27 itself and, in place of a FIFO testbench, a recording of the discipline it would follow: 5 planted bugs in packets.t27 -- a CRC polynomial bit, a CRC address width, LFRM no-ops, a COR0 bit, a type-2 word count -- each mutant rebuilt and re-swept, every one caught. When a real testbench spec lands, this lesson takes it.
Try it
In the recording, list the 5 planted bugs and count how many were caught; then in the spec frame find the flags a real testbench would have to tear on purpose.
67 specs lose 23,578 tokens to parser recovery, each held at its pinned bound.
specs/fpga/fifo.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/fifo.t27
// Synchronous and Asynchronous FIFO Stdlib for Trinity T27 FPGA HIR
// Defines FIFO configuration with depth, data width, and flags
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY
module Fifo {
// === FIFO kind ===
pub const FifoKind = enum(i8) {
sync_fifo = 0,
async_fifo = 1,
}
// === FIFO status flags ===
pub struct FifoFlags {
empty : bool,
full : bool,
almost_empty : bool,
almost_full : bool,
}
// === FIFO configuration ===
pub struct FifoConfig {
name : &str,
kind : i8,
depth : u32,
data_width : u32,
has_almost_empty : bool,
has_almost_full : bool,
almost_empty_threshold : u32,
almost_full_threshold : u32,
use_bram : bool,
}
// === FIFO runtime state (for simulation) ===
pub const MAX_FIFO_DEPTH : u32 = 65536;
pub struct FifoState {
fill_count : u32,
head_ptr : u32,
tail_ptr : u32,
flags : FifoFlags,
}
// === Constructor helpers ===
fn sync_fifo(name: &str, depth: u32, data_width: u32) -> FifoConfig {
return FifoConfig{
.name = name,
.kind = 0,
.depth = depth,
.data_width = data_width,
.has_almost_empty = false,
.has_almost_full = false,
.almost_empty_threshold = 0,
.almost_full_threshold = 0,
.use_bram = true,
};
}
fn async_fifo(name: &str, depth: u32, data_width: u32) -> FifoConfig {
return FifoConfig{
.name = name,
.kind = 1,
.depth = depth,
.data_width = data_width,
.has_almost_empty = false,
.has_almost_full = false,
.almost_empty_threshold = 0,
.almost_full_threshold = 0,
.use_bram = true,
};
}
fn with_almost_empty(cfg: FifoConfig, threshold: u32) -> FifoConfig {
var result = cfg;
result.has_almost_empty = true;
result.almost_empty_threshold = threshold;
return result;
}
fn with_almost_full(cfg: FifoConfig, threshold: u32) -> FifoConfig {
var result = cfg;
result.has_almost_full = true;
result.almost_full_threshold = threshold;
return result;
}
fn empty_fifo_state() -> FifoState {
return FifoState{
.fill_count = 0,
.head_ptr = 0,
.tail_ptr = 0,
.flags = FifoFlags{
.empty = true,
.full = false,
.almost_empty = false,
.almost_full = false,
},
};
}
// === Query functions ===
fn is_sync(cfg: FifoConfig) -> bool {
return cfg.kind == 0;
}
fn is_async(cfg: FifoConfig) -> bool {
return cfg.kind == 1;
}
fn addr_width(cfg: FifoConfig) -> u32 {
var d : u32 = cfg.depth;
var w : u32 = 0;
while (d > 1) {
w = w + 1;
d = d / 2;
}
if (w == 0) {
w = 1;
}
return w;
}
fn total_storage_bits(cfg: FifoConfig) -> u32 {
return cfg.depth * cfg.data_width;
}
fn bram18_count(cfg: FifoConfig) -> u32 {
var bits : u32 = cfg.depth * cfg.data_width;
var count : u32 = bits / 18432;
if (bits % 18432 > 0) {
count = count + 1;
}
return count;
}
fn is_empty(state: FifoState) -> bool {
return state.flags.empty;
}
fn is_full(state: FifoState) -> bool {
return state.flags.full;
}
fn fill_count(state: FifoState) -> u32 {
return state.fill_count;
}
fn has_space(state: FifoState) -> bool {
return state.flags.full == false;
}
fn has_data(state: FifoState) -> bool {
return state.flags.empty == false;
}
// === Push/Pop state updates ===
fn push(state: FifoState, cfg: FifoConfig) -> FifoState {
var result = state;
if (state.flags.full) {
return result;
}
result.tail_ptr = (state.tail_ptr + 1) % cfg.depth;
result.fill_count = state.fill_count + 1;
result.flags.empty = false;
if (result.fill_count == cfg.depth) {
result.flags.full = true;
}
return result;
}
fn pop(state: FifoState, cfg: FifoConfig) -> FifoState {
var result = state;
if (state.flags.empty) {
return result;
}
result.head_ptr = (state.head_ptr + 1) % cfg.depth;
result.fill_count = state.fill_count - 1;
result.flags.full = false;
if (result.fill_count == 0) {
result.flags.empty = true;
}
return result;
}
// === Validation ===
fn validate_fifo(cfg: FifoConfig) -> u32 {
var errors : u32 = 0;
if (cfg.name == "") {
errors = errors + 1;
}
if (cfg.depth == 0) {
errors = errors + 1;
}
if (cfg.data_width == 0) {
errors = errors + 1;
}
if (cfg.has_almost_empty and cfg.almost_empty_threshold >= cfg.depth) {
errors = errors + 1;
}
if (cfg.has_almost_full and cfg.almost_full_threshold >= cfg.depth) {
errors = errors + 1;
}
return errors;
}
// === Tests ===
test sync_fifo_is_sync
given f = sync_fifo("tx_fifo", 16, 8)
then is_sync(f) == true
and is_async(f) == false
test async_fifo_is_async
given f = async_fifo("cross_fifo", 32, 16)
then is_async(f) == true
and is_sync(f) == false
test addr_width_16
given f = sync_fifo("f", 16, 8)
then addr_width(f) == 4
test addr_width_256
given f = sync_fifo("f", 256, 32)
then addr_width(f) == 8
test total_storage_bits
given f = sync_fifo("f", 16, 32)
then total_storage_bits(f) == 512
test bram18_small
given f = sync_fifo("f", 16, 32)
then bram18_count(f) == 1
test empty_state_is_empty
given s = empty_fifo_state()
then is_empty(s) == true
and is_full(s) == false
and fill_count(s) == 0
and has_data(s) == false
and has_space(s) == true
test push_increments_fill
given cfg = sync_fifo("f", 4, 8)
and s = empty_fifo_state()
and s2 = push(s, cfg)
then fill_count(s2) == 1
and is_empty(s2) == false
test push_to_full
given cfg = sync_fifo("f", 2, 8)
and s = empty_fifo_state()
and s2 = push(s, cfg)
and s3 = push(s2, cfg)
then is_full(s3) == true
and fill_count(s3) == 2
test push_on_full_noop
given cfg = sync_fifo("f", 2, 8)
and s = empty_fifo_state()
and s2 = push(s, cfg)
and s3 = push(s2, cfg)
and s4 = push(s3, cfg)
then fill_count(s4) == 2
test pop_decrements_fill
given cfg = sync_fifo("f", 4, 8)
and s = empty_fifo_state()
and s2 = push(s, cfg)
and s3 = pop(s2, cfg)
then fill_count(s3) == 0
and is_empty(s3) == true
test pop_on_empty_noop
given cfg = sync_fifo("f", 4, 8)
and s = empty_fifo_state()
and s2 = pop(s, cfg)
then fill_count(s2) == 0
test push_pop_roundtrip
given cfg = sync_fifo("f", 4, 8)
and s = empty_fifo_state()
and s2 = push(s, cfg)
and s3 = push(s2, cfg)
and s4 = pop(s3, cfg)
then fill_count(s4) == 1
and has_data(s4) == true
and has_space(s4) == true
test with_almost_empty
given f = sync_fifo("f", 16, 8)
and f2 = with_almost_empty(f, 2)
then f2.has_almost_empty == true
and f2.almost_empty_threshold == 2
test with_almost_full
given f = sync_fifo("f", 16, 8)
and f2 = with_almost_full(f, 14)
then f2.has_almost_full == true
and f2.almost_full_threshold == 14
test validate_ok
given f = sync_fifo("f", 16, 8)
then validate_fifo(f) == 0
test validate_empty_name
given f = sync_fifo("", 16, 8)
then validate_fifo(f) > 0
test validate_zero_depth
given f = FifoConfig{.name = "x", .kind = 0, .depth = 0, .data_width = 8, .has_almost_empty = false, .has_almost_full = false, .almost_empty_threshold = 0, .almost_full_threshold = 0, .use_bram = true}
then validate_fifo(f) > 0
// === Invariants ===
invariant fill_count_non_negative
given s = empty_fifo_state()
assert fill_count(s) >= 0
invariant fill_count_le_depth
given cfg = sync_fifo("inv", 16, 8)
and s = push(empty_fifo_state(), cfg)
assert fill_count(s) <= cfg.depth
invariant empty_xor_full
given s = empty_fifo_state()
assert (is_empty(s) and is_full(s)) == false
invariant has_space_iff_not_full
given s = empty_fifo_state()
assert has_space(s) == (is_full(s) == false)
invariant has_data_iff_not_empty
given s = empty_fifo_state()
assert has_data(s) == (is_empty(s) == false)
invariant bram18_positive
given f = sync_fifo("inv", 16, 8)
assert bram18_count(f) > 0
// === Benchmarks ===
bench push_latency
measure: nanoseconds to push(empty_fifo_state(), sync_fifo("b", 16, 8))
target: < 100ns
bench pop_latency
measure: nanoseconds to pop(push(empty_fifo_state(), sync_fifo("b", 16, 8)), sync_fifo("b", 16, 8))
target: < 100ns
}
// phi^2 + 1/phi^2 = 3 | TRINITY
All lessons
Module 1 · What a clock is
One edge, one world: what shares a clock edge shares a world, the period and the jitter of a real edge, and where the clock enters a board.
Module 2 · Clock trees
Skew and insertion delay, the global buffer network, and the trap of gating a clock with logic.
Module 3 · PLL and MMCM
Multiply and divide one clock into another, move its phase in steps of the VCO, and which clocks the analyzer treats as related.
Module 4 · Resets
Assert asynchronously, release synchronously: the three reset kinds, the release pipe, and the tree a reset grows.
Module 5 · Metastability
The setup-hold window, the mean time between failures in integer arithmetic, and the two flops that fix it.
Module 6 · Crossing many bits
Why a binary bus tears, why Gray code does not, and the handshake that moves a pulse between worlds.
Module 7 · The asynchronous FIFO
Pointers, flags and depth: the buffer that moves a stream between two clocks.
Module 8 · Constraints
The lines that tell the analyzer what a clock is, which paths not to check, and what the pins must meet.
Module 9 · On the board
A CDC report, one crossing captured at the flip-flops, and the bitstream diff that closes the course.