The complete verification program for the SHDL project: what must be tested, how it is verified,
what is already covered, and what remains. Companion to SHDL_Project.md, shdl.md,
base_shdl.md, and shdlc_goals.md.
SHDL's project principles demand correctness before performance and a test corpus mature
enough that the flattener and compiler can be refactored or reimplemented with confidence. This
document defines the golden test suite: the closed list of obligations that, when all green,
justify the claim "SHDL contains no known bugs and no untested normative behavior."
"Extremely certain" is operationalized as five concrete conditions:
Spec closure — every normative statement in shdl.md, base_shdl.md, and
shdlc_goals.md maps to at least one test (this document is that mapping).
Diagnostic closure — every diagnostic raise site (not just every code) is exercised by
at least one test asserting code, message substance, and position.
Oracle closure — every executable artifact is validated bit-exactly, cycle-by-cycle,
against an independent reference, on fixed corpora and randomized inputs.
Crash closure — no user input, however malformed, produces an uncaught Python exception,
a C compiler error, or undefined behavior; failures are always structured diagnostics.
Determinism closure — byte-identical Base SHDL, byte-identical generated C, identical
traces: across runs, hash seeds, optimization levels, build modes, and platforms.
Each domain below lists its obligations with stable IDs. Status legend:
✅ covered (exists today) · 🟡 partial (exists, with named holes) · ❌ missing ·
⚪ blocked (component not yet built; obligation defined now, activated at build time).
│ trace equality on random + exhaustive stimulus (test_equivalence)
▼
BaseEval ── reference interpreter for Base SHDL (THE ground truth, §7.1 shdlc_goals)
│ lockstep differential, every port, every cycle (DualSim)
▼
Compiled C library (release; later: debug build, optimization tiers, backends)
│ replayed bit-exactly against (traces sourced from BaseEval, never from C)
▼
Conformance corpus (v1.1.0 — 38 cases / 40 traces, provenance: never from C)
Independence rules (already in force, must never be weakened):
Conformance traces are generated by OracleSim (BaseEval) only — never by the C
implementation under test.
expected.base.shdl files are frozen flattener output with pinned timestamps; regeneration is
a deliberate, reviewed, manifest-versioned act, never a side effect of a failing test.
Every future backend/tier validates against both the corpus and live BaseEval lockstep.
Diagnostics completeness assertion (test_diagnostics_matrix): the set of tested codes
must equal the ErrorCode enum — a new code cannot land untested. Extend (see DIA-2) to
per-raise-site coverage.
STRICT_CFLAGS (-std=c11 -Wall -Wextra -Werror -pedantic -O2 -fPIC -shared -fvisibility=hidden): every harness-driven generated-C build in the suite is a zero-warning
proof. (The CLI subprocess tests build with release DEFAULT_CFLAGS, which carry no warning
flags — the CCT-3 hole.)
Corpus integrity test: manifest↔disk bijection, feature-coverage check, minimum case count
guard (≥38 Tier A, ≥40 traces) plus per-golden content hashes (CNF-9 drift fence) so silent
corpus loss or coordinated regen fails loudly.
Seed-stable randomness: all randomized tests derive seeds from fixture names
(zlib.crc32), and failures embed the full netlist/action log for replay.
All token kinds: 29 token kinds (28 + EOF), all one- and two-char operators, keywords vs identifiers
✅
LEX-2
Literal forms: decimal, hex 0x, binary 0b, value correctness
✅
LEX-3
Uppercase prefixes 0X / 0B accepted per spec §2.3 — implemented (lexer.py handles both cases); pure test gap
✅
LEX-4
All three comment forms (#, "…", """…""") stripped; doc comment captured only when leading
✅
LEX-5
1-based line/column tracking with file attribution
✅
LEX-6
E0101 per raise site (6 sites in lexer.py): unexpected char, unterminated """, unterminated "…", hex with no digits, binary with no digits, ident char trailing a literal (12ab, 0xFG)
✅ (all 6 sites — test_lexer.py LEX-6 block)
LEX-7
Boundary inputs: empty file, comment-only file, literal/comment at EOF, tabs, CRLF line endings, BOM
✅ (comment-only, tabs, CRLF, BOM-as-E0101 all pinned)
LEX-8
Huge literals (e.g. 10^100): lexed as exact ints; downstream width-inference behavior pinned (see AMB-11)
✅ (decimal/hex 10**100 exact-int)
LEX-9
Character-set policy: ASCII-only [A-Za-z_]/[0-9] pinned (AMB-14) — é/٣/²/BOM all fall through to E0101; the ²→int() raw ValueError crash is closed
✅ (lexer pinned ASCII; crash regression-tested)
LEX-10
Source decoding: a .shdl file with invalid UTF-8 bytes → structured diagnostic at the read boundary, never a raw UnicodeDecodeError (loader decodes in a try → positioned E0101)
✅ (flattener loader side; shdlc-CLI mirror is FUZ-4's open xfail)
LEX-11
Doc-comment capture edge rules: only the first leading """…""" becomes meta.doc; preceding #/"…" comments do not disqualify capture; a second leading docstring is ignored
Positive coverage of every EBNF production in shdl.md §13 — components (with/without top, params, empty port lists), instances (positional/named/mixed args), constants, init blocks, connect, generators, conditionals, all Signal/IndexExpr/NameTemplate forms
✅ (empty-output -> (), declaration-context when, parenthesized ( BoolExpr ), and all RelOps != < <= >= + || now positively parsed)
PAR-2
Slice forms [a:b], [a:], [:b], single [k], and [{expr}] index
Nested replication (Replication contains ConcatItem which may be Replication, e.g. 2{2{s}}) — grammar permits it; behavior pinned
✅
PAR-5
NameTemplate interleaving: cell{i}_{j}, mem{row*4+col}, substitution followed by literal ident
✅
PAR-6
E0201 per raise site (parser.py) — each triggered by a dedicated minimal program
✅ (all 12 parser raise sites individually triggered via the DIA-2 site matrix)
PAR-7
Context legality — corrected: declarations inside connect are rejected via E0201 (they parse as connections and die at the -> expect), not E0604; the connection-context E0604 site fires only for non-IDENT/non-LBRACE tokens (e.g. 5 -> Y;)
✅ (both directions pinned + the conn-context E0604 site triggered)
PAR-8
Deeply nested input (1000-deep braces/parens): structured diagnostic or documented cap — never a raw RecursionError (live-verified crash at 400-deep nesting)
✅ (MAX_NESTING_DEPTH=200 cap → E0201; 201-deep probe pinned, crash closed)
PAR-9
</> contextual disambiguation: param list vs generator intro vs relational inside when — adversarial mixes (a<b: T<N> style)
✅ (three-role angle-bracket mix pinned)
PAR-10
Premature EOF inside component/connect/generator/init bodies: pinned code + position — never a crash or hang
✅ (all four body kinds pinned)
PAR-11
Body-order laxity: declarations/init/connect accepted in any order (§13's EBNF fixes the order, §4.2's prose allows interleaving — AMB-16); pinned
✅
PAR-12
Reserved keyword in identifier position (a port/instance/constant/component named when, connect, …) → E0201 with position
✅ (zero + negative port widths; both constant-width sites; AMB-31 E0403-vs-E0906 branch pinned)
VAL-8
Reserved-name checks at the remaining declare sites: generator variable (>__i[2] → E0303, >i_1_[…] → E0304) and constant name (__K = 1 → E0303)
✅
VAL-9
Expansion-time name checks on generated names: template duplicate (>i[1:2, 1:2]{ b{i}: OR; } → E0301), generated name colliding with a port (E0301), generated name matching a reserved pattern (x_{i}_ → E0304) — the expand-phase declare sites, distinct from validate-phase checks on plain names
Parameter scope: param referenced outside its component → E0603/E0307; generator var shadowing a param (pinned: shadowing wins); generator range expressions evaluate in the enclosing scope (AMB-22)
✅ (shadowing-wins, out-of-scope param ref → E0603, range-scope-under-shadowing all pinned)
MON-7
Specialization scale: e.g. 100 distinct Adder<k> instantiations — output correct, no superlinear blowup (ties into SCL)
✅ (100 distinct Rep<k> specs; also SCL-4)
MON-8
Binding canonicalization across named-arg order: P<N = 2, M = 1> ≡ P<M = 1, N = 2> dedup to one specialization (the declaration-order normalization exists precisely for this; its purpose is unasserted)
✅
Domain E — Generators, conditionals & compile-time expressions (GEN)
ID
Obligation
Status
GEN-1
Range forms: [N], [a:b], [a:], [:b], compound [a:b, c, d:e]
✅ ([:b] RangeTo now exercised end-to-end through parser + expansion)
GEN-2
Open-range resolution from governing signal; ambiguity → E0602; declaration-context open range → E0602
when/else: structural selection, boundary-folding idiom (i == 1 / i > 1 carry chain)
✅ (the dual-wheni > 1 §7.7.1 carry chain now elaborated to a real ripple)
GEN-8
Conditional operator matrix: each of == != < <= > >= and &&, ||, parenthesized BoolExpr — each proven to select/deselect structure
✅ (every RelOp + BoolAnd/BoolOr + parenthesized BoolExpr proven to select structure in an elaborated when)
GEN-9
Expression semantics pinned: precedence, integer division truncation direction (C-style toward zero, incl. negative operands), division by zero → E0605, unbound ident → E0603
✅
GEN-10
Compound-range duplicate index ([1:4, 2:6]) → behavior decided & pinned (expected: duplicate instance names → E0301) — see AMB-4
✅ (verbatim iteration; overlap collides → E0301)
GEN-11
Open range with expression bound (>i[N/2:]) — see AMB-5
✅
GEN-12
Declaration-context when/else (spec §7.7.2): conditional instance/constant creation gated on a parameter (when {WITH_CARRY == 1} { c: Carry; }) — elaboration and deselected-branch absence pinned (every when in the entire corpus lives inside connect)
✅ (parameter-gated instance + conditional constant both pinned)
GEN-13
Range value domain: lower bound 0 accepted today ([0:b] iterates from 0), negative → E0601 — accept/reject boundary pinned (see AMB-19)
✅
GEN-14
Open-range governing-signal scan semantics: several same-width signals dedup to one bound; no-signal-in-body E0602 site; both when branches scanned pre-evaluation; inner-loop-var shadowing; silent skip of unevaluable templates — each pinned (see AMB-20/AMB-21)
✅
Domain F — Expanders: slices, concat, replication (EXP)
Width mismatch E0401; index out of range E0402; ill-ordered/zero-based slice E0404
✅
EXP-5
Degenerate slice [k:k] (one bit) accepted
✅
EXP-6
Replication count 0 or negative — implemented as E0601 (count must be >= 1); spec amendment + pinning test outstanding (see AMB-6)
✅
EXP-7
Role enforcement (E0505, all 6 raise sites): input as destination, output as source, instance-port directions, constant as destination, replication as destination
✅
EXP-8
Multiple drivers E0501, floating input E0502, floating output E0503 — messages name the offending signal
✅ (expander-path E0501 message names the wire; flatten-path E0501 proven-unreachable from per-component-valid input)
EXP-9
Self-connection E0504 — policy (flag-gated?) decided and both modes tested
✅ (role check fires first → E0505; E0504 structurally shadowed, pinned as the observable contract)
EXP-10
Concat on both sides of one connection ({a,b} -> {x,y})
✅
EXP-11
Multi-item replication group N{a, b} lowering: N copies of the MSB-first group — exact per-bit connection order pinned (parse-only today; every flattened replication in the suite is single-item)
✅
EXP-12
Open-ended slice [a:] in a connection: upper bound resolved from the signal's width at resolve time
✅ (hi=None resolution branch pinned end-to-end)
EXP-13
Slice and bit-index on instance ports (ir.Q[1:8], sel.O[1], spec §5.1): pairing pinned with a targeted test; E0402/E0404 on an instance port asserted
✅ (dedicated pairing assert + E0402/E0404 on an instance port)
Referenced-bits-only materialization to __VCC__/__GND__; unreferenced constants produce nothing
✅
CON-2
Spec §8.1 truth table: unbounded-width semantics — referencing far beyond significant bits yields __GND__ (e.g. Hundred[64])
✅ (§8.1 table pinned verbatim)
CON-3
Declared width = overflow assertion only (E0801); width inference for bare constants
✅
CON-4
ZERO = 0 edge: inferred width of value 0 — decided & pinned (see AMB-12)
✅ (direct unit assert of the width-1 inference + spec amended — AMB-12)
CON-5
Constants are sources only (E0505); per-bit indexing in generators
✅
CON-6
Name collision with materialized X_bitN gates → E0308; hierarchy-prefixed constant metadata
✅
CON-7
Parameter-derived constant widths (K[N] = v): re-checked post-monomorphization — E0403/E0801 at the expand-phase sites (validate pre-checks literal widths only; both expand sites are dead in the suite; grammar question: AMB-17)
Deep prefixing (3+ levels), inline-at-declaration ordering, canonical wires for hierarchy ports
✅
FLT-2
Pass-through/wire-through alias chains resolve fully; pure alias cycle → E0506
✅
FLT-3
Generated-name collision (fa_x1 vs hierarchical fa containing x1) → E0308
✅
FLT-4
Hierarchy depth ≥10 — explicit deep-nest fixture (the CPU does not hit this: measured max nesting is 6 — SR16 > RegFile > RegE > MSFFE > DLatch > SRLatch; deepest dedicated fixture is 3)
✅ (dedicated 10-level chain)
FLT-5
Init: canonical-key extraction, propagation through hierarchy, multi-bit LSB-first spread
Init on a combinational (non-state-holding) wire: allowed, then overwritten by first cycle — verified end-to-end in simulation (spec §11.4)
✅ (named end-to-end case: seed visible at cycle 0, overwritten on first tick)
FLT-8
Whole-loop seeding lesson (tasks/lessons): init values that don't form a fixed point of the seeded feedback loop — document & test expected (possibly oscillating) behavior deterministically
E0308 second flatten site: flattened gate name colliding with a top-level port wire (FLT-3 covers gate-vs-gate only; the gate-vs-port site is unexecuted by any test)
✅
FLT-10
Indexed/sliced init targets (init { Q[3] = 1; }, init { Q[4:2] = 5; }): grammar and primary_bits support them — per-bit seeding semantics plus E0402/E0404 on bad init indexes pinned
✅
FLT-11
Init targets resolve with an empty environment: a {…} template in an init target → E0603 by construction — pinned
use mod::{A, B} resolution; search order (file's directory shadows -I dirs; spec wording divergence: AMB-24)
✅
IMP-2
E07xx: missing module (E0701), circular import with cycle chain in message (E0702), missing name (E0703)
✅
IMP-3
Imported/local name collision → E0301
✅
IMP-4
Diamond imports (A→B→D, A→C→D): legal, D loaded once, not flagged circular
✅ (minimal A→B→D fixture asserts D loaded once + a diamond conformance case — CNF-4)
IMP-5
Self-import; importing a primitive name (impossible per implementation — contradicts spec §9.2, see AMB-25); use after a component definition (implemented as E0201, untested)
Module name = filename semantics; main file missing → E0701
✅
IMP-7
No transitive re-export: use b::{X} where b merely imports X → E0703 (the visibility-origin check; see AMB-26)
✅
IMP-8
Import-import collisions: use a::{X}; use b::{X}; → E0301; duplicate name within one list use lib::{A, A} → E0301 (the collision site covers all three shapes; only local-vs-import is tested)
✅ (cross-module + within-list shapes)
IMP-9
-I precedence among multiple include dirs: earlier dir wins (ordered search) — asserted the way IMP-1 asserts file-dir shadowing
Module-name case vs case-insensitive filesystems: use Add2 resolving add2.shdl on APFS but not Linux; two spellings loading one file as two modules — platform-independent behavior pinned (see AMB-28)
✅ (case mismatch → E0701 platform-independently; exact case still loads)
Cross-consistency invariants (every name in meta exists in the structural core) — today internal asserts in metadata.py; promote to a public validator with structured errors + direct tests
monitors block: emitted (even if empty), consumed by future SHDB — schema pinned now (the flattener hardcodes {} and no population path exists — see AMB-30)
✅ (always-present {} across all fixtures — AMB-30)
MET-10
source_map column exactness: at least one gate and one instantiation site asserted against a hand-counted column (lines are pinned exactly today; columns only >= 1 — a column-attribution regression would pass the whole suite)
✅ (hand-counted columns for direct gates + an instantiation site)
MET-11
No absolute paths in emitted bytes: doc.source and source_map keys are basenames — asserted directly (checkout-location independence)
✅ (direct basename assert + the absolute load dir never appears in bytes)
Domain K — Emission, serialization & determinism (DET)
Byte-identical output across runs; with explicit --top; SOURCE_DATE_EPOCH pinning
✅
DET-3
Flattener byte-determinism across fresh processes with different PYTHONHASHSEED (compiler side has this; flattener side runs in-process only)
✅ (python -m flattener over distinct hash seeds, byte-compared)
DET-4
Idempotence property: re-flattening a flattened file yields byte-identical structure (modulo timestamp) — AMB-29 landed a trailing-meta-block production, so emitted Base SHDL re-flattens
🟡 (structural-core idempotence pinned on plain-identifier fixtures; bus-port fixtures emit A_1_ which re-flattening rightly rejects via E0304, so they cannot fully round-trip by design — init/meta intentionally outside the structural core)
DET-5
Generated C byte-identical across runs and hash seeds
✅
DET-6
Non-ASCII metadata emission: doc text emitted as raw UTF-8 (ensure_ascii=False), round-trips emit → parse_base, and the bare-stdout path never raises UnicodeEncodeError under a non-UTF-8 locale (-o writes UTF-8 explicitly; stdout writes UTF-8 via sys.stdout.buffer)
✅
DET-7
Cross-stage acceptance: every fixture's emitted Base SHDL parses via shdlc parse_base and validates via build_circuit
✅ (all 16 fixtures incl. stdgates components cross both parse_base and build_circuit)
Under feedback: max_depth = feedback-free shell only; settle() must be refused — enforced at the oracle (BaseEval) level and, since 2026-06-12, at the driver level (PySHDL settle() raises SettleRefusedError under has_feedback — V.2, test_pyshdl_settle.py)
✅
TIM-4
Critical path is a real connected path ending at an output (structural property test)
✅
TIM-5
Settle sufficiency property: for every combinational fixture, poke → step(max_depth) → outputs equal BaseEval fixpoint; step(max_depth−1) may differ (proves bound is tight on at least one input)
✅ (tightness witnessed on add2's carry path)
TIM-6
Feedback-circuit timing content: per-output output_depths for SCC-driven outputs; critical_path that starts at a feedback gate or power pin rather than an input — exact values pinned on minimal fixtures (srlatch Q/Qn, ring)
✅ (srlatch path ['n1_n1','Q'] starts at the feedback NOT; ring path pinned)
TIM-7
Degenerate timing blocks: zero-output top → max_depth 0, empty output_depths, empty critical_path; output wired directly from a power pin (ONE[1] -> Y) → depth 1, path [pin_gate, Y] (both live-verified to flatten with exactly these values; nothing pins them)
Every ErrorCode has ≥1 minimal trigger, with valid position (line ≥1, col ≥1) — enforced by completeness assertion
✅ (41/41)
DIA-2
Per-raise-site coverage: 107 raise err( sites across the pipeline; each site triggered by a dedicated case (a code reached via one path can silently break on another)
✅ (mechanical inventory re-derives all 107 sites each run; test_sites_complete enforces registry==inventory, every trigger proves it reaches the exact file:line)
✅ (the complete five-field line pinned exactly + field-by-field partition)
DIA-4
Policy decision — multi-error collection: pipeline currently stops at first error. Legacy suite collected several errors per pass. Decide: implement collection (then test multi-error files, counts, ordering) or pin fail-fast as the contract.
✅ (pinned fail-fast in shdl.md §14.1)
DIA-5
Policy decision — warnings (legacy W01xx: unused input port, unused constant, unconnected instance output). No warning machinery exists. Decide scope; if adopted, extend the completeness matrix to W-codes.
✅ (pinned out of scope for V1 — no W-codes, shdl.md §14.1)
DIA-6
Policy decision — "did you mean" suggestions (legacy had similar-name hints for E03xx). None exist. Decide; if adopted, test suggestion quality and absence of false suggestions.
✅ (pinned out of scope for V1 — no suggestions, shdl.md §14.1)
DIA-7
Message quality assertions: offending name/value appears in message (spot-tested today for six codes: E0501/E0502/E0503/E0702/E0703/E0801) — extend to all codes
✅ (33 codes mapped to verbatim name/value substrings + 6 name-free structural codes; the two sets partition the full enum — test_dia7_partition_is_exhaustive)
DIA-8
Position accuracy: each diagnostic's line:col equals the offending token's actual coordinates, asserted per trigger (today only validity line≥1/col≥1 is checked; a raise site could drift to a wrong-but-valid position undetected)
✅ (the DIA-2 matrix asserts exact line:col per site; mutation-checked to catch a 1-column drift)
DIA-9
CLI usage-error contract: argparse failures (missing FILE, unknown flag) exit 2 with usage on stderr — distinct from the documented exit-1 diagnostic path; python -m flattener entry point executed by a test
Truth tables for all six primitives, compiled and oracle, all input rows
✅
SIM-2
Cycle-0 all-zeros; __VCC__ reads 0 at cycle 0 and 1 from cycle 1 (anti-preload pin)
✅
SIM-3
Unit delay observable: NOT-chains, adder8 carry ripple per-cycle trace (Cout flips exactly at cycle 16), no early visibility
✅
SIM-4
Fixpoint stability: extra steps after max_depth change nothing (combinational)
✅
SIM-5
Feedback: SR latch scripted sequence incl. forbidden-state transient (Q==Qn==1 observable — fidelity, not a bug); ring oscillator with exact period N
✅
SIM-6
Compute-commit order independence: permute instance/connection declaration order of a netlist → identical traces (direct property test; today only implied)
✅ (direct property test at the oracle level + scrambled-feedback lockstep lib-vs-oracle)
SIM-7
Reset semantics: idempotent, clears inputs+state+dirty, re-applies init seeds, constants take effect on first evaluation after reset (shdlc_goals' 'all-zero' wording contradicts the implemented & tested seed re-application — AMB-39)
✅
SIM-8
Init-at-load: fresh library has seeds applied without a tick
✅
SIM-9
Exhaustive small-circuit grids (add2: all input combos × cycles 0..6)
✅
SIM-10
2-state guarantee: no value other than 0/1 ever observable per single-bit wire (guaranteed by the poke per-bit &1u scatter plus Boolean closure of the gate ops — not by the uint8 casts; assert in debug-build tests later)
✅ (single-bit wires asserted always two-state at the port boundary; full-gate-state closure staged for the debug build under V.1)
SIM-11
Input persistence (§11.1): poked component inputs hold their values across cycles until changed — direct assertion (poke once, step N, input peek unchanged, dependent outputs consistent at intermediate cycles)
✅ (named contract: held inputs keep outputs pinned across cycles; persistence ends only on an explicit re-poke)
The release library exports six functions: reset, poke, peek, step, plus the
later-landed step_settle and run_batch (ABI-11/ABI-12; shdlc_goals still documents four —
AMB-38).
ID
Obligation
Status
ABI-1
poke: user-facing names, LSB packing, masking to port width (2/8/64-bit), arms dirty flag
✅
ABI-2
peek: lazy exactly-one-tick on dirty output read; input peek never ticks nor clears dirty
✅
ABI-3
step(0) no-op preserving dirty; step(n) advances exactly n
✅
ABI-4
step with negative argument: pinned as no-op
✅ (step(1) discriminator distinguishes a true no-op from one-tick-plus-dirty-clear)
ABI-5
Unknown signal poke/peek: stderr message, no-op / returns 0, does not arm or consume dirty
✅
ABI-6
Signal-name case sensitivity pinned (see AMB-1)
✅
ABI-7
peek return zero-extension above port width pinned (see AMB-13)
✅ (dedicated contract test + spec amended — AMB-13)
ABI-8
Ports wider than 64 bits: uint64_t cannot carry them — shdlc must reject at compile time with a structured error; pinned by test
✅ (end-to-end .shdl >64-bit port: flattens fine, shdlc rejects with a structured error)
ABI-9
Multiple libraries in one process: distinct circuits, and two copies of the same circuit (dlopen cache-busting, symbol isolation via -fvisibility=hidden)
✅
ABI-10
Zero-input, zero-output, zero-gate circuits load and obey the ABI
✅
ABI-11
step_settle(n): observably ≡ step(n) with fixed-point early exit; returns ticks actually run (1 at an existing fixed point); n ≤ 0 no-op preserving dirty; oscillators never early-exit and run the full budget
✅
ABI-12
run_batch(in, out, count, cycles, settle): per-frame scatter/advance/gather ≡ the same poke/step/peek sequence (both settle modes, mid-settle budgets); cycles ≤ 0 takes the lazy-peek path; count 0 no-op; zero-input-port frames legal
✅ (zero-output-port through run_batch + dirty-stays-set when nop==0 ∧ cycles≤0 now pinned)
ABI-13
Export-set hygiene: the visible symbol set is exactly the six ABI functions — nothing else (no get_cycle in release, no leaked statics)
🟡 (asserted via nm on macOS; source-level SHDLC_API/static scan exists; the Linux ELF export-set variant remains macOS-gated, deferred to a Linux CI pass — ties CCT-6)
ABI-14
poke on an output port name resolves to the unknown-signal path (stderr names it, complete no-op, dirty untouched) — tested with a real output name; decide whether it deserves a distinct diagnostic
✅
ABI-15
Empty-string signal name takes the unknown-signal path even on zero-port circuits (the dummy { "", 0, 0 } table entries must never match — only the NUM_*_PORTS loop bounds protect them)
✅
ABI-16
NULL signal name to poke/peek: currently undefined behavior (unguarded strcmp) — decide guard-vs-precondition and pin (see AMB-32)
✅ (generated C guards NULL → unknown-signal path, never UB; ctypes-tested — AMB-32)
ABI-17
Double poke of the same port within one dirty batch (poke A=x; poke A=y; peek): last value wins, still exactly one lazy tick (re-poke is tested only across peek batches; the fuzzer samples distinct ports, so it never hits this)
✅
ABI-18
Load-time constructor is __GNUC__-gated: on non-GNUC builds no constructor runs, so init-at-load (SIM-8) does not hold and an explicit reset() before first use is the contract — pin when the Windows toolchain lands (ties CCT-6)
⚪
ABI-19
Fully-empty circuit (0 inputs, 0 outputs, 0 gates) loads and obeys the ABI (ABI-10 tests each degenerate axis separately, never all at once)
CC discovery (CC env, PATH, precedence), per-platform flags/suffix
✅
CCT-3
Zero-warning generation under STRICT_CFLAGS for every test build, including >1024-gate chunked tick
✅ (CLI builds via --cc "cc -Wall -Wextra -Werror -pedantic" — a strict build exiting 0 IS the proof, incl. the chunked tick)
CCT-4
-O0 ≡ -O3 trace equality
✅
CCT-5
Sanitizer builds: run the differential suite against -fsanitize=address,undefined builds of generated C (UB in generated code is otherwise invisible)
✅ (generated C + a driver main() built into a standalone ASAN+UBSAN executable, run as a subprocess and checked vs a BaseEval trace; self-gates on a probe)
CCT-6
Platform matrix: today macOS/clang only. CI must add Linux/gcc + Linux/clang; Windows/MSVC best-effort later (shdlc_goals §8)
🟡 (ci.yml matrix {ubuntu/gcc, ubuntu/clang, macos/clang} + nightly.yml authored and YAML-validated, $CC honoring verified; the Linux/gcc + Linux/clang generated-C builds are UNPROVEN — need one real CI pass; Windows/MSVC still later)
CCT-7
Frontend robustness: malformed Base SHDL / metadata into shdlc → structured errors (model invariants, ~40 negative cases)
✅ (malformed meta JSON now wrapped in BaseParseError — the raw json.JSONDecodeError crash closed; all 7 BaseParseError sites triggered — CCT-9)
CCT-8
Model validation completeness: every ModelError path exercised (mirror of DIA-2 for the compiler side)
Base-reader diagnostics per raise site (7 BaseParseError sites: scanner EOF, expect mismatch, non-identifier, unknown primitive, duplicate instance, one-component-per-file/trailing token, trailing content after meta) — each via a minimal artifact asserting the message; malformed meta JSON wrapped in BaseParseError, never a raw JSONDecodeError
✅
CCT-10
shdlc CLI contract: exit 0/1/2; default artifact naming (input stem + platform suffix, in CWD); --emit-c alongside build; --no-build with its default.c path; --base/--shdl overrides; --base+--shdl exclusion pinned at exit 2; --top/-I rejection for Base inputs; flattener-SHDLError surfacing branch; --cc plumb-through
✅ (--shdl flag, --no-build default .c path, SHDLError-surfacing branch, exclusion pinned at exit 2 exactly, --cc at CLI level all closed)
CCT-11
build_library temp hygiene: the mkstemp'd .c is unlinked on success and on CCError; with --emit-c the C file persists; no stray temp files after a failed build
✅
CCT-12
find_cc whitespace-only/empty value (explicit arg or $CC that shlex-splits to nothing) → CCError, no fallback
✅
CCT-13
Minimal-consumer guarantee end-to-end (base_shdl §2): a Base SHDL file with no meta section compiles to a working library; identity single-bit ports synthesized from the header; sim parity vs oracle
✅ (a meta-less artifact built and run with synthesized identity ports, sim parity vs oracle)
CCT-14
C-compile failure surfacing: CCError carries the exact argv and the compiler's stderr verbatim; str() names the exit code; CLI prints a single clean diagnostic, rc 1
✅
CCT-15
in_wires_* initializer wrapping past the 80-col limit: 8 names per line, comma discipline, closing brace — structurally pinned
✅ (the wrapped text format structurally asserted: 8 names/line with comma discipline)
CCT-16
Hot-path purity of generated C (shdlc_goals §3.2/§5.3): step() free of strcmp/fprintf/malloc/branches; tick() additionally loop-free; strcmp confined to the poke/peek scans
✅
CCT-17
The n-only tick_chunk_k signature variant (chunk with no cur[] reads) actually compiles under STRICT_CFLAGS and lockstep-matches BaseEval
✅ (a circuit whose chunks read no gate outputs emits and builds the n-only signature, lockstep-matches BaseEval)
CCT-18
Base-level naming-reservation asymmetry: shdlc accepts __x / Sum_2_ gate names unchecked while fully re-validating §3.6 connection rules — pin the trust as the contract with an acceptance test, or add rejection (see AMB-36)
✅ (acceptance test pins the trust; §3.6 wiring rules still re-validated — AMB-36)
CCT-19
Self-containedness (shdlc_goals §8): the built library's undefined-symbol set is a subset of libc — no other runtime dependencies (nm -u / platform equivalent)
✅ (nm -u subset-of-libc; macOS-gated, ties CCT-6 for the Linux equivalent)
Fixture differential: 10 fixtures + 10 handwritten minimal netlists, 150 cycles random poke/step/reset, all ports compared every cycle
✅
FUZ-2
Netlist fuzzer: random valid Base SHDL (5–80 gates, optional feedback), self-checked against BaseEval, then lib-vs-oracle lockstep; env-scalable
✅
FUZ-3
SHDL-source fuzzer: generate random high-level programs (params, generators, conditionals, slices, concat, constants, init, hierarchy) → flatten → HighEval vs BaseEval vs C. The flattener is the most complex component and currently has no randomized adversary.
✅ (valid-by-construction generator + flatten → HighEval/BaseEval lockstep, env-gated compiled-C tier; campaigns to 1000/1000 found no flattener/oracle divergence)
FUZ-4
No-crash fuzzing of the frontend: mutated/truncated/garbage .shdl text → always SHDLError-or-success, never a raw traceback (targets the 22 asserts, 7 raw exceptions, 25 raise AssertionError guards, and the implicit decode/JSON/env crash paths — ROB-5/ROB-6)
✅ (SHDLC_NOCRASH=2000 + 66k out-of-band inputs, 0 breaches; the shdlc-CLI invalid-UTF-8 path now diagnosed via BaseParseError)
FUZ-5
Action-sequence adversary: randomized interleavings emphasizing reset-after-poke, peek storms, step(0) runs (the dirty-flag state machine — mutation-killing cases exist; generalize)
✅ (full-ABI adversary modeling the C per-frame dirty state machine in lockstep + a double-poke mutation killer; verified across 1000 seed-sequences)
FUZ-6
Soak tier: nightly large-N campaign with frozen failure artifacts
✅ (nightly.yml soak job — cron + all campaign knobs cranked across ubuntu+macos; CI execution unproven, ties CCT-6)
FUZ-7
(Optional, post-V1) Mutation testing over flattener+shdlc to measure suite strength
❌
FUZ-8
DualSim observability boundary: port-only comparison is blind to internal divergences that cancel at the ports for the driven stimulus — pin the limitation in the harness docstring now; close via V.1 full-gate-state lockstep (peek_gate at every compared cycle)
✅ (limitation pinned in the DualSim docstring; full closure staged under V.1)
Every future component (PySHDL, debug build, backends, optimization tiers) consumes the corpus as its acceptance gate — wiring obligation, restated per component in Domain V
🟡 (PySHDL wired 2026-06-12: the full corpus replays through the public Circuit API — from_base build once per case, from_library per trace, strict=False — bit-exact via conformance.runner.executor, tests/pyshdl/test_pyshdl_conformance.py; the debug build / backends / optimization tiers remain ⚪ until built — Domain V)
CNF-6
Integrity-checker self-test: a corrupted-corpus matrix (missing/stray artifact, de-listed case, unsorted lists, wrong _format, ops[0] not reset, bad op keys, out-of-range values, unknown feature, empty provenance, unknown-signal trace via check_trace_signals) — each → ConformanceError naming the artifact (today only the healthy corpus is proven to pass; a silently broken checker keeps passing)
✅ (full corrupted-corpus matrix over a sandboxed copy)
CNF-7
Regen tooling contract: dry run writes nothing and prints the full diff; --write applies exactly the shown diff and touches only golden bytes/expect values (stimulus, metadata, descriptions frozen); unknown case → error listing names — pinned over a sandboxed corpus copy (gen.py is the only sanctioned golden writer and is completely untested)
Drift enforcement: a changed golden byte without a major suite_version bump + changelog entry fails mechanically (per-golden content hashes in MANIFEST.json or a CI diff against the last release) — closes the coordinated-regen loophole that live checks cannot see
✅ (per-golden sha256 golden_hashes map in MANIFEST.json, bijective with the on-disk golden set; refreshed only on the sanctioned regen --write)
10⁵-gate synthetic: flatten + compile + 100-cycle differential smoke (known clang misched risk on giant tick — see perf memory; this is the regression guard)
Documented limits: max wire index (65535) and max port width (64) — both already have cap and cap+1 boundary tests; holes: the limits appear only in code comments, not in base_shdl.md/shdlc_goals.md; a max-gate-count limit is neither defined nor tested
✅ (limits documented in shdl.md §14.2, base_shdl.md §6, shdlc_goals.md §3.2; max-gate-count decided as deliberately uncapped)
SCL-7
Pathological single ranges ([1:10⁹], huge replication counts via params): documented instance-count cap with a structured diagnostic — never an unbounded list materialization / OOM hang (range_values materializes Python lists unguarded at four sites; mirror of the compiler-side wire cap)
✅ (the four range_values sites AND the RRepl replication-count site are guarded by MAX_RANGE_VALUES=1_000_000 → E0601; tested at cap, [1:10⁹], param-driven, open-range, and literal-count replication {10⁹{Sign}})
Domain T — Robustness: the no-crash guarantee (ROB)
The re-derived inventory: 7 raw builtin-exception raise sites (KeyError in loader.py;
ValueErrors in high_eval.py, codegen.py, and base_eval.py ×4 — count and locations verified),
22 bare assert statements (9 of them verify_meta's — MET-7/ROB-3), 25 raise AssertionError invariant guards (a third class the original inventory missed — ROB-5), and
four implicit raw-exception paths reachable from user input, each reproduced as a live
crash: invalid UTF-8 through both CLIs, malformed meta JSON through shdlc, garbage
SOURCE_DATE_EPOCH through the flattener (ROB-6) — plus the lexer's ² → int() ValueError
(LEX-9). Policy:
ID
Obligation
Status
ROB-1
Each raw-exception path: either (a) prove unreachable from user input and convert to an internal-invariant assert with a comment, or (b) convert to a structured diagnostic — then test it. Notably: codegen.py unknown gate type, loader.py cache KeyError.
Oracle API errors are intentional (BaseEval.poke overflow raises ValueError — it's a test harness, stricter than the C ABI's masking). Pin this asymmetry explicitly in a test + docstring so it's never "fixed" into agreement by accident.
✅ (pytest.raises pins on both BaseEval and HighEval poke overflow + the stricter-than-ABI intent in both docstrings)
ROB-3
metadata.py asserts → public validator (MET-7)
✅ (validate_meta + MetaValidationError)
ROB-4
FUZ-4 (frontend no-crash fuzzing) is the enforcement mechanism for this domain
✅ (see FUZ-4)
ROB-5
The 25 raise AssertionError invariant guards (monomorphize 7, expander 6, expr 4, expand 4, flatten 3, high_eval 1): classify each unreachable-from-user-input (comment) or convert to a structured diagnostic, per the ROB-1 policy; FUZ-4 targets these too
✅ (each match-exhaustiveness guard carries a # pragma: no cover + unreachable-by-construction justification; FUZ-4 campaigns hit none)
ROB-6
Implicit raw-exception paths (all reproduced): invalid-UTF-8 source → UnicodeDecodeError escapes both CLIs; non-JSON meta block → json.JSONDecodeError escapes shdlc (not a BaseParseError); malformed SOURCE_DATE_EPOCH → ValueError/OverflowError escapes the flattener CLI — catch-or-convert at each boundary, then test (LEX-10, CCT-9, DET-2's env var)
✅ (flattener-side UTF-8 → positioned E0101, meta JSON → BaseParseError, SOURCE_DATE_EPOCH → structured E0001, shdlc-CLI invalid UTF-8 → BaseParseError naming the byte offset — all closed and tested)
Domain U — Spec ambiguities: decide, amend, pin (AMB)
Each item needs: a decision, a spec amendment, a unit test, and (where observable) a conformance
case. AMB-1..12 came from the original spec-extraction pass; AMB-13..41 from the 2026-06 full
audit.
Resolution state (2026-06-12): all 41 AMBs are decided, spec-amended, and pinned. WP-C
applied every Domain-U amendment to shdl.md / base_shdl.md / shdlc_goals.md as native
prose (no AMB-NN literals in the docs); the behavior is implemented in the flattener/shdlc and
exercised by a named unit test (the cross-references in the resolution column point at the owning
obligation row). No new ErrorCode was minted: every resolution reuses an existing code —
AMB-27 (a re-used module name resolving to a different file) lands as E0701 in the loader
(test_imp*_… / the AMB-27 loader test), not the speculative new E07xx the original proposal
floated. Observable cases carry conformance coverage (CNF-4: diamond for AMB-27-adjacent import
identity, init_comb for AMB-3/AMB-39 power-on, abi_poke_masking for AMB-2, cond_matrix for
the operator matrix). The table below is the decision register; the Resolution column states
what was pinned.
ID
Ambiguity
Resolution (decided · amended · pinned)
AMB-1
poke/peek signal-name case sensitivity
case-sensitive (matches language)
AMB-2
poke value larger than width
masked modulo 2^width (already implemented & tested — amend spec to say so)
allowed; governing-signal rule applies after evaluation
AMB-6
Replication count 0
already implemented: E0601 'count must be ≥ 1' covers 0 and negative — amend spec + pin (EXP-6)
AMB-7
init value overflow on multi-bit port
error E0A03 (implemented — amend spec)
AMB-8
Does step(0) / lazy tick increment get_cycle?
step(0): no; lazy peek tick: yes by 1 (pin when debug build lands)
AMB-9
peek_gate on power pins
observable like any gate (pin when debug build lands)
AMB-10
get_gate_info enumeration order stability
stable = state-layout order, invariant across reset (pin when debug build lands)
AMB-11
Huge literals (≫64 bits) in constants
legal in flattener (unbounded ints); >64-bit port connection rejected (ABI-8)
AMB-12
ZERO = 0 inferred width
width 1 (a single GND bit) — implemented & byte-frozen in the corpus; amend spec + direct unit pin (CON-4)
AMB-13
peek return bits above port width
always zero-extended to uint64 (bits ≥ width are 0, on every read, incl. after over-wide poke and after reset) — symmetric with AMB-2; dedicated test + amend shdlc_goals §3.1 (ABI-7)
AMB-14
Identifier/digit character set: Unicode-wide today (é → IDENT, ٣ → NUMBER, ² → raw ValueError crash); spec's LETTER/DIGIT undefined
pin ASCII-only [A-Za-z]/[0-9]; any other non-whitespace, non-comment char → E0101 — fixes the ² crash class and makes LEX-7 implementable (LEX-9)
AMB-15
Source encoding: undecodable UTF-8 dies at the read boundary (loader, byte offset only) before any lexing; decodable non-ASCII reaches the lexer
pin UTF-8 source; undecodable input → positioned diagnostic raised at the read boundary, mirrored in shdlc for Base inputs (LEX-10, ROB-6)
AMB-16
Component-body block order: §13's EBNF fixes decl→init→connect, §4.2's prose allows interleaving, the parser accepts any order
pin any-order; the count rules (E0309/E0310) remain the only structural constraints; amend the §13 note (PAR-11)
§13 wins; amend §8; param-dependent constant widths are overflow-checked per instantiation (CON-7)
AMB-18
N{x} replication-vs-template tie-break: an IDENT count over a brace group holding a single arithmetic expression parses as a template, contra §13's note
pin the parser's rule in the spec: replication requires a literal count or signal-only group syntax; parse tests both ways
AMB-19
Generator range value domain: 0 accepted, negative → E0601; §7.1's table silent; E0601's enum text ('empty or ill-ordered') doesn't match its 'is negative' sites
pin bounds ≥ 0 legal (0 iterates/emits index 0), negative → E0601; widen E0601's description; accept- and reject-side tests (GEN-13)
AMB-20
Open-range governing signal: §7.1 says 'exactly one multi-bit signal' but the implementation collects a width set — several same-width signals are legal (GEN-2's own test relies on this)
amend spec to the implemented rule: all loop-var-indexed signals must agree on one width; differing widths → E0602 (GEN-14)
AMB-21
Governing-signal scan vs conditional branches: both when/else bodies are scanned before any condition is evaluated, so a never-emitted branch can ambiguate resolution
pin the conservative implemented behavior; amend §7.1; test an else-branch width forcing E0602 (GEN-14)
AMB-22
Generator range scope under shadowing: >N[N]'s range evaluates in the enclosing scope (shadowed param visible), body sees the loop var
pin current behavior; amend §7; unit test >N[N] with param default (MON-6)
AMB-23
Diagnostic precedence when a user component shadows a dunder primitive (component __VCC__ violates both E0305 and E0303)
pin E0305-wins (the more specific code); assert in VAL-2's completion tests
AMB-24
Import search order: §9.1 says 'current directory first'; the loader (deliberately, per its docstring) searches the importing file's directory first, and IMP-1's test pins that
amend §9.1 to 'the importing file's directory, then -I dirs in order' (relocatable, deterministic; already tested)
AMB-25
§9.2 claims importing primitives from stdgates is 'harmless but unnecessary' — impossible: stdgates cannot define primitive names (E0305) and importing an undefined name is E0703
amend §9.2: primitive names are built in, cannot be defined or imported (E0703 if requested); negative test (IMP-5)
AMB-26
Re-export of imported names: the loader requires a name to be defined in the target module (origin check) — no re-exports; unspecified
pin no-re-export (E0703); amend §9.1; three-module test (IMP-7)
AMB-27
Module identity is keyed by bare name, not resolved path: two different lib.shdl files reachable from different importers silently bind to whichever loaded first
pinned: module names are program-global; a resolved-path mismatch against the loaded module → E0701 ('resolves to two different files', naming both) — no new code minted
AMB-28
Module-name case vs case-insensitive filesystems: use Add2 resolves add2.shdl on APFS, fails on Linux; two spellings can load one file as two modules
verify the real filename case; mismatch → E0701 (platform-independent) (IMP-11)
AMB-29
Is the meta { … } block valid SHDL? The grammar has no production; re-flattening emitted output fails E0201 at meta, so DET-4 is undefined
flattener accepts and ignores a trailing meta block (one small production); DET-4 idempotence defined on the structural core (DET-4)
AMB-30
Who populates monitors? base_shdl §4.8 says 'flattener or user annotations'; no annotation syntax or population path exists — always {}
pin V1: always {}; schema {group: [gate_or_wire,…]} reserved; amend §4.8; stage population under FUT (MET-9)
AMB-31
E0403 vs E0906 attribution is path-dependent: A[0] inside a parameterized component raises E0906 even with a literal width; identical A[0] elsewhere raises E0403
pin: inside a specialization, any non-positive port width is E0906; elsewhere E0403; amend §14; test both branches of the shared site (VAL-7)
AMB-32
NULL signal name to poke/peek: unguarded strcmp — UB/segfault, at odds with crash closure
guard in generated C: NULL takes the unknown-signal path (stderr, no-op/0, dirty untouched); test via ctypes (ABI-16)
AMB-33
meta.ports covering only a subset of header wires: uncovered inputs are stuck at 0 and ABI-unreachable, uncovered outputs unobservable — silently
pin legal-but-defined (matches the referenced-bits philosophy) and amend base_shdl §4.2 — or require total coverage with a ModelError; then test
AMB-34
Duplicate wire references in meta.ports (within one port or across ports of one direction): silent last/highest-bit-wins aliasing
reject duplicate use of an input wire (ModelError); allow output-wire reuse (harmless fan-out); negative cases both shapes
AMB-35
meta.ports present but a direction key absent: zero ports of that direction with no diagnostic (identity synthesis fires only when ports is wholly absent)
require both inputs and outputs keys whenever ports is present (ModelError naming the missing key)
AMB-36
Base SHDL naming reservations (§3.5 __, §6 …_<digits>_): producer-side obligation or consumer-enforced? shdlc accepts both silently while §3.6 connection rules are fully re-validated
pin producer-side: consumers MAY accept violating names without semantic interpretation; state in base_shdl §6 + shdlc acceptance test (CCT-18) — or add rejection
AMB-37
base_shdl §3.6 omits two rules shdlc enforces and tests: input wires cannot be connection destinations; only pin O is readable
amend §3.6 with both rules (implementation and tests already conform)
AMB-38
Release ABI surface drift: step_settle/run_batch are exported, tested, and symbol-asserted but absent from shdlc_goals §3.1/§3.2/§10 (their pointer params sit outside §3.2's type list)
amend goals to document both with the observable-equivalence contract; extend §3.2 to 'primitive C types and pointers to them'; clarify run_batch borrows, never owns (ABI-11/12)
AMB-39
Reset semantics contradiction: shdlc_goals says 'all-zero' in §2.4/§3.1/§7.1; base_shdl §4.11 + the implemented, tested behavior re-apply init seeds
amend shdlc_goals: reset() returns to the power-on state — all-zero except meta.init seeds (SIM-7)
AMB-40
Debug-build name lookup namespace: a port and a gate may legally share a name; V.1's peek_gate needs a rule before it lands
pin separate namespaces: poke/peek address ports exclusively, peek_gate gates exclusively; SHDB qualifies on collision; record in shdlc_goals
AMB-41
shdl.md §11.4's SRLatch example does not compile as printed (uses NOR without use stdgates::{NOR})
fix the spec example; the fixture already pins the corrected form
Domain V — Future components: obligations defined now (FUT) ⚪
These activate when each Layer-1+ component is built. The legacy suite's debugger catalog maps
here — none of it is lost, it is staged.
V.1 SHDLC debug build — release ≡ debug differential on the full fixture+fuzz corpus;
peek_gate / peek_gate_prev (current vs previous buffer — the two-buffer model makes "prev"
nearly free and the test must prove it's really the previous cycle); get_cycle semantics
(AMB-8); gate enumeration (count, names, type codes 0–5, chunk/lane), O(1)-ish lookup scaling
test at >1000 gates; .shdb = embedded meta + state_region, byte-equal JSON both places;
upgrade the differential harness to full-gate-state lockstep (closes FUZ-8); name-namespace
rule per AMB-40.
V.2 PySHDL — multi-bit poke/peek via ports; settle() = step(max_depth), refused when
has_feedback; power-on reset honoring init; context manager & dict-style access; boundary
re-runs of the legacy "comprehensive" catalog (pass-through 0–255, 0xFFFF patterns, bitwise ops,
nibble extraction) — mostly subsumed by conformance traces but cheap to mirror at the Python API.
EXECUTED 2026-06-12 — PySHDL is built (SHDL/ package); the full V.2 obligation set is
green (tests/pyshdl/, 130 tests over 10 modules + the session-scoped ExampleCache fixture in
conftest.py). Per-obligation closure:
context manager, all four constructors, two-instance independence (same source AND same library),
close/del safety, artifact lifecycle — ✅ test_pyshdl_construct.py
(test_context_manager_closes, test_two_instances_over_one_source_are_independent,
test_two_instances_over_one_library_file_are_independent, test_use_after_close_raises,
test_del_without_close_is_safe, test_artifacts_cleaned_by_default/test_keep_artifacts_retains_managed_dir/test_explicit_build_dir_is_retained)
legacy "comprehensive" boundary catalog at the Python API (pass-through 0–255, SignExtend 0xFFFF,
ALU bitwise/add boundaries, nibble split/swap) — ✅ test_pyshdl_boundary.py
OracleSim-vs-Circuit random-stimulus lockstep (adder8/mux2/srLatch/dLatch, 150 actions, all ports
every action) — ✅ test_pyshdl_lockstep.py (test_random_stimulus_lockstep)
conformance corpus replayed through the public Circuit API (CNF-5) — ✅ test_pyshdl_conformance.py
(test_corpus_trace_replays_bit_exactly)
SR16 CPU smoke test through the public API — ✅ test_pyshdl_cpu.py (test_sr16_runs_a_program)
V.3 SHDB debugger — port the legacy catalog wholesale: DebugInfo loading & JSON fidelity;
SymbolTable resolution + completion; controller poke/peek/step/StopInfo; internal-gate
inspection mid-propagation; breakpoints (value-change, conditional, temporary, hit counts,
enable/disable/clear); watchpoints; run-until-breakpoint with max_cycles; bulk inspection;
robustness (peek before step, 5 resets, 1000 steps, context-manager cleanup); SourceMap
tolerance of missing locations.
V.4 Testbench runner (.shtb) — format round-trip; conformance traces expressible as .shtb
and replayable bit-exactly (the corpus becomes the runner's own acceptance test).
V.5 Backends — Verilog: cross-validate against Verilator on the conformance corpus
(independent implementation of the unit-delay model — the strongest external check available).
BLIF: ABC formal equivalence between flattener output and known-equivalent circuits (CLA vs
ripple adder). Both: corpus Tier A inputs → backend → external tool agrees with golden traces.
V.6 State Region — header magic/version, layout documented in .shdb matches reality
(offset-poke equals ABI-poke), identical layout regardless of allocation, shared-memory
read-only observer sees live values.
V.7 Optimization tiers (Layer 7) — every tier: full conformance + differential + fuzz at
parity with V1, bit-exact, per the "validated bit-exactly against V1" mandate. The suite as
specified here is the gate; no new obligations, just re-execution per tier.
Every ISA instruction lockstep vs golden model (PC, R0–R7, flags, halt, cycle cost after every instruction)
✅
CPU-2
ALU: 13 ops × corner + random vectors × carry-in
✅
CPU-3
Power-on fixed-point regression: SRLatch — oracle full-gate-state fixed point (ticks 1–8); DLatch/MSFFE/RegE plus RegFile, RAM256 (incl. write-isolation) and the SR16 top's visible state held across the 15-offset settle sweep (the consecutive 1–8 prefix covers every phase of period ≤ 8)
Real programs: fib, gcd, memcpy, recursive sum, array wraparound — lockstep plus hand-derived headline constants (so the golden model cannot common-mode vouch); RAM/regfile/seq element units
✅
CPU-6
Reserved encodings via .word (shift functs 6/7 behave as NOT under lockstep; MISC/branch reserved words; canary register checks)
DMA port (ISA.md §6): full 256-word image load + bit-exact readback through LdEn/LdWe/LdAddr/LdData; LdEn freeze of a running CPU asserted directly
✅ (freeze of a mid-execution CPU asserted directly: zero drift + RAM untouched + clean resumption)
CPU-9
Memory-model aliasing (ISA.md §1): data addresses alias mod 2^A (incl. negative-EA wrap mod 2^16), instruction fetch aliases mod 2^A, PC wraps 0xFFFF→0
✅
CPU-10
HALTED is terminal (ISA.md §4): extra clocks after HALT change no visible architectural state
✅
CPU-11
ALU Op[4] codes 13–15: the reference models them as adder pass-through but no test drives them — pin at unit level or prove control never emits them
✅ (unit-pinned 13/14/15 + decode analysis showing control never emits them)
CPU-12
Shipped example programs (examples/CPU/programs: mul.s, popcount.s, maxarray.s) run under lockstep vs golden (today only the profiling scripts touch them)
✅ (all three under lockstep + hand-derived headline constants)
CPU-13
Lockstep input-space corners: an ISA-level write to R0 (no program targets rd=0 — a writeback special-case bug would be invisible at system level); shift-group V-preservation witnessed with V=1 pre-set (today only ever V=0)
✅ (R0 writeback across all RegWDataSel sources + shift-group V-preservation with V pre-set to 1)
41 codes, 100% enum-enforced, per-raise-site matrix (107 sites, DIA-2), exact line:col (DIA-8), full five-field CLI format (DIA-3)
Covered+ for codes and sites; the legacy multi-error/W-codes/"did you mean" features are now pinned as deliberate V1 non-goals (DIA-4/5/6) rather than gaps
Debugger (.shdb, breakpoints, watchpoints, symbol table…)
Not built yet (Layer 1)
Staged, fully specified in FUT V.3
Legacy's own admitted gaps: sequential elements, >16-bit, error recovery
New suite closes the legacy gaps; parser error recovery is now a pinned non-goal (fail-fast, DIA-4)
(no legacy equivalent)
Differential oracle lockstep, netlist fuzzing, frozen conformance corpus, determinism across hash seeds/opt levels, strict-CFLAGS proofs, ABI dirty-flag state machine, CPU golden-model lockstep
Net-new, strictly more
Bottom line: the new suite (1905 collected tests at PySHDL 1.1.0 — 1644 toolchain + 130 PySHDL driver-level + 131 shdl CLI (tests/shdl_cli/) —
~15k test lines — ~16k including the conformance runner — plus 38 conformance cases / 40 frozen
traces) covers essentially everything
the legacy suite covered for components that exist, and is categorically stronger on simulation
semantics, verification methodology, and regression protection. The three deliberate-feature
questions the legacy suite was "ahead" on (warnings, suggestions, multi-error reporting) are now
pinned as explicit V1 non-goals (DIA-4/5/6, shdl.md §14.1); only the debugger remains, staged
under FUT V.3.
MET-4/7/8/9/10/11 public metadata validator + BaseEval unknown-key/version-mismatch +
column exactness + basename checks all landed
CCT-5 ASAN/UBSAN differential; CCT-3/10/11/12/13/15/17/18/19 all closed.
Residual:CCT-6 Linux gcc+clang CI matrix is authored (ci.yml/nightly.yml) but
UNPROVEN — needs one real Linux CI pass (also gates the ABI-13 ELF export-set variant)
SCL-3/4/5 stress fixtures; SCL-6 limits documented in all three specs (max-gates
decided as deliberately uncapped); SCL-7 range-bomb guard on all four range_values
sites plus the RRepl literal-count replication site (E0601)
FUZ-6 nightly soak job authored (nightly.yml, all knobs); FUZ-7 mutation-testing
audit still optional/open
[~] Coverage gate: a report-only coverage job is in nightly.yml (no fail-under yet); the
ratchet to ≥95% on flattener phases is not yet enforced — UNPROVEN until the first CI run
Tests are the spec's enforcement arm. When a test pins previously ambiguous behavior, the
spec is amended in the same change. No "tested but undocumented" semantics.
Regeneration discipline. Conformance artifacts regenerate only via the dedicated script,
with a manifest version bump and changelog entry; CI rejects drift (mechanism: CNF-9 — today
this policy has no enforcement hook).
The completeness assertions are sacred (diagnostics enum match, corpus minimum counts,
STRICT_CFLAGS). They are the mechanisms that keep this document true over time; extending
them (per-site matrix, W-codes) is preferred over adding unenforced conventions.
Randomized ≠ flaky. All fuzz/differential tests are seed-stable per fixture and embed
replay artifacts in failure output. A fuzz failure is a permanent regression test candidate:
minimize and freeze it into the corpus.
Oracles stay strict. BaseEval may be stricter than the C ABI (e.g., raising on overflow
where C masks). Harnesses bridge deliberately (DualSim masks for the oracle); never relax the
oracle to match the implementation.
One lesson, one test. Every bug found in the wild (e.g., the SRLatch power-on fixed-point
incident) lands a minimal pinned regression in the most upstream suite that can express it,
plus a conformance case if observable in traces.
The golden suite is complete when: every row in Domains A–T and W is ✅ (the per-component
rows — CNF-5 (PySHDL wired 2026-06-12; debug build / backends / tiers still open), ABI-18 —
convert and close per component under Domain V); every AMB row has
decision+amendment+test; P0 and P1 registers are empty; CI runs T0–T4 on Linux+macOS per commit
and T5 nightly; and the coverage gate holds. At that point — and only then — the project's
"correct first, fast last" mandate permits Layer-7 optimization work, with this suite re-run
bit-exactly per tier as the unchanging gate.