Three-way agreement
You will learn
How spec, simulator and board are held to one answer, and what each one is trusted for.
Three answers, one question. The spec says what should happen; the simulator says what a model of the silicon does; the board says what the silicon does. The widget is the rehearsal for that agreement with the board taken out of the loop: 26 checks, no board, no RTL -- a clean link returns every receipt with no retransmit, 11 loss and fault cases recover, and a lie, a duplicate or a wrong-key answer stops the run. When all three agree on the bench Artix-7 XC7A200T, you are done arguing.
Try it
Find the 11 recovery cases in the batch rehearsal and the three answers that stop the run; then say which of the three (spec, simulator, board) each one guards.
26 checks, no board, no RTL: a clean link returns every receipt with no retransmit, 11 loss and fault cases recover, and a lie, a duplicate or a wrong-key answer stops the run. self-test: PASS.
specs/tools/trios/tri/fpga-batch-cosim.t27
// SPDX-License-Identifier: Apache-2.0
; specs/tools/trios/tri/fpga-batch-cosim.t27 -- tool gHashTag/BrowserOS:tri/fpga-batch-cosim, the `tri fpga-batch-cosim` command of the trios loop CLI
; Generated by apps/website/scripts/tools-from-trios-tri.mjs from gHashTag/BrowserOS:trios/bin/tri at 7366096248df; do not edit.
; The CLI the loop timers run (`tri drift` holds ~/.local/bin/tri to the tracked copy). It is another program than
; the Rust tri of gHashTag/t27 and the Zig tri of gHashTag/trinity, so the ID is repository-qualified.
; A card is data and carries no test block. ASCII only (L3). phi^2 + 1/phi^2 = 3 | TRINITY
module tool_trios_tri_fpga_batch_cosim;
pub const KIND : str = "tool";
pub const FAMILY : str = "tri-cli";
pub const ID : str = "gHashTag/BrowserOS:tri/fpga-batch-cosim";
pub const REPO : str = "gHashTag/BrowserOS";
pub const QUALIFIED_ID : str = "gHashTag/BrowserOS:tri/fpga-batch-cosim";
pub const SCHEMA : u32 = 2;
pub const COMMAND : str = "tri fpga-batch-cosim";
; The case arm of the dispatcher and the first line of it that does the work.
pub const VARIANT : str = "case arm `fpga-batch-cosim)`, line 1937";
pub const SOURCE : str = "trios/bin/tri";
pub const ENTRY : str = "trios/bin/tri";
pub const SOURCE_COMMIT : str = "7366096248dfb09893e9a7d1a0f1c56ced13d16e";
pub const ROUTED : bool = true;
pub const DISPATCH : str = "exec python3 \"$(git rev-parse --show-toplevel 2>/dev/null || echo .)/conformance/tern_tc_batch_rtl_cosim.py\" \"$@\"";
pub const DOCUMENTED : bool = true;
pub const HELP_LINE : str = "tri fpga-batch-cosim [--passes wq|both] [--keep DIR] -- conformance/tern_tc_batch_rtl_cosim.py: the rehearsal's recorded request stream replayed through formal/tern_tc_layer_rtl_tb.v under iverilog vs a fresh HuntingBatchCell (byte-for-byte; negative control = blind 24-byte framing). Pre-built red: FAILs on the current core at the first SETX tag (no SETX/DOT6 ops yet); PASS is the TERN_TC_BATCH_RTL_PLAN.md core edit's gate. The walk_answers precondition refuses non-adjudicable streams (out-of-range phantom frames: model drops, RTL will answer) loudly instead of reporting a mystery diff; needs iverilog+vvp";
pub const CATEGORY : str = "AX7203 board (tern_tc: receipts, UART, formats)";
pub const ABOUT : str = "conformance/tern_tc_batch_rtl_cosim.py: the rehearsal's recorded request stream replayed through formal/tern_tc_layer_rtl_tb.v under iverilog vs a fresh HuntingBatchCell (byte-for-byte; negative control = blind 24-byte framing). Pre-built red: FAILs on the current core at the first SETX tag (no SETX/DOT6 ops yet); PASS is the TERN_TC_BATCH_RTL_PLAN.md core edit's gate. The walk_answers precondition refuses non-adjudicable streams (out-of-range phantom frames: model drops, RTL will answer) loudly instead of reporting a mystery diff; needs iverilog+vvp";
pub const ABOUT_SOURCE : str = "`tri help` (the heredoc under the help arm of trios/bin/tri)";
pub const ACTIONS : [0]str = [];
pub const ACTIONS_ABOUT : [0]str = [];
pub const ARGS : [2]str = ["[--passes wq|both]", "[--keep DIR]"];
pub const AGENTS : [0]str = [];
pub const AGENTS_NOTE : str = "No source binds an agent letter to this command: the trios CLI is not named by docs/agents/AGENTS_ALPHABET.md or .claude/agents/*.md of gHashTag/t27.";
pub const WHEN_TO_USE : str = "conformance/tern_tc_batch_rtl_cosim.py: the rehearsal's recorded request stream replayed through formal/tern_tc_layer_rtl_tb.v under iverilog vs a fresh HuntingBatchCell (byte-for-byte; negative control = blind 24-byte framing). Pre-built red: FAILs on the current core at the first SETX tag (no SETX/DOT6 ops yet); PASS is the TERN_TC_BATCH_RTL_PLAN.md core edit's gate. The walk_answers precondition refuses non-adjudicable streams (out-of-range phantom frames: model drops, RTL will answer) loudly instead of reporting a mystery diff; needs iverilog+vvp";
pub const WITNESS : str = "source-parse";
pub const WITNESS_SOURCE : str = "gHashTag/BrowserOS:trios/bin/tri at 7366096248dfb09893e9a7d1a0f1c56ced13d16e, read as text (the help heredoc and the top-level case arms); the CLI was not run";
pub const ENABLED : bool = true;
All lessons
Module 1 · Why verify
Designs that compile and are wrong, the model that decides, and the plan written before the code.
Module 2 · Testbenches
Stimulus, checks and a verdict, written as one spec beside the design it judges.
Module 3 · Waveforms
A trace of every signal, read the way a hardware engineer reads it, and two runs compared.
Module 4 · Conformance vectors
Cases with the answer written beside them, kept where the compiler can reach them.
Module 5 · Cosimulation
Spec, simulator and board agreeing on the bench Artix-7 XC7A200T, and what to do when they do not.
Module 6 · Coverage
What the tests touched: lines, toggles, states, and what that number hides.
Module 7 · Formal
Assertions that hold every cycle, bounded search for a counterexample, and why a proof needs induction.
Module 8 · Mutation
Break the design on purpose and count what the tests catch.
Module 9 · Sign-off
One command, every receipt, a clean verdict you can show.