Среднее время между отказами
Вы узнаете
Как MTBF назначает пересечению цену в целочисленной арифметике log2 и какие константы в ней допущения.
MTBF назначает пересечению цену: e^(T/tau), делённое на F_clk, F_data и окно W, — форма, которой учит Xilinx WP323. mtbf.t27, написанная для этого курса, считает её в целочисленном log2 с 10 дробными битами, потому что честный ответ переполняет любой целочисленный счёт секунд. tau 50 пс и W 10 пс помечены как допущения: вендоры публикуют параметры триггеров лишь частично. На приёме 100 МГц потока 10 МГц 1 ступень оставляет -200 пс запаса и Q10 log2-MTBF -19513 — меньше двух микросекунд; 2 ступени оставляют 9800 пс и 275887 — дольше любых часов, которые вселенная успеет протикать. Запись запускает нативный t27c: проходят 15 тестов, 4 инварианта comptime.
Попробуйте
В записи найдите grep, перечисляющий допущения; затем в окне спеки посчитайте, что сулит stage_gain_q10() на 100 МГц за ещё один триггер.

t27c 0.4.0 on a laptop (macOS): 15 tests pass natively -- the WP323 form in Q10 log2, one flop negative slack, two flops astronomical, and the grep that shows the assumptions.
specs/fpga/mtbf.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/mtbf.t27
// Metastability MTBF model for Trinity T27 FPGA HIR
// Integer-only log2 arithmetic, no floats anywhere
// phi^2 + 1/phi^2 = 3 | TRINITY
//
// THE MODEL. MTBF = e^(T_slack / tau) / (F_clk * F_data * W), the form taught
// by Xilinx WP323, "Understanding Metastability in FPGAs": T_slack is the time
// a synchronizer's first flop is given to resolve, tau is its resolve time
// constant, W is the metastability aperture (window) of that flop, F_clk is
// the receiving clock and F_data the transition rate of the asynchronous
// input. Because e^(T/tau) overflows any integer seconds count long before a
// real synchronizer becomes safe, this file works in log2 of seconds with 10
// fractional bits (Q10): every MTBF below is log2(MTBF) * 1024.
//
// THE CONSTANTS ARE ASSUMPTIONS, NOT DATASHEET NUMBERS. Xilinx publishes flop
// metastability parameters only partially (WP323 gives the method and some
// measured taus for older families; DS181 does not list W or tau per device),
// so tau = 50 ps and W = 10 ps here are labelled teaching assumptions in the
// WP323 form. A design that needs a real number measures its own, or reads it
// from the vendor's CDC report. The lesson these numbers teach -- each extra
// synchronizer stage multiplies MTBF by 2^(T_clk * log2 e / tau) -- does not
// depend on the exact constants, and the tests below only use differences and
// the model's own arithmetic.
module Mtbf {
// === Model constants (assumptions; see header) ===
fn tau_ps() -> u32 {
return 50; // resolve time constant, ASSUMPTION (WP323 form)
}
fn window_ps() -> u32 {
return 10; // metastability aperture, ASSUMPTION (WP323 form)
}
fn setup_ps() -> u32 {
return 200; // flop setup, same teaching value as timing.t27
}
pub const LOG2_E_Q10 : i64 = 1477; // 1024 * log2(e) = 1477.33
pub const LOG2_1E6_Q10 : i64 = 20410; // 1024 * log2(1e6) = 20409.97
pub const LOG2_1E12_Q10 : i64 = 40820; // 1024 * log2(1e12) = 40819.85
pub const MAX_STAGES : u32 = 8;
// === Crossing model ===
pub struct MtbfModel {
name : &str,
clk_mhz : u32, // the receiving (destination) clock
data_mhz : u32, // transitions per second of the async input, in MHz
}
fn mtbf_model(name: &str, clk_mhz: u32, data_mhz: u32) -> MtbfModel {
return MtbfModel{
.name = name,
.clk_mhz = clk_mhz,
.data_mhz = data_mhz,
};
}
fn period_ps(clk_mhz: u32) -> u32 {
if clk_mhz == 0 {
return 0;
}
return 1000000 / clk_mhz;
}
// Time the first flop is given to resolve: an N-stage synchronizer leaves
// (N - 1) full periods minus one setup before its output is sampled again
fn resolve_slack_ps(m: MtbfModel, stages: u32) -> i64 {
var p : i64 = period_ps(m.clk_mhz) as i64;
return (stages as i64 - 1) * p - setup_ps() as i64;
}
// Integer log2 in Q10: bit-normalize to [2^20, 2^21), then one fractional
// bit per squaring. Exact for powers of two, +-1 unit otherwise.
fn log2_q10(n: u32) -> i64 {
if n < 2 {
return 0;
}
var x : i64 = n as i64;
var e : i64 = 0;
while x < 1048576 {
x = x * 2;
e = e - 1;
}
while x >= 2097152 {
x = x / 2;
e = e + 1;
}
var frac : i64 = 0;
var w : i64 = 512;
var i : u32 = 0;
while i < 10 {
x = (x * x) >> 20;
if x >= 2097152 {
x = x / 2;
frac = frac + w;
}
w = w / 2;
i = i + 1;
}
return (e + 20) * 1024 + frac;
}
// log2(MTBF in seconds) * 1024 for a given resolve slack, per the header
fn mtbf_log2_q10(m: MtbfModel, slack_ps: i64) -> i64 {
var acc : i64 = slack_ps * LOG2_E_Q10 / (tau_ps() as i64);
acc = acc - (log2_q10(m.clk_mhz) + LOG2_1E6_Q10);
acc = acc - (log2_q10(m.data_mhz) + LOG2_1E6_Q10);
acc = acc + (LOG2_1E12_Q10 - log2_q10(window_ps()));
return acc;
}
// One more stage buys T_clk * log2(e) / tau of log2-MTBF, exactly
fn stage_gain_q10(m: MtbfModel) -> i64 {
return period_ps(m.clk_mhz) as i64 * LOG2_E_Q10 / (tau_ps() as i64);
}
// MTBF of an N-stage synchronizer on this crossing
fn synchronizer_mtbf_q10(m: MtbfModel, stages: u32) -> i64 {
return mtbf_log2_q10(m, resolve_slack_ps(m, stages));
}
// Smallest stage count (1..MAX_STAGES) whose MTBF reaches the Q10 target;
// returns MAX_STAGES when even that does not reach it
fn stages_for_mtbf(m: MtbfModel, target_q10: i64) -> u32 {
var stages : u32 = 1;
while stages < MAX_STAGES {
if synchronizer_mtbf_q10(m, stages) >= target_q10 {
return stages;
}
stages = stages + 1;
}
return stages;
}
// === Validation ===
fn validate_model(m: MtbfModel) -> u32 {
var errors : u32 = 0;
if m.name == "" {
errors = errors + 1;
}
if m.clk_mhz == 0 {
errors = errors + 1;
}
if m.data_mhz == 0 {
errors = errors + 1;
}
return errors;
}
// === Tests ===
test log2_q10_is_exact_for_powers_of_two
then log2_q10(1) == 0
and log2_q10(2) == 1024
and log2_q10(1024) == 10240
and log2_q10(4096) == 12288
test log2_q10_tracks_the_true_value
then log2_q10(10) == 3401
and log2_q10(100) == 6803
and log2_q10(1000000) == 20409
test a_100mhz_clock_has_a_10000ps_period
then period_ps(100) == 10000
and period_ps(200) == 5000
test one_flop_gets_negative_slack
given m = mtbf_model("cross", 100, 10)
then resolve_slack_ps(m, 1) == -200
test two_flops_get_a_period_minus_setup
given m = mtbf_model("cross", 100, 10)
then resolve_slack_ps(m, 2) == 9800
test one_flop_is_not_enough
given m = mtbf_model("cross", 100, 10)
then synchronizer_mtbf_q10(m, 1) == -19513
test two_flops_reach_astronomical_mtbf
given m = mtbf_model("cross", 100, 10)
then synchronizer_mtbf_q10(m, 2) == 275887
test a_billion_seconds_needs_two_flops_here
given m = mtbf_model("cross", 100, 10)
and target = 30 * 1024
then stages_for_mtbf(m, target) == 2
test a_higher_bar_needs_a_third_flop
given m = mtbf_model("cross", 100, 10)
and target = 280000
then synchronizer_mtbf_q10(m, 2) < target
and stages_for_mtbf(m, target) == 3
test a_faster_clock_makes_the_same_crossing_worse
given slow = mtbf_model("slow", 50, 10)
and fast = mtbf_model("fast", 200, 10)
then synchronizer_mtbf_q10(slow, 2) > synchronizer_mtbf_q10(fast, 2)
test busier_data_makes_the_crossing_worse
given quiet = mtbf_model("quiet", 100, 1)
and busy = mtbf_model("busy", 100, 50)
then synchronizer_mtbf_q10(quiet, 2) > synchronizer_mtbf_q10(busy, 2)
test mtbf_rises_exponentially_with_slack
given m = mtbf_model("cross", 100, 10)
then mtbf_log2_q10(m, 500) == 1165
and mtbf_log2_q10(m, 1000) == 15935
and mtbf_log2_q10(m, 1000) - mtbf_log2_q10(m, 500) > 10000
test one_more_stage_gains_exactly_the_period
given m = mtbf_model("cross", 100, 10)
then stage_gain_q10(m) == 295400
and synchronizer_mtbf_q10(m, 3) - synchronizer_mtbf_q10(m, 2) == stage_gain_q10(m)
test validate_accepts_a_named_crossing
given m = mtbf_model("cross", 100, 10)
then validate_model(m) == 0
test validate_rejects_a_clock_of_zero
given m = mtbf_model("bad", 0, 10)
then validate_model(m) > 0
// === Invariants ===
invariant mtbf_never_falls_as_slack_grows
given m = mtbf_model("inv", 100, 10)
assert mtbf_log2_q10(m, 1000) > mtbf_log2_q10(m, 500)
invariant the_stage_gain_is_positive
given m = mtbf_model("inv", 100, 10)
assert stage_gain_q10(m) > 0
invariant two_flops_beat_one
given m = mtbf_model("inv", 100, 10)
assert synchronizer_mtbf_q10(m, 2) > synchronizer_mtbf_q10(m, 1)
invariant the_window_and_tau_are_stated_assumptions
assert tau_ps() == 50
and window_ps() == 10
// === Benchmarks ===
bench log2_cost
measure: nanoseconds for log2_q10(1000000)
target: < 100ns
bench mtbf_cost
measure: nanoseconds for synchronizer_mtbf_q10(mtbf_model("b", 100, 10), 2)
target: < 200ns
}
// phi^2 + 1/phi^2 = 3 | TRINITY
Все уроки
Модуль 1 · Что такое тактовый сигнал
Один фронт, один мир: всё, что делит фронт тактового сигнала, делит и мир; период и джиттер настоящего фронта и место, где тактовый сигнал входит в плату.
Модуль 2 · Деревья тактового сигнала
Перекос и задержка прохождения, глобальная сеть буферов и ловушка стробирования клока логикой.
Модуль 3 · PLL и MMCM
Умножить и поделить один тактовый сигнал в другой, сдвинуть его фазу шагами VCO и какие тактовые сигналы анализатор считает родственными.
Модуль 4 · Сбросы
Ассертировать асинхронно, снимать синхронно: три вида сброса, конвейер снятия и дерево, которое растит сброс.
Модуль 5 · Метастабильность
Окно setup-hold, среднее время между отказами в целочисленной арифметике и два триггера, которые это чинят.
Модуль 6 · Пересечение многих бит
Почему двоичная шина рвётся, почему код Грея нет, и рукопожатие, переносящее импульс между мирами.
Модуль 7 · Асинхронный FIFO
Указатели, флаги и глубина: буфер, переносящий поток между двумя тактовыми сигналами.
Модуль 8 · Ограничения
Строки, сообщающие анализатору, что такое тактовый сигнал, какие пути не проверять и чему должны соответствовать выводы.
Модуль 9 · На плате
Отчёт CDC, одно пересечение, захваченное на триггерах, и дифф битстрима, замыкающий курс.