Sign up
View stargazers0Sign up
Commits

README.md

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:

sh
1cargo run -p strata-cli -- compile crates/strata-cli/tests/fixtures/counter.strata \
2 --generic WIDTH=3 --clock clock --reset reset --reset-mode synchronous
3cargo run -p strata-cli -- structure crates/strata-cli/tests/fixtures/counter.strata
4cargo run -p strata-cli -- simulate crates/strata-cli/tests/fixtures/counter.strata \
5 --generic WIDTH=3 --cycles 9

simulate is the deterministic Architectural IR reference interpreter, not the roadmap's later Arcilator integration.

The compiler slice supports ordered multiple named outputs across checking, Architectural IR, provenance, structure reports, simulation, and CIRCT. Run the bounded presentation-grammar ratchet separately with:

sh
1cd tree-sitter-strata
2npm ci
3npm test

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