strata

The Strata toolchain — typed comptime HDL + integrated verification platform. Design authority: ../proposal/ (decisions register D-001–D-080). Language surface: ../proposal/16-syntax.md. Probe seeds being promoted (rewrite-with-tests-carried, never copied): ../probes/.

Workspace layout

• crates/strata-syntax — lexer, lossless trivia-anchored tree, and resilient-LL parser (D-052/D-053/D-062; full 16-syntax grammar)
• crates/strata-fmt — deterministic source formatter over strata-syntax, exposed for source files through strata fmt
• crates/strata-hir — deterministic, syntax-anchored HIR for declarations, callable bodies, and name-resolution inputs
• crates/strata-width — canonical closed width algebra and normalization (D-037)
• crates/strata-check — package-aware Tier-A header checks plus the supported body-checking slice; unsupported bodies are reported as explicit tri-state deferrals
• crates/strata-arch-ir — the current closed Architectural IR slice with complete provenance-ledger coverage
• crates/strata-arch-sim — deterministic reference semantics for the current Architectural IR slice
• crates/strata-structure — exact P-2 structure reports and summary diffs without physical-cost guesses
• crates/strata-circt — deterministic Architectural IR lowering to pinned textual CIRCT hw/comb/seq
• crates/strata-forge — deterministic Forge v0 manifests, workspaces, local path resolution, and canonical locks
• crates/strata-cli — parse, fmt, check, compile, structure, and reference simulate drivers over the shared frontend
• tests/circt — pinned, source-to-tool strata compile → CIRCT → SystemVerilog → synthesis/simulation contract
• tree-sitter-strata — presentation-only grammar and shared-corpus conformance ratchet; eight valid-corpus gaps remain explicit

Package-wide formatter discovery and forge.toml formatting remain deferred with later architecture IR/ledger phases.

Run cargo xtask ci for the ordinary workspace gate and cargo xtask circt for the source-to-tool boundary: Counter source is compiled through the CLI, checked against the deterministic MLIR contract, lowered through pinned CIRCT, synthesized, and simulated. The gate resolves CIRCT tools from CIRCT_BIN or PATH and fails closed if the pinned toolchain or Icarus Verilog is unavailable. Set STRATA_CI_CIRCT=1 to explicitly include it in the ordinary CI gate.

The current executable Counter slice is available through:

simulate is the deterministic Architectural IR reference interpreter, not the roadmap's later Arcilator integration. Static Phase 1 value inputs use one --input NAME=VALUE per declared input. Changing inputs use --stimulus FILE, a strict strata-stimulus/0 JSON document whose cycles array contains one complete input object per requested cycle. Bool inputs are JSON booleans; UInt inputs are quoted unsigned decimal integers so arbitrary-width values remain exact. The stimulus cycle count must equal --cycles, and static inputs and a stimulus file are mutually exclusive.

The compiler slice supports ordered multiple named outputs across checking, Architectural IR, provenance, structure reports, simulation, and CIRCT. Its retained expression algebra includes Bool not/and/or, Bool and UInt equality, inequality, value-producing if, UInt constants, and wrapping addition. Run the bounded presentation-grammar ratchet separately with:

This ratchet currently holds five clean shared fixtures and eight explicit valid-fixture gaps; it is not the Phase 1 zero-gap/fuzz-corpus gate yet.

Invariants enforced from day one

• P-6: determinism everywhere; no wall clock, no env-dependence in any tool path
• D-053: parser losslessness and recovery invariants are CI-fuzzed (text(tree) == input, including malformed input)
• R-LS-1 lineage: one frontend — every tool is a driver over these crates