Why binary fails
You will learn
Why sampling a binary bus mid-change tears it, and what the FIFO spec checks of its pointers.
Cross a multi-bit bus by sampling it in another domain and it tears: some bits arrive from before the change, some from after, and the value you read never existed. A binary counter is the worst carrier -- 7 to 8 flips four bits at once. fifo.t27 is the buffer that does this properly, and its head advances as (head_ptr + 1) % depth, with MAX_FIFO_DEPTH 65536. The recording runs the native t27c on it: 18 tests pass, 6 invariants comptime. What the tests check is fill counts and flags; the next lesson shows what they never check.
Try it
In the recording, count the passing tests and the proved invariants; then in the spec frame find the head pointer update and the maximum depth constant.
t27c 0.4.0 on a laptop (macOS): 18 tests of the FIFO spec pass natively, 6 invariants comptime -- push and pop state, flags, BRAM count.
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.