Pointers and flags
You will learn
How the flags are derived from the pointers, which signals actually cross, and what one flipped assignment breaks.
The data does not cross; it lives in BRAM and both sides address it. What crosses is the pointers, in Gray, and the flags derived from them: empty when the pointers match, full when they differ by the depth. The recording breaks the flag arithmetic with one flipped assignment -- push sets flags.empty to true -- and exactly one test fails, push_increments_fill, the one that asks a push for a non-empty FIFO. The recording restores the spec and prints its sha256. The spec frame opens fifo.t27, where push and pop build the flags the crossing carries.
Try it
In the recording, find the flipped assignment and the one test that fails; then in the spec frame find where push builds the flags and derive empty from the pointers yourself.
push sets flags.empty = false; one sed flips it to true and push_increments_fill fails on the next run; git restores the spec.
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.