Course: Verifying hardware with t27 -- testbenches, waveforms, formal, mutation (9x3, hardware track) #1483

Parent epic: #1476

Course id: verify-hardware
Audience: hardware engineers (RTL / FPGA / ASIC).
Prerequisites: Course 0 (t27 basics) module tests-and-functions; Course 1 module program.

Why this course

Verification is more than half of real hardware work, and it is where t27's claim (the spec IS the test) is strongest. The repo has 30 *_tb testbenches, VCD tracing and comparison, a formal spec, cosimulation and mutation tooling (tri x7-mutate). None of it is taught. Verification engineers are a large audience that the current courses ignore.

What already exists in the repo (grounding)

• fpga/testbench.t27, 30 files under fpga/testbench/*_tb.t27, fpga/simulator.t27
• fpga/vcd_trace.t27, fpga/vcd_conformance_compare.t27
• fpga/formal.t27 + formal_tb, fpga/verification/build_verify.t27
• conformance/e2e_scenarios.t27, numeric/formats_catalog.t27 (bit-exact vectors)
• tools/trios/tri/x7-mutate.t27, fpga-batch-cosim.t27, fpga-selftest.t27

Decomposition: 9 modules x 3 lessons

Module 1 -- why-verify: the spec is the golden model

Module 2 -- testbenches: stimulus, check, report

Module 3 -- waveforms: reading what happened

Module 4 -- conformance-vectors: bit-exact or nothing

Module 5 -- cosimulation: spec, RTL and board must agree

Module 6 -- coverage: what you did not test

Module 7 -- formal: proof instead of samples

Module 8 -- mutation: testing the tests

Module 9 -- sign-off: done means proven

Specs that do not exist yet (write in gHashTag/t27 first)

• fpga/coverage.t27 -- line, toggle and FSM coverage model

Honesty notes and traps

• The browser runner cannot run most *_tb specs today (calls, locals, struct fields). This course is the strongest reason to land that issue first.
• Avoid repeating Course 1 lesson tests-are-the-spec; link to it.

Acceptance criteria

• specs/course/<id>.t27 + <id>-ru.t27 exist, registered in specs/course/courses.t27, built by course-from-spec.mjs (recipe: specs/course_recipe/course-27.t27).
• Exactly 9 modules x 3 lessons = 27 lessons; every lesson names one widget and one spec.
• Every lesson spec compiles AND its test blocks pass in the reader's browser (blocked by the browser-runner issue), or the lesson says plainly that it is a recorded tri cast and links the recording.
• Every number on a page comes from real tool output named in the widget's DATA_SOURCES (yosys / nextpnr / board run / spec test). No invented figures.
• Board named on every hardware page (Wukong xc7a200tfgg676 vs AX7203 xc7a200tfbg484 vs Arty A7 / XC7A100T).
• Black-and-white share cards and SEO pages generated for all 27 lessons (EN + RU).
• The course PR carries a blog post: EN body + RU ruBody.
• Lessons that need a spec that does not exist yet are listed as sub-tasks (spec first in gHashTag/t27, then copied here).

Blocked by: #1477 (browser test runner) for every lesson whose spec uses calls, locals or struct fields in tests.