When they disagree
You will learn
How to triage a disagreement: which of the three is lying, and how to find out.
When spec, simulator and board disagree, one of them is lying and the disagreement itself tells you where to look. If the simulator matches the spec but the board differs, suspect constraints, timing, or the model's assumptions -- pin assignments first, they are the usual liar. The widget is the triage tool for exactly that class: before an edit to a Verilog file, every spec and generator it would touch, so a fix cannot silently wander. Breadth first (what changes?), then depth (why does this one?).
Try it
Make the triage list: for each mismatch direction (spec vs simulator, simulator vs board), name the file you would open before any other, and why.
Before editing trinet_node_core.v: 5 specs pin it by sha256 and 5 generators read those specs. radius: 5 specs, 1 level, the exact set fpga-repin walks after the edit.
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.