One edge, one world
You will learn
What a clock domain is, the four ways clock_domain.t27 names to cross one, and what the native compiler checks of them.
A clock domain is every flip-flop that shares one clock edge. Move a signal between two domains and the receiving edge can sample it mid-change: that is the whole subject of this course. clock_domain.t27 names the four ways across in one enum: no_cross, two_flop, fifo_async, handshake. Module 5 takes two_flop apart, module 6 the handshake, module 7 the FIFO. The recording runs the native t27c on this spec: 12 tests pass and 5 invariants are proved while it compiles. The player compiles the spec in your browser; where the browser cannot run a check it skips it and says why.
Try it
In the recording, count the passing tests and the proved invariants; then in the spec frame find the four crossing strategies and name the module of this course that takes each one apart.
t27c 0.4.0 on a laptop (macOS): 12 tests of the clock-domain spec pass natively, 5 invariants proved comptime, and the spec's own header says what it models.
specs/fpga/clock_domain.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/clock_domain.t27
// Clock Domain Abstraction for Trinity T27 FPGA HIR
// Defines clock sources, PLL configs, and cross-domain crossing
// Uses flat structs (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY
module ClockDomain {
// === Clock source kind ===
pub const ClkSrcKind = enum(i8) {
external = 0,
pll = 1,
dcm = 2,
mmcm = 3,
};
// === Clock edge ===
pub const ClkEdge = enum(i8) {
posedge = 0,
negedge = 1,
};
// === Crossing strategy ===
pub const CrossStrategy = enum(i8) {
no_cross = 0,
two_flop = 1,
fifo_async = 2,
handshake = 3,
};
// === Clock source descriptor ===
pub struct ClkSource {
name : &str,
kind : i8,
freq_hz : u32,
phase_deg : u32,
jitter_ps : u32,
}
// === Clock domain descriptor ===
pub struct ClkDomain {
name : &str,
source_name : &str,
freq_hz : u32,
edge : i8,
}
// === Cross-domain crossing descriptor ===
pub struct ClockCrossing {
src_domain : &str,
dst_domain : &str,
strategy : i8,
data_width : u32,
}
// === Constructor helpers ===
fn ext_clock(name: &str, freq_hz: u32) -> ClkSource {
return ClkSource{
.name = name,
.kind = 0,
.freq_hz = freq_hz,
.phase_deg = 0,
.jitter_ps = 0,
};
}
fn pll_clock(name: &str, freq_hz: u32, phase_deg: u32) -> ClkSource {
return ClkSource{
.name = name,
.kind = 1,
.freq_hz = freq_hz,
.phase_deg = phase_deg,
.jitter_ps = 0,
};
}
fn make_domain(name: &str, source_name: &str, freq_hz: u32) -> ClkDomain {
return ClkDomain{
.name = name,
.source_name = source_name,
.freq_hz = freq_hz,
.edge = 0,
};
}
fn make_crossing(src: &str, dst: &str, strategy: i8, data_width: u32) -> ClockCrossing {
return ClockCrossing{
.src_domain = src,
.dst_domain = dst,
.strategy = strategy,
.data_width = data_width,
};
}
// === Query functions ===
fn is_external(src: ClkSource) -> bool {
return src.kind == 0;
}
fn is_pll(src: ClkSource) -> bool {
return src.kind == 1;
}
fn period_ns(domain: ClkDomain) -> u32 {
if (domain.freq_hz == 0) {
return 0;
}
return 1000000000 / domain.freq_hz;
}
fn half_period_ns(domain: ClkDomain) -> u32 {
return period_ns(domain) / 2;
}
fn same_domain(a: ClkDomain, b: ClkDomain) -> bool {
return a.name == b.name;
}
fn needs_crossing(a: ClkDomain, b: ClkDomain) -> bool {
if (a.name == b.name) {
return false;
}
if (a.freq_hz == b.freq_hz and a.source_name == b.source_name) {
return false;
}
return true;
}
fn crossing_data_bits(cross: ClockCrossing) -> u32 {
return cross.data_width;
}
fn is_async_cross(cross: ClockCrossing) -> bool {
return cross.strategy == 2;
}
// === Tests ===
test ext_clock_is_external
given c = ext_clock("sys_clk", 12000000)
then is_external(c) == true
and is_pll(c) == false
test pll_clock_is_pll
given c = pll_clock("pll_clk", 100000000, 0)
then is_pll(c) == true
and is_external(c) == false
test period_12mhz
given d = make_domain("sys", "sys_clk", 12000000)
then period_ns(d) == 83
test period_100mhz
given d = make_domain("fast", "pll_clk", 100000000)
then period_ns(d) == 10
test half_period
given d = make_domain("sys", "sys_clk", 12000000)
then half_period_ns(d) == 41
test same_domain_true
given a = make_domain("sys", "clk", 12000000)
then same_domain(a, a) == true
test same_domain_false
given a = make_domain("sys", "clk", 12000000)
and b = make_domain("fast", "pll", 100000000)
then same_domain(a, b) == false
test needs_crossing_diff_freq
given a = make_domain("sys", "clk", 12000000)
and b = make_domain("fast", "pll", 100000000)
then needs_crossing(a, b) == true
test needs_crossing_same
given a = make_domain("sys", "clk", 12000000)
then needs_crossing(a, a) == false
test crossing_data_bits
given c = make_crossing("sys", "fast", 1, 32)
then crossing_data_bits(c) == 32
test async_cross_fifo
given c = make_crossing("sys", "fast", 2, 16)
then is_async_cross(c) == true
test sync_cross_not_async
given c = make_crossing("sys", "fast", 1, 8)
then is_async_cross(c) == false
// === Invariants ===
invariant ext_clock_has_freq
given c = ext_clock("inv", 12000000)
assert c.freq_hz > 0
invariant period_positive_for_valid_freq
given d = make_domain("inv", "clk", 12000000)
assert period_ns(d) > 0
invariant half_period_half_of_period
given d = make_domain("inv", "clk", 12000000)
assert half_period_ns(d) == period_ns(d) / 2
invariant same_domain_reflexive
given d = make_domain("inv", "clk", 12000000)
assert same_domain(d, d) == true
invariant needs_crossing_symmetric
given a = make_domain("a", "clk", 12000000)
and b = make_domain("b", "pll", 100000000)
assert needs_crossing(a, b) == needs_crossing(b, a)
// === Benchmarks ===
bench period_ns_latency
measure: nanoseconds to period_ns(make_domain("b", "c", 100000000))
target: < 50ns
}
// 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.