Код Грея
Вы узнаете
Почему код Грея меняет по одному биту за шаг и чего не может увидеть набор тестов, не читающий указатели.
Код Грея меняет ровно один бит за шаг, поэтому сэмпл, взятый посреди изменения, даёт один из двух соседних кодов — ошибку на единицу, но не мусор. FIFO, чьи указатели чтения и записи считают по Грею, можно безопасно сэмплировать через домены, и выводимые из них флаги держатся. Запись подкладывает мутацию, которую Грей поймал бы с поличным, если бы тесты смотрели: (state.head_ptr + 1) превращается в + 3, и все тесты по-прежнему проходят, потому что набор утверждает заполнение и флаги, но никогда значения указателей. Набор тестов защищает то, что он читает; кодировку защищает правило следующего урока, а не эти тесты. Запись восстанавливает спеку и печатает её sha256.
Попробуйте
В записи найдите строку sed и убедитесь, что ни один тест не упал; затем в окне спеки найдите утверждения о заполнении и флагах и укажите дыру, в которую проскользнула мутация.
head_ptr + 1 to + 3 in one sed: every test still passes, because the suite asserts fill counts and flags, never pointer values -- the exact hole a torn multi-bit pointer would slip through; 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
Все уроки
Модуль 1 · Что такое тактовый сигнал
Один фронт, один мир: всё, что делит фронт тактового сигнала, делит и мир; период и джиттер настоящего фронта и место, где тактовый сигнал входит в плату.
Модуль 2 · Деревья тактового сигнала
Перекос и задержка прохождения, глобальная сеть буферов и ловушка стробирования клока логикой.
Модуль 3 · PLL и MMCM
Умножить и поделить один тактовый сигнал в другой, сдвинуть его фазу шагами VCO и какие тактовые сигналы анализатор считает родственными.
Модуль 4 · Сбросы
Ассертировать асинхронно, снимать синхронно: три вида сброса, конвейер снятия и дерево, которое растит сброс.
Модуль 5 · Метастабильность
Окно setup-hold, среднее время между отказами в целочисленной арифметике и два триггера, которые это чинят.
Модуль 6 · Пересечение многих бит
Почему двоичная шина рвётся, почему код Грея нет, и рукопожатие, переносящее импульс между мирами.
Модуль 7 · Асинхронный FIFO
Указатели, флаги и глубина: буфер, переносящий поток между двумя тактовыми сигналами.
Модуль 8 · Ограничения
Строки, сообщающие анализатору, что такое тактовый сигнал, какие пути не проверять и чему должны соответствовать выводы.
Модуль 9 · На плате
Отчёт CDC, одно пересечение, захваченное на триггерах, и дифф битстрима, замыкающий курс.