FSM coverage
You will learn
How state and transition coverage see the arcs a run never took.
A state machine is verified by its arcs, not its states: 4 states with 12 transitions is 12 ways to be wrong, and visiting every state can leave half the arcs cold. The spec models it directly: state points and transition points, each with a hit count, and illegal transitions that fail the report the moment one warms. The widget is the discipline in another shape: 112 files pinned by sha256 in specs, every one accounted for -- 0 lost, 0 not kept, 0 unlocated. Nothing on the list is allowed to be unvisited.
Try it
List the arcs of a 4-state FIFO FSM and mark which a read-only workload leaves cold; then find the illegal arcs in the spec and what warms them.
112 files under /tmp are pinned by sha256 in specs. /tmp is emptied at boot and all 112 are gone from it; every one has a kept copy. 0 lost, 0 not kept, 0 unlocated.
specs/fpga/coverage.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/coverage.t27
// T27 Coverage Model Specification: line, toggle and FSM coverage
// Answers one question for every simulation: what did the tests touch?
// A point with hit_count == 0 is a promise the tests never kept.
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY
module Coverage {
// === Coverage point kind ===
pub const CoverageKind = enum(i8) {
line = 0,
toggle = 1,
fsm_state = 2,
fsm_transition = 3,
branch = 4,
}
// === Line / branch point ===
pub struct LinePoint {
name : &str,
module_name : &str,
kind : i8,
line_no : u32,
hit_count : u32,
}
// === Toggle point: one signal bit, one direction ===
pub struct TogglePoint {
name : &str,
module_name : &str,
bit_index : u32,
rise : bool,
hit_count : u32,
}
// === FSM state visit ===
pub struct FsmStatePoint {
fsm_name : &str,
state_name : &str,
hit_count : u32,
}
// === FSM transition visit; illegal ones must stay at 0 hits ===
pub struct FsmTransitionPoint {
fsm_name : &str,
from_state : &str,
to_state : &str,
illegal : bool,
hit_count : u32,
}
// === Coverage report ===
pub struct CoverageReport {
name : &str,
points_total : u32,
points_hit : u32,
cycles : u32,
}
// === Constructor helpers ===
fn line_point(name: &str, module_name: &str, line_no: u32) -> LinePoint {
return LinePoint{
.name = name,
.module_name = module_name,
.kind = 0,
.line_no = line_no,
.hit_count = 0,
};
}
fn branch_point(name: &str, module_name: &str, line_no: u32) -> LinePoint {
return LinePoint{
.name = name,
.module_name = module_name,
.kind = 4,
.line_no = line_no,
.hit_count = 0,
};
}
fn toggle_rise(name: &str, module_name: &str, bit_index: u32) -> TogglePoint {
return TogglePoint{
.name = name,
.module_name = module_name,
.bit_index = bit_index,
.rise = true,
.hit_count = 0,
};
}
fn toggle_fall(name: &str, module_name: &str, bit_index: u32) -> TogglePoint {
return TogglePoint{
.name = name,
.module_name = module_name,
.bit_index = bit_index,
.rise = false,
.hit_count = 0,
};
}
fn fsm_state(fsm_name: &str, state_name: &str) -> FsmStatePoint {
return FsmStatePoint{
.fsm_name = fsm_name,
.state_name = state_name,
.hit_count = 0,
};
}
fn fsm_transition(fsm_name: &str, from_state: &str, to_state: &str) -> FsmTransitionPoint {
return FsmTransitionPoint{
.fsm_name = fsm_name,
.from_state = from_state,
.to_state = to_state,
.illegal = false,
.hit_count = 0,
};
}
fn illegal_transition(fsm_name: &str, from_state: &str, to_state: &str) -> FsmTransitionPoint {
return FsmTransitionPoint{
.fsm_name = fsm_name,
.from_state = from_state,
.to_state = to_state,
.illegal = true,
.hit_count = 0,
};
}
// === Hit accounting: copies, never side effects ===
fn mark_hit_line(p: LinePoint) -> LinePoint {
var result = p;
result.hit_count = p.hit_count + 1;
return result;
}
fn mark_hit_toggle(p: TogglePoint) -> TogglePoint {
var result = p;
result.hit_count = p.hit_count + 1;
return result;
}
fn mark_hit_state(p: FsmStatePoint) -> FsmStatePoint {
var result = p;
result.hit_count = p.hit_count + 1;
return result;
}
fn mark_hit_transition(p: FsmTransitionPoint) -> FsmTransitionPoint {
var result = p;
result.hit_count = p.hit_count + 1;
return result;
}
fn is_covered_line(p: LinePoint) -> bool {
return p.hit_count > 0;
}
fn is_covered_toggle(p: TogglePoint) -> bool {
return p.hit_count > 0;
}
fn is_covered_state(p: FsmStatePoint) -> bool {
return p.hit_count > 0;
}
fn is_covered_transition(p: FsmTransitionPoint) -> bool {
return p.hit_count > 0;
}
// === Report math: integer percent, 0 when nothing was measured ===
fn hit_lines(points: [LinePoint], count: u32) -> u32 {
var hit : u32 = 0;
var i : u32 = 0;
while i < count {
if points[i].hit_count > 0 {
hit = hit + 1;
}
i = i + 1;
}
return hit;
}
fn line_coverage_percent(points: [LinePoint], count: u32) -> u32 {
if count == 0 {
return 0;
}
return (hit_lines(points, count) * 100) / count;
}
fn hit_toggles(points: [TogglePoint], count: u32) -> u32 {
var hit : u32 = 0;
var i : u32 = 0;
while i < count {
if points[i].hit_count > 0 {
hit = hit + 1;
}
i = i + 1;
}
return hit;
}
fn toggle_coverage_percent(points: [TogglePoint], count: u32) -> u32 {
if count == 0 {
return 0;
}
return (hit_toggles(points, count) * 100) / count;
}
// === FSM: every state and arc; illegal arcs must stay cold ===
fn hit_states(points: [FsmStatePoint], count: u32) -> u32 {
var hit : u32 = 0;
var i : u32 = 0;
while i < count {
if points[i].hit_count > 0 {
hit = hit + 1;
}
i = i + 1;
}
return hit;
}
fn hit_transitions(points: [FsmTransitionPoint], count: u32) -> u32 {
var hit : u32 = 0;
var i : u32 = 0;
while i < count {
if points[i].hit_count > 0 {
hit = hit + 1;
}
i = i + 1;
}
return hit;
}
fn illegal_hits(points: [FsmTransitionPoint], count: u32) -> u32 {
var hit : u32 = 0;
var i : u32 = 0;
while i < count {
if points[i].illegal == true {
if points[i].hit_count > 0 {
hit = hit + 1;
}
}
i = i + 1;
}
return hit;
}
fn fsm_report(name: &str, states: [FsmStatePoint], state_count: u32,
transitions: [FsmTransitionPoint], transition_count: u32) -> CoverageReport {
return CoverageReport{
.name = name,
.points_total = state_count + transition_count,
.points_hit = hit_states(states, state_count) + hit_transitions(transitions, transition_count),
.cycles = 0,
};
}
fn report_percent(r: CoverageReport) -> u32 {
if r.points_total == 0 {
return 0;
}
return (r.points_hit * 100) / r.points_total;
}
// === Validation ===
fn validate_line(p: LinePoint) -> u32 {
var errors : u32 = 0;
if p.name == "" {
errors = errors + 1;
}
if p.module_name == "" {
errors = errors + 1;
}
if p.line_no == 0 {
errors = errors + 1;
}
return errors;
}
fn validate_toggle(p: TogglePoint) -> u32 {
var errors : u32 = 0;
if p.name == "" {
errors = errors + 1;
}
if p.module_name == "" {
errors = errors + 1;
}
return errors;
}
fn validate_state(p: FsmStatePoint) -> u32 {
var errors : u32 = 0;
if p.fsm_name == "" {
errors = errors + 1;
}
if p.state_name == "" {
errors = errors + 1;
}
return errors;
}
fn validate_transition(p: FsmTransitionPoint) -> u32 {
var errors : u32 = 0;
if p.fsm_name == "" {
errors = errors + 1;
}
if p.from_state == "" {
errors = errors + 1;
}
if p.to_state == "" {
errors = errors + 1;
}
return errors;
}
fn validate_report(r: CoverageReport) -> u32 {
var errors : u32 = 0;
if r.name == "" {
errors = errors + 1;
}
if r.points_hit > r.points_total {
errors = errors + 1;
}
return errors;
}
// === Tests ===
test line_point_creation
given p = line_point("uart_tx.latch", "UART_TX", 42)
then p.kind == 0
and p.line_no == 42
and p.hit_count == 0
test branch_point_creation
given p = branch_point("fifo.full", "FIFO", 88)
then p.kind == 4
and p.line_no == 88
test toggle_points_creation
given rise = toggle_rise("txd", "UART_TX", 0)
and fall = toggle_fall("txd", "UART_TX", 0)
then rise.rise == true
and fall.rise == false
test fsm_points_creation
given s = fsm_state("uart_ctrl", "IDLE")
and t = fsm_transition("uart_ctrl", "IDLE", "SEND")
then s.state_name == "IDLE"
and t.from_state == "IDLE"
and t.to_state == "SEND"
and t.illegal == false
test illegal_transition_creation
given t = illegal_transition("uart_ctrl", "SEND", "IDLE")
then t.illegal == true
and t.hit_count == 0
test mark_hit_counts
given p0 = line_point("a", "M", 1)
and p1 = mark_hit_line(p0)
and p2 = mark_hit_line(p1)
then p0.hit_count == 0
and p2.hit_count == 2
and is_covered_line(p0) == false
and is_covered_line(p2) == true
test line_coverage_percent_mixed
given a = mark_hit_line(line_point("a", "M", 1))
and b = mark_hit_line(line_point("b", "M", 2))
and c = line_point("c", "M", 3)
and d = line_point("d", "M", 4)
then hit_lines([a, b, c, d], 4) == 2
and line_coverage_percent([a, b, c, d], 4) == 50
test line_coverage_percent_full
given a = mark_hit_line(line_point("a", "M", 1))
and b = mark_hit_line(line_point("b", "M", 2))
then line_coverage_percent([a, b], 2) == 100
test line_coverage_percent_empty
then line_coverage_percent([], 0) == 0
test toggle_coverage_percent
given r = mark_hit_toggle(toggle_rise("txd", "UART_TX", 0))
and f = toggle_fall("txd", "UART_TX", 0)
and r1 = mark_hit_toggle(toggle_rise("rxd", "UART_RX", 1))
and f1 = toggle_fall("rxd", "UART_RX", 1)
then hit_toggles([r, f, r1, f1], 4) == 2
and toggle_coverage_percent([r, f, r1, f1], 4) == 50
test fsm_coverage_counts
given idle = mark_hit_state(fsm_state("uart_ctrl", "IDLE"))
and send = mark_hit_state(fsm_state("uart_ctrl", "SEND"))
and done = fsm_state("uart_ctrl", "DONE")
and t1 = mark_hit_transition(fsm_transition("uart_ctrl", "IDLE", "SEND"))
and t2 = fsm_transition("uart_ctrl", "SEND", "DONE")
then hit_states([idle, send, done], 3) == 2
and hit_transitions([t1, t2], 2) == 1
test illegal_hits_zero_when_cold
given x = illegal_transition("uart_ctrl", "SEND", "IDLE")
then illegal_hits([x], 1) == 0
test illegal_hits_counts_when_warm
given x = mark_hit_transition(illegal_transition("uart_ctrl", "SEND", "IDLE"))
then illegal_hits([x], 1) == 1
test fsm_report_totals
given idle = mark_hit_state(fsm_state("uart_ctrl", "IDLE"))
and send = fsm_state("uart_ctrl", "SEND")
and t1 = mark_hit_transition(fsm_transition("uart_ctrl", "IDLE", "SEND"))
and t2 = fsm_transition("uart_ctrl", "SEND", "IDLE")
and r = fsm_report("uart_ctrl", [idle, send], 2, [t1, t2], 2)
then r.points_total == 4
and r.points_hit == 2
and report_percent(r) == 50
test report_percent_empty
given r = CoverageReport{.name = "empty", .points_total = 0, .points_hit = 0, .cycles = 0}
then report_percent(r) == 0
test validate_line_ok
given p = line_point("a", "M", 1)
then validate_line(p) == 0
test validate_line_empty_name
given p = line_point("", "M", 1)
then validate_line(p) > 0
test validate_line_zero_line
given p = line_point("a", "M", 0)
then validate_line(p) > 0
test validate_toggle_ok
given p = toggle_rise("txd", "UART_TX", 0)
then validate_toggle(p) == 0
test validate_toggle_empty_module
given p = toggle_rise("txd", "", 0)
then validate_toggle(p) > 0
test validate_state_ok
given p = fsm_state("uart_ctrl", "IDLE")
then validate_state(p) == 0
test validate_state_empty
given p = fsm_state("", "")
then validate_state(p) > 0
test validate_transition_ok
given p = fsm_transition("uart_ctrl", "IDLE", "SEND")
then validate_transition(p) == 0
test validate_transition_empty_to
given p = fsm_transition("uart_ctrl", "IDLE", "")
then validate_transition(p) > 0
test validate_report_ok
given r = fsm_report("uart_ctrl", [], 0, [], 0)
then validate_report(r) == 0
test validate_report_hit_over_total
given r = CoverageReport{.name = "bad", .points_total = 1, .points_hit = 2, .cycles = 0}
then validate_report(r) > 0
// === Invariants ===
invariant line_percent_bounded
given a = mark_hit_line(line_point("a", "M", 1))
and b = line_point("b", "M", 2)
assert line_coverage_percent([a, b], 2) <= 100
invariant illegal_must_stay_cold
given x = illegal_transition("uart_ctrl", "SEND", "IDLE")
assert illegal_hits([x], 1) == 0
invariant validate_non_negative
given p = line_point("inv", "M", 1)
assert validate_line(p) >= 0
invariant report_percent_bounded
given r = fsm_report("inv", [], 0, [], 0)
assert report_percent(r) <= 100
// === Benchmarks ===
bench line_percent_latency
measure: nanoseconds for line_coverage_percent([], 0)
target: < 50ns
}
// phi^2 + 1/phi^2 = 3 | TRINITY
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.