t27c on mtbf.t27 -- MTBF in integer log2, native
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.
t27c on mtbf.t27 -- MTBF in integer log2, native
--- test report: specs/fpga/mtbf.t27 ---
tests 15
pass 15
FAIL 0
invariants 4 proved -- comptime, so compiling IS the check
rate 100.0%
runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):
4 log2_q10_is_exact_for_powers_of_two
3 log2_q10_tracks_the_true_value
2 a_100mhz_clock_has_a_10000ps_period
1 one_flop_gets_negative_slack
1 two_flops_get_a_period_minus_setup
1 one_flop_is_not_enough
1 two_flops_reach_astronomical_mtbf
1 a_billion_seconds_needs_two_flops_here
2 a_higher_bar_needs_a_third_flop
1 a_faster_clock_makes_the_same_crossing_worse
1 busier_data_makes_the_crossing_worse
3 mtbf_rises_exponentially_with_slack
2 one_more_stage_gains_exactly_the_period
1 validate_accepts_a_named_crossing
1 validate_rejects_a_clock_of_zero
vacuous passes 0 of 15 (passed with 0 runtime asserts executed)
files $ grep -n 'ASSUMPTION' specs/fpga/mtbf.t27 | head -4
16:// THE CONSTANTS ARE ASSUMPTIONS, NOT DATASHEET NUMBERS. Xilinx publishes flop
31: return 50; // resolve time constant, ASSUMPTION (WP323 form)
35: return 10; // metastability aperture, ASSUMPTION (WP323 form)
files $
recorded 2026-10-07 17:35 UTC real 12.7 s shown 12.5 s exit codes 0 0 0
$ t27c --version
$ t27c test-report specs/fpga/mtbf.t27 --specs-dir specs
$ grep -n 'ASSUMPTION' specs/fpga/mtbf.t27 | head -4
Staged: the prompt and the typing. Real: every byte the commands printed, at the time they printed it. Any silence longer than 2 s is shown for 2 s, and the title bar says so while it happens. Edited: home directory shown as ~.