MIRR: A Safety-Critical HDL Compiler
with Formal Width Inference

Abstract

Safety-critical cyber-physical systems demand hardware that is correct by construction. We present MIRR, an open-source Rust compiler (30,719 lines, 101 files, zero unsafe blocks) for a domain-specific language targeting safety-critical hardware–software co-design. MIRR compiles temporal guards, guarded reflexes, and LTL safety properties through a 9-stage deterministic pipeline into 9 emission backends including SystemVerilog RTL, FIRRTL, and a novel 30-instruction R-SPU ISA with 32-bit binary encoding, tagged-word registers, and cycle-accurate simulation. Width inference is backed by 1,906 lines of Rocq proofs (55 theorems across 12 files). A signedness type system with 16 inference rules rejects mixed signed/unsigned expressions. A homoiconic S-expression IR enables code-as-data transformation with a verified round-trip invariant. The compiler enforces NASA Power-of-10 compliance: bounded iteration, zero recursion, and explicit resource limits throughout. A test suite of 2,601 tests achieves a 1.41:1 test-to-source ratio.

This paper is a Living Research Artifact. Every claim above is verifiable live in the browser below—the compiler runs as WebAssembly, the proofs are in the repo, and the paper is GPL-3.0 licensed so it can never be paywalled.

Claims

1. MIRR compiles temporal specifications to correct SystemVerilog, FIRRTL, R-SPU assembly, S-expression IR, JSON netlist, and DOT graph. [Evidence ↓]
2. Width inference is sound: no assignment silently truncates a value. Backed by 55 Rocq theorems (52 fully mechanized).
3. All compiler algorithms are bounded: no unbounded recursion or iteration exists. Every loop has an explicit MAX_* constant. [Evidence ↓]
4. The compiler is safe: #![forbid(unsafe_code)] on every source file.

1. Introduction

Safety-critical cyber-physical systems—neonatal respirators, flight controllers, industrial interlocks, autonomous vehicle watchdogs—demand hardware that is correct by construction. Traditional flows compile C++ or hand-written Verilog through opaque synthesis tools, leaving a semantic gap between the engineer’s intent and the generated gates. High-level synthesis (HLS) tools narrow this gap but lack native concepts of temporal behavior and formal safety properties. The resulting verification burden falls on post-synthesis simulation, which cannot exhaustively cover the state space of even modest safety monitors.

Hardware construction languages such as Chisel, Clash, and Bluespec raise the abstraction level above RTL, yet none combines temporal guard specification, LTL property compilation, formal width verification, and instruction-level emission in a single deterministic pipeline. Furthermore, existing tools do not enforce the bounded-resource discipline required by NASA Power-of-10 or DO-254 certification workflows.

Contributions

1. A three-construct surface language (Signal, Guard, Reflex) that maps directly to synthesizable hardware primitives.
2. A 9-stage deterministic pipeline producing 9 emission backends: SystemVerilog RTL, FIRRTL, JSON netlist, Graphviz DOT, R-SPU assembly, R-SPU binary, S-expression IR, SystemVerilog testbench, and FPGA scaffold.
3. SCC-based width inference with 1,906 lines of Rocq proofs (55 theorems, 52 mechanized, across 12 proof files).
4. A signedness type system (16 rules, E601–E609) rejecting mixed signed/unsigned expressions.
5. An extended type system with 8 features: refinement types, linear types, effect typing, clock domains, phantom types, type-level naturals, dependent types, session types.
6. The R-SPU ISA v2: 30 instructions across 7 tiers with 32-bit binary encoding and cycle-accurate simulation.
7. A homoiconic S-expression IR with verified round-trip invariant and bounded eval/apply core.
8. A MAPE-K feedback loop simulator for autonomic observability with LTL property monitoring.
9. 2,601 tests at a 1.41:1 test-to-source ratio, with 92 #![forbid(unsafe_code)] directives and 0 Clippy warnings.

Figure 1 shows the complete system architecture, and Figure 2 presents the core grammar fragment.

2. The MIRR Language

MIRR’s design rests on three principles:

P1: The Generative Power of Three. The surface language has exactly three behavioral constructs—Signal, Guard, Reflex—each mapping to a distinct hardware primitive. Signals are typed wires. Guards are temporal conditions implemented as shift registers or saturating counters that fire after a sustained boolean condition holds for a specified number of clock cycles. Reflexes are guarded assignments: when a guard fires, the reflex drives an output signal to a deterministic value.

P2: NASA Power-of-10 Compliance. Every algorithm has an explicit iteration bound. Recursion is forbidden. All 92 source files carry #![forbid(unsafe_code)]. Every loop is bounded by an explicit MAX_* constant.

P3: Properties Are Verification-Only. Safety properties compile to SVA (SystemVerilog Assertions) directives. They produce no hardware—they constrain the verification environment only. Adding or removing properties never changes the synthesized circuit.

Formal Grammar (core fragment)

program   ::= {patterndef} module
module    ::= "module" ID "{" {item} "}"
item      ::= signal | guard | reflex | property | call

signal    ::= "signal" ID ":" dir type ";"
dir       ::= "in" | "out" | "internal"
type      ::= "bool" | "u"N | "i"N

guard     ::= "guard" ID "{" "when" expr "for" N "cycles" ";"  "}"
reflex    ::= "reflex" ID "{" "on" glist "{" {assign} "}" "}"
property  ::= "property" ID "{" [dir_p] body "}"
body      ::= "always(" φ ")" | "never(" φ ")"
            | "eventually_within(" expr "," N ")"
            | "always_followed_by(" expr "," expr "," N ")"
  

Pattern System

Property Forms → SVA Compilation

Type System

The signedness type system enforces the cross-category invariant: signed and unsigned types never mix in the same expression. This eliminates implicit-conversion bugs common in C and Verilog. The core checker (480 lines) uses 16 inference rules across error codes E601–E609. The extended type system adds 8 certification-oriented features (E610–E625):

3. Compilation Pipeline

The pipeline processes MIRR source through 9 deterministic stages, each with explicit bounds on iteration depth and node count.

Parse (Stage 1)

The lexer tokenizes MIRR source into a stream of typed tokens. The recursive-descent parser (parser/mod.rs, parser/expr.rs, parser/pattern.rs, parser/module.rs) constructs a typed AST. Expression parsing uses Pratt precedence for 14 binary operators and 2 unary operators. All expression nodes carry source Span information for downstream diagnostics. Parse errors produce codes in the E1xx range (76 distinct codes covering lexical, syntactic, and structural errors).

Pattern Expansion (Stages 2–3)

Pattern validation checks arity and argument-kind compatibility for all pattern calls. The expander performs compile-time textual substitution bounded by MAX_EXPANSION_DEPTH and MAX_EXPANDED_ITEMS. A bounded DFS detects circular pattern references (E402). Each expanded item carries an origin tag recording which pattern it was instantiated from, preserving DO-254 traceability. The pattern system supports three parameter kinds (signal, constant, pattern) and four argument kinds at the call site, enabling higher-order composition of hardware templates.

Semantic Validation (Stage 4)

Module-level validation checks include: duplicate signal names (E201), undefined guard references (E203), missing output signals (E205), type direction mismatches (E207), and self-referential expressions (E209). The validator enforces that reflex bodies only assign to output or internal signals, never to inputs (E210). Semantic errors occupy the E2xx range with 16 distinct codes.

Type Checking (Stage 5/5b)

The core type checker (Stage 5) infers the type of every expression using a two-phase explicit work stack (zero recursion), bounded by MAX_EXPR_NODES = 512. The cross-category invariant—signed and unsigned types never mix—is the central rule, catching the class of implicit-conversion bugs that plague C and Verilog.

Stage 5b, introduced in MEGA-1, applies the extended type system with 8 advanced features: refinement types for value constraints, linear types for single-use signal guarantees, effect typing for side-effect tracking, clock domain qualifiers for CDC analysis, phantom types for zero-cost tagging, type-level naturals for parametric widths, dependent types for value-dependent specifications, and session types for protocol-aware channel communication. Extended type errors span codes E610–E625.

Simplification (Stage 6)

The simplifier performs constant folding and identity reduction. It operates on guards, reflexes, and properties using 33 rewrite rules applied over a maximum of MAX_SIMPLIFY_PASSES passes, each bounded by MAX_SIMPLIFY_DEPTH. Rewrites include: x + 0 → x, x * 1 → x, x && true → x, !!x → x, and constant propagation through comparison operators. The multi-pass design ensures that simplification of one subexpression can expose further simplification opportunities in parent nodes.

Width Inference (Stage 7)

Width inference determines the minimum bit-width for every expression node, using SCC-based constraint solving. The solver runs for at most 16 propagation rounds over a maximum of 256 signals, with individual SCC components bounded at 64 nodes. See Section 4 for the full algorithm and mechanized Rocq proofs (1,906 lines, 55 theorems).

Temporal Compilation (Stage 8)

The temporal compiler translates guards into hardware netlists. An adaptive strategy selects between shift registers (for delays ≤ 16 cycles), counter-comparator circuits (for longer delays), and a third strategy—DynamicCounter—for expression-valued delays with runtime-configurable thresholds (bounded by MAX_DYNAMIC_DELAY = 1,048,576). Boolean compound guards (AND/OR) are decomposed into sub-guards with individual compilation.

The crossover at N = 16 yields a discontinuity: at N = 17, the counter uses 6 flip-flops versus 17 for a shift register, a 2.8× reduction.

logic sustained_pressure_drop_cond;
assign sustained_pressure_drop_cond =
    (airway_pressure < 50);

always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n)
    sustained_pressure_drop_counter <= '0;
  else if (!sustained_pressure_drop_cond)
    sustained_pressure_drop_counter <= '0;
  else if (sustained_pressure_drop_counter < 1000)
    sustained_pressure_drop_counter <=
      sustained_pressure_drop_counter + 1;
end

assign sustained_pressure_drop =
    (sustained_pressure_drop_counter >= 1000);

Guard Classification

Before selecting a hardware strategy, the compiler classifies every guard condition via ConditionKind::try_from_expr(), which pattern-matches the guard’s Boolean expression into one of three canonical forms:

1. SimpleSignal — a bare signal reference (e.g., sensor_active). The signal value is used directly as the sustain condition.
2. NegatedSignal — a logically inverted signal reference (e.g., !engine_running). The compiler emits an inversion gate ahead of the temporal circuit.
3. Comparison — a relational expression of the form signal op literal, where op ∈ {<, ≤, >, ≥, ==, !=}. The compiler emits a combinational comparator whose output feeds the sustain logic.

Any expression that does not match these three forms is rejected at compile time, ensuring the temporal backend never encounters an unclassifiable condition.

Emission Backends

The compiler emits to 9 targets: SystemVerilog RTL (with SVA assertions), FIRRTL (CHIPS Alliance IR), JSON netlist (machine-readable), Graphviz DOT (visual dependency graph), R-SPU assembly (instruction-level), R-SPU binary (32-bit encoded), S-expression IR (homoiconic code-as-data), SystemVerilog testbench (simulation harness), and FPGA project scaffold (Yosys/nextpnr). Six of these are executable live in the playground above.

module flight_controller (
  input  logic        clk,
  input  logic        rst_n,
  input  logic [31:0] altitude,
  input  logic [15:0] airspeed,
  input  logic [15:0] pitch_angle,
  input  logic [15:0] roll_angle,
  output logic        throttle_cut,
  output logic        stabilise,
  output logic        terrain_warn
);
  // -- Temporal Guards --
  // Guard: altitude_low (10 cycles, shift register)
  logic [9:0] altitude_low_sr;
  logic altitude_low_cond;
  assign altitude_low_cond = (altitude < 500);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)
      altitude_low_sr <= '0;
    else
      altitude_low_sr <= {altitude_low_cond,
                            altitude_low_sr[9:1]};
  end
  assign altitude_low_out = &altitude_low_sr;

  // Guard: overspeed (5 cycles, shift register)
  logic [4:0] overspeed_sr;
  logic overspeed_cond;
  assign overspeed_cond = (airspeed > 340);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) overspeed_sr <= '0;
    else overspeed_sr <= {overspeed_cond,
                            overspeed_sr[4:1]};
  end
  assign overspeed_out = &overspeed_sr;

  // -- Reflex Assignments --
  logic altitude_low_out, overspeed_out;
  logic excessive_pitch_out, excessive_roll_out;

  always_comb begin
    terrain_warn = '0;
    if (altitude_low_out) terrain_warn = 1'b1;
  end
  always_comb begin
    throttle_cut = '0;
    if (overspeed_out) throttle_cut = 1'b1;
  end
  always_comb begin
    stabilise = '0;
    if (excessive_pitch_out && excessive_roll_out)
      stabilise = 1'b1;
  end

  // -- Safety Properties (SVA) --
  assert property (@(posedge clk)
    (airspeed < 400));
  assert property (@(posedge clk)
    (altitude < 500) |-> terrain_warn);
endmodule

Stage 6b: SAT-Based Simplification

When PipelineConfig.sat_simplify is enabled, the pipeline invokes a bounded DPLL solver (src/sat/) to prove expression equivalences that algebraic rewriting cannot reach. The solver converts expressions to CNF via Tseitin encoding, bounded by MAX_SAT_VARIABLES = 256 and MAX_SAT_CLAUSES = 1,024.

If two subexpressions are proven equivalent under all valuations within these bounds, the more complex one is replaced by the simpler form. The SAT pass is optional and gated because the DPLL search, while bounded, is more expensive than the algebraic rules of Stage 6; it is most useful for simplifying redundant guard conditions in large specifications.

Clock Domain Crossing Detection

The temporal model currently assumes a single clock domain. The module src/temporal/clock_domain.rs implements CDC violation detection: it inspects signal annotations for clock domain qualifiers (introduced in MEGA-1’s extended type system) and reports errors when signals from different domains interact without explicit synchronization.

Full multi-clock synchronizer generation remains future work; the current implementation ensures that single-clock assumptions are not silently violated. Violations produce errors E618–E619.

Register Retiming

The module src/temporal/retiming.rs implements Leiserson–Saxe register retiming optimization. Given a netlist produced by Stage 8, the retimer rebalances register placement across combinational paths to minimize the critical-path delay while preserving functional equivalence. All iterations are bounded by MAX_RETIMING_ITERATIONS, and the algorithm operates on the single-clock netlist produced by the temporal compiler.

Error Architecture

189 distinct error codes span 8 diagnostic ranges: E1xx (parse), E2xx (semantic), E3xx (temporal), E4xx (pattern), E5xx (width), E6xx (type), E7xx (R-SPU), E8xx (S-expression). Every error carries a source span, severity, and structured message. Negative tests cover all 189 codes.

Interactive Pipeline Visualization

Compile the current playground source through all 9 stages and inspect intermediate representations.

4. Width Inference with Mechanized Proofs

Width inference determines the minimum bit-width for every signal and sub-expression, ensuring no data is silently truncated. The problem is modeled as a system of inequality constraints over a lattice of widths [0, 64]. The implementation spans 2,108 lines across 10 files.

Constraint System

The expression tree is flattened into a post-order array of FlatNode values (bounded by MAX_FLAT_NODES = 512). Each node generates one of 10 constraint kinds:

SCC-Based Solver

The solver performs iterative propagation bounded by MAX_PROPAGATION_ROUNDS = 16. Tarjan’s algorithm detects strongly connected components (bounded by MAX_SIGNALS = 1,024 and MAX_SCC_SIZE = 64). SCCs are classified as expansive (contains Add, Mul, Shl—values can grow) or nonexpansive (Prev-only or bitwise—values circulate but don’t grow). Convergence is guaranteed by monotonicity: widths can only increase, and the lattice has finite height 65.

Rocq Proof Coverage

55 theorems across 12 files (1,906 lines of Rocq). 52 fully mechanized (Qed), 3 axiomatized (Admitted). See claim 2.

Proof Coverage Map

Above the proof boundary (mechanized or axiomatized): width solver (T1–T9, 3 Admitted), SCC analysis (T10–T13), constraint soundness (T4–T8), MinBits (T13–T13b), flattening, truncation, R-SPU encoding (T26), tag safety (T27).
Below the proof boundary (tested only): parser, validator, emitters, temporal compiler, MAPE-K, S-expression, pattern expander—covered by 2,601 tests and #![forbid(unsafe_code)].

Theorem add_sound : forall a b,
  a < Nat.pow 2 (Nat.max a b) ->
  b < Nat.pow 2 (Nat.max a b) ->
  a + b < Nat.pow 2 (S (Nat.max a b)).
Proof.
  intros a b H1 H2.
  rewrite Nat.pow_succ_r; [| lia].
  lia.
Qed.

Theorem e2e_solver_sound :
  forall nodes constraints st,
  well_formed nodes ->
  (forall i, lookup st i = 0) ->
  let result := iterate constraints st
                  (solver_budget (length st)) in
  is_fixpoint constraints result /\
  st <= result.
Proof.
  intros nodes constraints st Hwf Hzero.
  simpl. split.
  - apply solver_terminates.
    intros i. rewrite Hzero.
    unfold MAX_WIDTH. lia.
  - assert (Hgen : forall fuel s,
      s <= apply_constraints constraints s ->
      s <= iterate constraints s fuel).
    { induction fuel as [|fuel' IHfuel'].
      - intros. simpl. apply state_le_refl.
      - intros s Hmono. simpl.
        destruct (list_eq_dec Nat.eq_dec
          s (solver_round constraints s)).
        + apply state_le_refl.
        + apply state_le_trans with
            (solver_round constraints s).
          * exact Hmono.
          * apply IHfuel'.
            apply evaluate_monotone. }
    apply Hgen. apply evaluate_monotone.
Qed.

Theorem opcode_roundtrip : forall op payload,
  (0 <= op < 64) ->
  (0 <= payload < 67108864) ->
  extract_opcode (Z.lor (Z.shiftl op 26) payload) = op.
Proof.
  intros op payload Hop Hpay.
  unfold extract_opcode, extract_bits.
  rewrite Z.shiftr_lor.
  rewrite Z.shiftr_shiftl_l; [|lia].
  replace (26 - 26) with 0 by lia.
  rewrite Z.shiftl_0_r.
  assert (Hpay_shift : Z.shiftr payload 26 = 0).
  { apply Z.shiftr_eq_0; [lia|].
    destruct (Z.eq_dec payload 0) as [->|Hne];
      [simpl; lia|].
    apply Z.log2_lt_pow2; [lia|lia]. }
  rewrite Hpay_shift. rewrite Z.lor_0_r.
  replace (31 - 26 + 1) with 6 by lia.
  rewrite Z.land_ones; [|lia].
  rewrite Z.mod_small; lia.
Qed.

Interactive Proof Dashboard

Query the compiler’s built-in proof status table. Shows all 55 theorems with mechanization status.

5. Type System

The core type checker (480 lines, 16 inference rules) enforces the cross-category invariant: signed and unsigned types never mix in the same expression. Unlike software languages that silently widen unsigned to int, MIRR rejects such coercions because sign extension alters the bit pattern reaching downstream logic—a deliberate trade of convenience for correctness in safety-critical HDL compilation.

Bounded Inference Algorithm

Type inference uses a two-phase explicit work stack with zero recursion, bounded by MAX_EXPR_NODES = 512. Phase 1 walks the AST and pushes nodes in post-order; Phase 2 pops and evaluates bottom-up. This mirrors recursive traversal while satisfying NASA Power-of-10 Rule 1 (no recursion) and Rule 2 (bounded iteration).

Formal Inference Rules

The judgment Γ ⊢ e : τ reads: “under signal environment Γ, expression e has type τ.” Γ maps signal names to their declared types. All 16 rules are extracted directly from typeck/mod.rs. We write u_w for Unsigned(w), i_w for Signed(w), and sign(τ) for the signedness category of τ.

Atoms

Arithmetic & Shift

Logic & Bitwise

Comparison

Negation & Context

Cross-Category Rejection (E608)

The cross-category invariant is a side condition on every binary operator ⊕ over numeric types: sign(a) = sign(b) is required. If violated, E608 is emitted. No implicit signed/unsigned coercion exists in MIRR — mixing uw with iv in any arithmetic, shift, or comparison is a static error.

Assignment Compatibility (τ₂ ≤ τ₁)

The subtyping relation τ₂ ≤ τ₁ holds when a value of type τ₂ can be implicitly widened to τ₁ without loss. Five rules capture all valid conversions; the cross-category invariant (u_w ≰ i_v) is the cornerstone of MIRR’s type safety for hardware.

Core Type Rules

Extended Type System (8 Features)

The extended type checker adds 8 certification-oriented features (E610–E625), each opt-in via PipelineConfig. The extended checker runs 7 phases, each bounded by MAX_EXTENDED_TYPE_NODES = 512. Features target DO-254 Level A certification workflows: refinement types for value-range bounds, linear types for consume-exactly-once resources, effect types for pure/stateful separation, clock domains for CDC crossing detection, phantom types for provenance tagging, type-level naturals for dimension checking, dependent types for value-dependent constraints, and session types for protocol conformance.

6. Formal Semantics

Safety-critical systems require mathematical certainty that a compiler preserves meaning. MIRR’s big-step operational semantics specify what a module means per clock cycle, while the R-SPU transition rules specify how compiled code executes on the target processor.

Module Semantics

Module state is a triple σ = (signals, guards, outputs). One clock cycle executes in two phases: Phase 1 evaluates all guards against input state σ₀ to produce guard vector σ₁; Phase 2 evaluates all reflexes against σ₁ to produce output state σ₂. The two-phase structure prevents guard–reflex circular dependencies within a single cycle.

Guard implementations use shift registers (N-bit history window, fires when all N bits are 1) or saturating counters (fires when counter ≥ N). Reflex conflict freedom is enforced statically by errors E205/E206—no two reflexes drive the same output.

R-SPU State Machine

The R-SPU state is a quintuple S = (regs, guards, pc, cycle, halted). The 256-entry tagged register file stores (value, type tag, provenance tag) per register; 64 guard slots track temporal state. Each instruction completes in exactly one clock cycle with no branches or interrupts in Reflex mode. The transition relation S → S′ is a total function on non-halted states.

Determinism Theorem

Theorem 1 (Semantic Determinism): For any MIRR module M and initial state σ₀, the output state σ_n after n clock cycles is uniquely determined.
Corollary 1 (Bit-Exact Reproducibility): Given identical input sequences, two independent executions produce identical output sequences at every cycle boundary—whether in the R-SPU simulator, synthesized RTL, or FIRRTL backend. This is a prerequisite for DO-254 certification, where reproducible builds are mandatory.

7. Mechanized Proof Corpus

MIRR includes 55 named proof items across 12 Rocq (Coq) source files, achieving a 94.5% mechanization rate (52 Qed, 3 Admitted). Every Proven entry compiles to Qed under Rocq 8.19+ with no axioms beyond the standard library. This table is the single source of truth for the proof corpus.

Admitted Proofs

Three proof items carry Admitted status with validated proof strategies:

1. #19: solver_terminates (Solver.v) — The fixed-point solver terminates because the lattice of bit-widths is finite and every iteration is monotone. Completing this proof requires a well-founded measure on the product lattice [0, 64]ⁿ.
2. #2: min_bits_minimal (MinBits.v) — States that min_bits returns the smallest sufficient width. The forward direction (correctness, #1) is proven; minimality requires showing that k−1 bits cannot represent n.
3. #26: step_one_monotone (Solver.v) — A helper lemma asserting that a single constraint-propagation step preserves the lattice ordering. The gap is composing per-operator monotonicity lemmas (proven in Monotone.v) over the constraint list.

None of the admitted items block downstream proofs: the end-to-end soundness theorem (e2e_solver_sound, #34 in Integration.v) is fully mechanized and does not transitively depend on any admitted lemma.

Representative Proof Excerpts

Three listings illustrate the range of proof techniques used across the corpus. See Listing 6 (constraint soundness via add_sound), Listing 7 (end-to-end solver soundness via e2e_solver_sound), and Listing 8 (R-SPU opcode roundtrip via opcode_roundtrip) in §4 above.

Proof Dependency Structure

The width-inference files compose into the end-to-end soundness theorem via Solver.v (Figure 3). R-SPU proofs are self-contained.

8. S-Expression IR

Campaign MEGA-2 introduced a homoiconic S-expression intermediate representation, following the Lisp tradition of code as data. The module serves three purposes: (1) enable compile-time metaprogramming via code-as-data transformation, (2) provide a serializable, human-readable IR for debugging and tooling, and (3) validate self-hosting by establishing a verified round-trip invariant between the AST and the S-expression encoding.

SExpr Type

The core type (sexpr/types.rs, 210 lines) defines 8 variants:

Submodule Architecture

Bounded Resource Constants

All operations enforce NASA Power-of-10 bounds:

Bounded Eval/Apply Core

The eval engine (eval.rs, 318 lines) implements a bounded eval/apply interpreter for compile-time metaprogramming. Evaluation is strictly bounded: MAX_EVAL_STEPS = 10,000 steps and MAX_EVAL_DEPTH = 32 nested frames. This enables compile-time code generation while guaranteeing termination—a critical property for a safety-critical compiler.

Hygienic Macro Expansion

The macro expander (macro_expand.rs, 143 lines) supports quasiquote/unquote-based template instantiation with hygienic name resolution. Expansion is bounded by MAX_MACRO_EXPAND_DEPTH = 8 nesting levels. Reader macros (reader.rs, 133 lines) allow user-defined syntax transformations, limited to 32 registered macros.

Round-Trip Invariant

The bidirectional converter (convert.rs) guarantees the round-trip invariant:

parse_mirr(s) = sexpr_to_ast(ast_to_sexpr(parse_mirr(s)))

This invariant is verified by 25 self-hosting tests in tests/self_hosting_ir_schema_tests.rs and tests/self_hosting_parity_tests.rs.

(module neonatal_respiratory_monitor
  (signal respirator_enable input bool)
  (signal airway_pressure input (unsigned 16))
  (signal clamp_valve output bool)
  (guard sustained_pressure_drop
    (sustain (lt airway_pressure 50) 1000))
  (reflex clamp_on_pressure_drop
    sustained_pressure_drop
    (assign clamp_valve true)))

Design Rationale

The S-expression IR is not the primary compilation target—SystemVerilog and R-SPU assembly serve that role. Instead, the S-expression layer validates the compiler’s internal representation by providing an independent serialization path. If the round-trip invariant holds, the AST→S-expr→AST path is faithful, which increases confidence that the AST→SystemVerilog path is also faithful.

9. MAPE-K Autonomic Simulator

The MAPE-K feedback loop (Monitor, Analyze, Plan, Execute over a shared Knowledge base) is the canonical framework for self-adaptive systems. MIRR implements a deterministic MAPE-K simulator that validates whether the hardware monitors designed in MIRR can observe and respond to runtime anomalies under fault injection.

Four-Phase Execution

Four phases execute in strict sequence each tick: σ_t+1 = E(P(A(M(σ_t, sensors), K_t), K_t), K_t). The simulator spans 10 submodules: orchestrator, monitor (ring buffer), analyzer (LTL evaluation), planner (priority-based action selection), executor, knowledge (bounded FIFO), LTL property types, and deterministic sensor simulation (LCG PRNG).

Bounded Temporal Operators

Three temporal operators evaluate over rolling windows of sensor data: Always G(P)—scan entire window, return false on first violation; Eventually-within F_≤N(P)—inspect last N entries; Persists P for N ticks—track consecutive satisfying ticks, fire when count ≥ N. All algorithms are iterative with O(window_size) complexity, bounded by MAX_WINDOW_SIZE = 1,024.

Knowledge Base & Audit Trail

The knowledge component maintains a bounded FIFO ring buffer (MAX_LOG_ENTRIES = 4,096). Each record stores tick number, triggering property index, action taken, pre/post state snapshots, and a success flag. The knowledge base exports to JSON for DO-254 evidence trails.

FPGA/ARM Partitioning

The module mape_k/partition.rs implements hardware/software boundary analysis for FPGA/ARM co-design targets. Given a compiled module and resource constraints, the partitioner classifies each monitor as hardware-resident (FPGA fabric) or software-resident (ARM core) based on latency requirements, resource utilization estimates, and I/O proximity.

Resource allocation respects bounded iteration over the signal and guard lists, with MAX_PARTITION_ITERATIONS = 512 ensuring termination. The partitioning result feeds the emission stage, enabling split code generation where hardware monitors emit SystemVerilog and software monitors emit R-SPU assembly.

MAPE-K Bridge

The module mape_k/bridge.rs implements the communication bridge between MAPE-K phases. The bridge routes events from the monitor phase to the analyzer, forwards analysis results to the planner, and delivers planned actions to the executor.

All message queues are bounded (MAX_BRIDGE_MESSAGES = 1,024), and the bridge enforces strict phase ordering to prevent out-of-sequence event delivery. The bridge abstraction decouples the four MAPE-K phases, enabling independent testing and future replacement of individual phases without affecting the overall loop structure.

Resource Bounds

Interactive MAPE-K Dashboard

Run the MAPE-K simulator with the neonatal scenario. The dashboard shows sensor traces, property violations, and autonomic actions over the simulation timeline.

Click Simulate MAPE-K to run.

10. R-SPU Backend

The Reflex Signal Processing Unit (R-SPU) is a safety-critical instruction-level target. The backend spans 3,291 lines across 6 files.

ISA v2: 30 Instructions, 7 Tiers

32-Bit Binary Encoding

Every instruction encodes to exactly one 32-bit word. Bits [31:26] carry a 6-bit opcode (64 slots, 30 used); bits [25:0] carry format-specific payload across 4 formats: R-type (register–register), I-type (register–immediate), G-type (guard), S-type (system). Encoding is formally bijective: decode(encode(i)) = i (Rocq theorem T26).

Tagged-Word Register File

Every register carries three fields: a 64-bit value, a TypeTag (Bool, Unsigned{w}, Signed{w}, Uninitialized), and a Provenance marker (Input, Computed, Literal, Unset). 256 registers in 4 partitions of 64: input ports (R0–R63), output ports (R64–R127), internal state (R128–R191), temporaries (R192–R255). Runtime tag checking on all ALU operations provides defense-in-depth (Rocq theorem T27).

Tag Algebra

The tagged ALU enforces type safety at execution time. Let tag(r) denote the tag of register r. The composition rules are:

• Tag-Arith: If tag(a) = u_w and tag(b) = u_v, and the operation is +, −, or *, then the result tag is u_max(w,v).
• Tag-Cmp: If tag(a) = u_w and tag(b) = u_v, and the operation is =, ≠, <, ≤, >, or ≥, the result tag is bool.
• Tag-Uninit: If either operand’s tag is ⊥ (uninitialized), the operation traps with E708.

This two-layer defense (static type checking + runtime tag checking) ensures that type confusion errors are caught even if the static checker is bypassed by hand-edited R-SPU assembly. Correctness is established by Rocq theorem T27 (tagged_alu_safe): if the static type checker accepts a program, the runtime tag checker never traps. Signed rules are symmetric. Implementation: rspu_tagged.rs, check_alu_tags.

Operational Semantics

The R-SPU executes in two modes: Reflex (default, deterministic, single-cycle) and Host (interrupt-driven). Each R-SPU program executes a fixed sequence per clock tick:

1. LOAD_INPUT preamble
2. Temporal guard init and tick
3. REFLEX_IF conditional execution
4. ASSERT_ALWAYS/NEVER property checking
5. STORE_OUTPUT postamble

Worst-case latency is bounded by MAX_INSTRUCTIONS. The determinism theorem guarantees identical output for identical input sequences.

Exception Model

The exception subsystem (336 lines) defines 7 exception codes with default actions:

Exception depth is bounded by MAX_EXCEPTION_DEPTH = 8. Handlers are registered at load time; the default action table ensures fail-safe behavior when no handler is configured. Additional instructions: TRAP/TRAP_IF (software exceptions), HALT (stop execution), MODE_SWITCH (operational mode transitions), DEADLINE_SET (worst-case execution time per tick).

TypeTag Wire Encoding

Tags are loaded into registers via TAG_LOAD, which takes an 8-bit immediate. The wire encoding is a compact bijection between u8 values and the TypeTag enum.

Register-File Partitioning

The 256-entry register file is partitioned into four contiguous regions of 64 registers each. Partitioning eliminates structural hazards: input and output ports are physically separated from computation registers.

Tier Architecture

The 30-instruction ISA is organized into 7 tiers by complexity. Each tier maps a class of MIRR primitives to one or more R-SPU instructions. Tiers execute in ascending order within each tick, enforcing the load–compute–store discipline.

R-SPU Assembly Output

The compiler emits R-SPU assembly following the tick execution model: load, temporal init/tick/query, reflex, store. The header reports register and guard allocation.

1  LOAD_INPUT  R0, P0    ; respirator_enable
2  LOAD_INPUT  R1, P1    ; airway_pressure
3  CTR_INIT    G0, 1000, R1
4  CTR_TICK    G0
5  CTR_QUERY   R1, G0
6  LOAD_IMM    R192, 1   (w1)
7  REFLEX_IF   G0, R64, R192
8  STORE_OUTPUT R64, P0  ; clamp_valve

Interactive R-SPU Simulator

Compile the current playground source to R-SPU assembly and simulate execution. The simulator traces register state, guard firings, and cycle count.

Click Simulate R-SPU to run.

11. Evaluation

Test Suite

Compilation Benchmarks

Criterion microbenchmarks (100 samples, warm cache). Pipeline time scales approximately linearly with signals × guards. Run these benchmarks live in the benchmark demo above.

Synthesis Validation

All 11 synthesizable examples compile through Yosys (v0.63) with zero errors after SVA property stripping, confirming that properties are verification-only.

Codebase Summary

Safety Assurance (6 Layers)

1. Formally proven: 55 Rocq theorems cover width inference and R-SPU encoding (1,906 proof lines).
2. Statically enforced: 16 type rules + 8 extended features reject unsafe programs at compile time.
3. Bounded by construction: every loop bounded by MAX_* constants, zero recursion, zero unsafe code.
4. Tested: 2,601 tests including golden-output, negative (all 189 error codes), and round-trip invariant tests.
5. Dynamically checked: R-SPU tagged-word register file catches type confusion at execution time.
6. Known gaps: 3 Admitted Rocq theorems, components below the proof boundary rely on testing.

12. Safety Assurance Argument

Safety-critical hardware certification under DO-254 requires a structured assurance case: a hierarchy of claims, evidence, and identified gaps that allows a certification authority to evaluate residual risk. No existing HDL compiler provides such an argument. MIRR’s assurance case is presented as six layers, ordered from strongest to weakest evidence, following the principle that honest disclosure of gaps is more credible than inflated coverage claims.

Layered Assurance Case

Layer 1: Formally Proven

The strongest evidence is mechanized proof. Width inference soundness is established by 55 Rocq theorems totaling 1,906 proof lines across 12 files. Of these, 52 are fully mechanized (Qed); the remaining 3 have proof sketches (Admitted) that establish the proof strategy without completing every inductive case.

We emphasize the distinction between proven and sketched: the 3 admitted theorems represent a real gap. They are listed here as Layer 1 evidence only to the extent that the proof structure has been validated; full mechanization remains future work.

Layer 2: Statically Enforced

Every one of MIRR’s 101 source files carries the directive #![forbid(unsafe_code)], which instructs the Rust compiler to reject any unsafe block at compile time. Combined with #![deny(warnings)] at the crate root, this eliminates dead code, unused variables, and—most critically—the entire class of memory-safety bugs (use-after-free, buffer overflows, data races) that the borrow checker prevents. The result is zero unsafe blocks across 30,719 source lines.

Layer 3: Bounded by Construction

Following NASA Power-of-10 Rule 2 (“all loops must have a fixed upper bound”), every loop and every dynamically sized allocation in MIRR is governed by an explicit MAX_* constant:

These bounds guarantee worst-case execution time (WCET) analysis is feasible: no code path can iterate more than 10⁶ times, and most paths are bounded by constants two to three orders of magnitude smaller.

Layer 4: Tested

The test suite comprises 2,601 tests (292 unit, 2,309 integration) with a 1.41:1 test-to-source line ratio. Three testing patterns provide distinct kinds of assurance:

• Golden-output tests compare emitted SystemVerilog, FIRRTL, R-SPU assembly, and S-expression output byte-for-byte against checked-in references.
• Negative tests exercise every one of 197 distinct error codes, asserting both the code and the source span.
• Round-trip invariant tests verify from(to(x)) = x for S-expression serialization and R-SPU binary encoding.

Layer 5: Dynamically Checked

The R-SPU simulator implements a tagged-register architecture: every u64 register carries an 8-bit TypeTag distinguishing Bool, Unsigned{width}, Signed{width}, and Uninitialized. ALU operations check tag compatibility at runtime and raise one of seven exception codes (0–6) on type violations, deadline overruns, or invalid operations. Three configurable exception actions—Halt, EmergencyStop, and TrapToHost—allow the deployment context to determine the appropriate failure response.

Layer 6: Known Gaps

Honest disclosure of limitations is essential to a credible assurance case:

1. Formal semantics scope. Formal operational semantics are provided (Section 6), including big-step evaluation rules, R-SPU transition rules, and a determinism theorem. However, these semantics have not yet been mechanized in a proof assistant; pen-and-paper proofs remain the current level of assurance.
2. Incomplete proofs. 3 of 55 Rocq theorems use Admitted (proof sketches). While the proof strategies are validated, full mechanization has not been achieved.
3. No silicon tape-out. All synthesis results are gate-level simulations through Yosys; no physical ASIC or FPGA bitstream has been tested on hardware.
4. No physical MAPE-K deployment. The autonomic feedback loop has been validated only in software simulation, not on a physical sensor–actuator loop.
5. Scalability untested. The largest validated module contains 27 signals and 13 guards. Behavior at larger scales (hundreds of signals) is uncharacterized.

Residual Risk

The primary residual risk is that the formal operational semantics have not yet been mechanized in a proof assistant. Mechanization in Rocq would close this gap and enable compiler-independent verification. Until then, the assurance case rests on defense in depth: six complementary layers, each catching classes of defects that the others miss, with honest enumeration of what remains uncovered.

Stage        Proven  Bounded  Tested  Gap
-------------------------------------------
Parse          --     MAX_*    E1xx    --
Patterns       --     MAX_*    E4xx    --
Semantics      --      --      E2xx    --
Typecheck      --      --      E6xx    --
Simplify       --      --       .      --
Width         Rocq    MAX_*    E5xx    3 adm.
Temporal       --     MAX_*    E3xx    no proof
R-SPU emit    Rocq    MAX_*    E7xx    --
S-expr         --     MAX_*    E8xx    --
MAPE-K         --     MAX_*     .     no HW

13. Case Studies

Three end-to-end case studies exercise progressively larger subsets of the pipeline. All outputs are actual compiler results—no manual editing.

Case Study Summary

Neonatal Respiratory Monitor

Exercises the counter-comparator path. The guard monitors airway_pressure < 50 for 1,000 consecutive cycles. Because 1,000 > 16 (shift-register threshold), the compiler selects a counter-comparator using 11 flip-flops instead of 1,000 shift register stages—a 91% area reduction.

Flight Controller

Exercises shift-register guards and LTL property compilation. All 4 guards use delays ≤ 16 cycles, so shift registers are used: altitude_low (10 stages), overspeed (5), excessive_pitch (8), excessive_roll (4) = 31 generated signals. The property low_alt_warns compiles to the SVA implication pattern P |-> Q.

TMR Sensor Fusion

Exercises pattern instantiation, majority voting, fault detection, and watchdog timers. The TMR module’s lower cell count relative to the flight controller (207 vs. 212) despite 3.25× more guards illustrates counter-comparator area efficiency: the watchdog uses a 7-bit counter (7 DFFs) for 64 cycles, versus 64 DFFs for a shift register.

14. End-to-End Compilation Trace

To make the pipeline concrete, this section traces a single MIRR program—the neonatal respiratory monitor—through all nine pipeline stages. Each stage’s intermediate representation is shown verbatim, demonstrating the deterministic lowering from domain-specific source to multi-backend emission.

Stage 1: Source (MIRR)

The input program declares three typed signals, one temporal guard with a 1,000-cycle sustain window, and one reflex that clamps the output valve when the guard fires:

module neonatal_respirator {
  signal respirator_enable: in  bool;
  signal airway_pressure:   in  u16;
  signal clamp_valve:       out bool;
  guard sustained_pressure_drop {
    when airway_pressure < 50
    for  1000 cycles;
  }
  reflex emergency_clamp {
    on sustained_pressure_drop {
      clamp_valve = true;
    }
  }
}

Stage 2: Lexer

The lexer tokenizes the source into a stream of typed tokens: MODULE, IDENT("neonatal_respirator"), LBRACE, SIGNAL, IDENT("respirator_enable"), COLON, IN, TYPE(Bool), and so forth. Token spans are preserved for downstream diagnostics. No errors are produced.

Stage 3: AST Construction

The recursive-descent parser produces the typed AST. Each signal carries its direction and core type. The guard’s condition is represented as a Binary node with operator Lt, and the cycle count is stored as a plain integer:

"signals": [
  {"name": "respirator_enable", "kind": "Input", "ty": {"core": "Bool"}},
  {"name": "airway_pressure",   "kind": "Input", "ty": {"core": {"Unsigned": 16}}},
  {"name": "clamp_valve",       "kind": "Output","ty": {"core": "Bool"}}
],
"guards": [{
  "name": "sustained_pressure_drop",
  "condition": {"Binary": {"op": "Lt",
    "left": {"Signal": "airway_pressure"},
    "right": {"Literal": {"Integer": 50}}}},
  "cycles": 1000
}]

Stage 4: Pattern Expansion

The neonatal respirator does not use pattern definitions (def/reflect), so Stages 2–3 (pattern validation and expansion) are no-ops. The AST passes through unchanged.

Stage 5: Semantic Validation

The semantic validator checks error codes E201–E216 against the module. All signals are referenced at least once, the guard references a declared input signal, the reflex references a declared guard, and output assignments target only output-direction signals. The validator emits 0 diagnostics—the module is semantically well-formed.

Stage 6: Type Checking

The type checker infers the type of every expression node. For the guard condition airway_pressure < 50: the left operand has declared type u16 (unsigned), the integer literal 50 is compatible with unsigned types, and the comparison operator yields bool. The cross-category invariant holds: no signed/unsigned mixing occurs. The reflex assignment clamp_valve = true type-checks because both sides are bool. Zero type errors are produced.

Stage 7: Width Inference

Width inference analyzes 4 expression nodes over 2 propagation rounds with 0 strongly-connected components. The inferred widths are:

• airway_pressure: 16 bits (declared u16).
• Literal 50: fits in u16 (value < 2¹⁶).
• Comparison airway_pressure < 50: bool (1 bit).
• Literal true: bool (1 bit).

All widths are determined in a single fixpoint pass; no SCC-based iterative solving is required for this acyclic expression graph.

Stage 8: Temporal Compilation

The temporal compiler classifies the guard sustained_pressure_drop with delay N = 1,000 cycles. Since N > T_sr = 16, the compiler selects the counter-comparator strategy. The generated hardware:

• sustained_pressure_drop_counter: u11 (⌈log₂(1000)⌉ + 1 = 11 bits), a saturating up-counter.
• sustained_pressure_drop_cmp: bool, the condition comparator output.
• sustained_pressure_drop_out: bool, the guard output (counter ≥ 1000).

Temporal compilation statistics: 0 shift registers, 1 counter, 1 logic gate. The counter uses 11 flip-flops plus one 11-bit comparator, versus 1,000 flip-flops for a shift register—a 90.9× area reduction.

Stage 9: SystemVerilog Emission

The complete SystemVerilog module emitted for the neonatal respirator. The counter-comparator pattern is visible: an 11-bit register increments on each cycle where the condition holds, resets to zero when it does not, and the guard output asserts when the count reaches 1,000:

module neonatal_respirator (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        respirator_enable,
  input  logic [15:0] airway_pressure,
  output logic        clamp_valve
);
  logic [10:0] sustained_pressure_drop_counter;
  logic sustained_pressure_drop_cond;
  assign sustained_pressure_drop_cond = (airway_pressure < 50);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)
      sustained_pressure_drop_counter <= '0;
    else if (!sustained_pressure_drop_cond)
      sustained_pressure_drop_counter <= '0;
    else if (sustained_pressure_drop_counter < 1000)
      sustained_pressure_drop_counter <=
        sustained_pressure_drop_counter + 1;
  end
  logic sustained_pressure_drop_out;
  assign sustained_pressure_drop_out =
    (sustained_pressure_drop_counter >= 1000);
  always_comb begin
    clamp_valve = '0;
    if (sustained_pressure_drop_out)
      clamp_valve = 1'b1;
  end
endmodule

Stage 9: R-SPU Assembly Emission

R-SPU assembly output targeting the 30-instruction ISA v2. Counter-based guard uses CTR_INIT/CTR_TICK/CTR_QUERY. Tagged registers enforce runtime type safety:

LOAD_INPUT  R0, P0      ; respirator_enable
LOAD_INPUT  R1, P1      ; airway_pressure
TAG_LOAD    R0, T1      ; tag: Bool
TAG_LOAD    R1, T16     ; tag: Unsigned(16)
TAG_LOAD    R64, T1     ; tag: Bool
CTR_INIT    G0, 1000, R1 ; counter guard
CTR_TICK    G0           ; advance counter
CTR_QUERY   R1, G0       ; read guard state
LOAD_IMM    R192, 1 (w1) ; true literal
REFLEX_IF   G0, R64, R192 ; clamp_valve = true
STORE_OUTPUT R64, P0     ; emit clamp_valve

Stage 9: S-Expression IR Emission

Homoiconic S-expression IR. The structure mirrors the AST directly; every node is a first-class data value suitable for macro transformation:

(program
  (patterns)
  (module "neonatal_respirator"
    (signals
      (signal "respirator_enable" input bool)
      (signal "airway_pressure"   input (unsigned 16))
      (signal "clamp_valve"       output bool))
    (guards
      (guard "sustained_pressure_drop"
        (< (signal "airway_pressure") 50) 1000))
    (reflexes
      (reflex "emergency_clamp"
        (on "sustained_pressure_drop")
        (assign "clamp_valve" true)))))

Trace Summary

The key observation is deterministic multi-target emission: the same 14-line MIRR source produces SystemVerilog RTL for synthesis, R-SPU assembly for the Reflexive Processing Unit, and S-expression IR for metaprogramming—all from a single invocation of run_pipeline. No stage introduces nondeterminism; given identical source and PipelineConfig, the compiler produces bit-identical output across runs. This is a prerequisite for DO-254 certification, where reproducible builds are mandatory.

15. Toolchain Integration

The MIRR toolchain module provides wrappers for five external EDA tools: Yosys (synthesis), Verilator (lint), SymbiYosys (formal verification), EQY (equivalence checking), and icetime (timing analysis).

Yosys Synthesis Flow

All 11 synthesizable examples compile through Yosys (v0.63) targeting either a generic gate library or iCE40 FPGAs. The MIRR compiler generates a companion bind file that wraps SVA property blocks into a separate verification module, allowing synthesis tools to strip properties before gate-level mapping.

Cell counts range from 15 (shift register guard) to 1,650 (FIR filter). This demonstrates that the compiler produces synthesis-ready SystemVerilog across a range of module complexities.

FPGA Scaffold Generation

The --emit fpga-scaffold flag generates a complete iCE40 HX8K project directory including: top-level wrapper with clock/reset, pin constraint file (.pcf), Yosys synthesis script, nextpnr place-and-route script, and a Makefile. This enables one-command synthesis-to-bitstream for prototyping.

Verilator Lint Integration

The toolchain module provides a Verilator --lint-only wrapper for local validation. The wrapper captures lint diagnostics and maps them back to MIRR source locations using the provenance metadata embedded in emitted comments. CI integration is planned.

LSP Integration

The lsp module provides Language Server Protocol support for VS Code. Diagnostics from all 8 error code ranges (E1xx through E8xx) are mapped to LSP severity levels: E1xx/E2xx errors map to Error; E5xx width warnings map to Warning; E4xx pattern hints map to Information.

Planned Extensions

Future toolchain integration targets:

• SymbiYosys for bounded model checking of SVA properties.
• nextpnr for place-and-route with timing-driven optimization.
• icetime for static timing analysis of critical paths.
• EQY for formal equivalence checking between MIRR revisions.

16. Related Work

Hardware Construction Languages

Chisel [1] and its intermediate representation FIRRTL [4] provide a Scala-embedded hardware construction language with parameterized generators. Chisel’s strength is hardware abstraction via Scala classes and traits; its weakness is the absence of built-in temporal specification or formal verification of compiler passes.

Clash [2] uses Haskell’s type system to describe synchronous hardware, leveraging parametric polymorphism and type-level naturals for compile-time dimension checking. Bluespec [3] employs guarded atomic actions with transactional semantics, providing a scheduling model that is more expressive than MIRR’s guard/reflex model but without explicit temporal cycle-count specifications.

None of these languages provides native temporal guard specifications, LTL property compilation to SVA, or instruction-level emission to a bounded ISA.

High-Level Synthesis

HLS tools such as Vivado HLS and Catapult compile C/C++ to RTL but rely on timing constraints and scheduling algorithms rather than explicit temporal semantics. MIRR’s temporal guards are a semantic-level construct, not a synthesis-time optimization.

Temporal Logic in Hardware

Cement2 introduces temporal hardware transactions with latency guards. MIRR’s temporal guard model is simpler: guards specify a condition and a cycle count, compiled to shift registers or counters. This trades expressiveness for deterministic resource usage.

Width Inference

FIRWINE provides formally verified width inference for FIRRTL with Rocq proofs. MIRR’s width inference implements a comparable SCC-based approach with its own proof development (1,906 lines, 55 theorems). Unlike FIRWINE, MIRR’s width pass is integrated into a full compilation pipeline including temporal compilation and instruction emission.

Formal Verification of Compilers

CompCert verified a C compiler in Coq. CakeML verified an ML implementation. MIRR’s proofs target a narrower claim—soundness of width inference and R-SPU encoding—but demonstrate that mechanized proofs are tractable for hardware compiler passes.

Autonomic Computing

The MAPE-K feedback loop [9, 10] is the canonical framework for self-adaptive systems. MIRR’s MAPE-K simulator (10 submodules) applies this framework to hardware monitor observability, providing LTL-based property monitoring with bounded knowledge-base recording. Unlike purely static verification, the simulator exercises the temporal properties under fault injection, closing the loop between design-time specification and runtime adaptation.

Feature Comparison

Table XXVIII compares MIRR with related systems across seven key capabilities: temporal guards (TG), LTL/SVA properties (LTL), type system (TS), formal proofs (FP), instruction-level backend (ISA), S-expression IR (SE), and MAPE-K simulator (MK). MIRR is, to our knowledge, the only open-source system that combines all seven in a single deterministic pipeline.

Quantitative Comparison

Table XXIX compares measurable evidence across the systems, limited to peer-reviewed publications or public release documentation.

FIRWINE has more proof lines but targets a single compiler pass (width inference) for an existing language. MIRR’s proofs cover two passes (width inference and R-SPU encoding) within a full compilation pipeline that also produces executable instructions. Among HDL compilers that serve as both synthesis tools and verification platforms, MIRR has the highest formal verification coverage per source line.

17. Vision and Claims

The original architectural exploration made five design claims. The table below maps each to its implementation status, updated with MEGA-1/2/3 evidence.

Four Roles of MIRR

MIRR serves four complementary roles in the safety-critical hardware ecosystem:

1. Design language — a domain-specific surface syntax for specifying temporal safety monitors with three constructs (Signal, Guard, Reflex) and LTL properties.
2. Compiler — a 9-stage deterministic pipeline producing 6 output formats, with SCC-based width inference backed by mechanized proofs.
3. Runtime ISA — the R-SPU provides instruction-level execution of compiled monitors with deterministic tick-level semantics, tagged registers, and exception handling.
4. Homoiconic IR — the S-expression representation enables code-as-data transformation, compile-time metaprogramming, and self-hosting validation.

Extended Type System as a Path to Dependent Types

The MEGA-1 extended type system introduces 8 advanced type features (Section 5). While each feature is currently independent, the long-term vision is convergence toward a dependent type system for hardware:

• Refinement types prove signal bounds statically, replacing runtime range checks.
• Linear types enforce resource discipline (e.g., each emergency stop channel consumed exactly once).
• Type-level naturals enable compile-time dimension checking (e.g., FIR filter tap count matches coefficient array length).
• Session types verify protocol conformance between communicating hardware modules.

SAT-Based Simplification

A bounded DPLL solver is implemented in src/sat/ with Tseitin CNF encoding (MAX_SAT_VARIABLES = 256, MAX_SAT_CLAUSES = 1,024), gated by PipelineConfig.sat_simplify. Future work includes extending the solver to full property checking of guard conditions.

Future Directions

• Fixed-point types: extend the type system with fixed-point arithmetic (fixed<I,F>) for DSP pipelines.
• DPR controller: generate dynamic partial reconfiguration controllers targeting Xilinx/Intel FPGAs.
• Multi-core R-SPU: extend the ISA for multi-core configurations with inter-core messaging.
• Certification: pursue DO-254 Level A and IEC 61508 SIL 3 certification for the compiler.

18. Conclusion

We presented MIRR, a safety-critical hardware rule language with a Rust compiler (30,719 lines, 101 files, zero unsafe blocks) that compiles temporal guards, guarded reflexes, and LTL safety properties through a 9-stage deterministic pipeline into 9 emission backends. All 11 synthesizable examples compile through Yosys with zero errors, and the full pipeline processes a 32-signal module in 378 microseconds.

Limitations

• Source input bounded to 64 KiB in the browser demo.
• Signed guard lowering is not yet supported.
• The LSP server is not compiled to WebAssembly.
• The R-SPU simulator is available via WASM (simulate_rspu) but provides batch-mode results rather than cycle-stepping.
• 3 of 55 Rocq theorems use Admitted stubs.
• No FPGA bitstream generation in the browser—Yosys synthesis requires the native toolchain.
• Scalability ceiling: largest tested module has 27 signals and 13 guards; industrial systems may require hundreds of monitors.
• Clock domain crossing detection (temporal/clock_domain.rs) identifies violations; multi-clock synchronizer generation remains future work.
• Formal semantics remain pen-and-paper; full Rocq mechanization is future work.

Future Directions

• Fixed-point types (fixed<I,F>) for DSP pipelines.
• SAT-based simplification is implemented in src/sat/ using a bounded DPLL solver with Tseitin CNF encoding, gated by PipelineConfig.sat_simplify. Future work: extend to full property checking.
• DPR controller generation for Xilinx/Intel FPGAs.
• Multi-core R-SPU configurations with inter-core messaging.
• DO-254 Level A certification pathway.

19. AI Tool Disclosure

In accordance with DAC and IEEE policy on the use of artificial intelligence tools in research, we disclose the following:

Tools Used

Claude (Anthropic) was used as a coding assistant during the implementation of the MIRR compiler and as an editorial assistant during manuscript preparation.

Scope of Use

• Code generation: Claude assisted with Rust implementation of compiler passes, test generation, pattern expansion, width inference, type checking, R-SPU backend, S-expression IR, and MAPE-K simulation. All code was reviewed, tested, and validated by the human author.
• Writing assistance: Claude was used for drafting, editing, and formatting portions of this manuscript. All technical claims, experimental design, and intellectual contributions are the sole responsibility of the human author.
• Campaign execution: Claude was used to execute parallel development campaigns (MEGA-1 through MEGA-3) under human supervision, with all changes gated by automated CI (fmt + clippy + test).
• Literature search: Claude was used to identify relevant prior work.

Intellectual Contribution

The MIRR language design, the R-SPU architecture, the compiler pipeline architecture, the decision to use Rocq for formal proofs, and the experimental methodology are original contributions of the human author. The human author takes full responsibility for all content in this paper.

Verification and Quality Assurance

All AI-generated code was subject to the following verification pipeline before acceptance:

• cargo fmt --check — formatting conformance
• cargo clippy --all-targets -- -D warnings — zero warnings policy
• cargo test --all — full test suite (2,601 tests)
• Manual review of every Rocq proof against the proof assistant (Qed. discharge)
• Campaign proposal system with audit, propose, sign/veto, execute, close-out phases

The proposal archive (proposals/) contains the full audit trail: 47 proposals, 42 executed, 5 superseded.

AI tools were not listed as co-authors and did not generate the core intellectual contributions of this work.

20. Campaign Log

The MIRR compiler evolves through a proposal system: audit, propose, sign/veto, execute, close out. This section records the history of changes to the living document and the compiler. Each entry corresponds to a campaign or documentation update.

AUDIT-001 Highlights

• Fixed 4 unbounded recursions (NASA Power-of-10 compliance restored)
• Fixed R-SPU ALU encoding bug (b-register truncation for registers ≥ 64)
• Resolved 8 error code collisions in E170–E183 range
• Removed 5 dead code items (Zero-Debt D3 compliance)
• Merged rspu-reference.md into rspu_isa_spec.md
• Reconciled stale metrics: test count, TMR signals/reflexes
• Fixed living doc contradictions: formal semantics claim, Layer 5 tags
• Created user-facing docs for S-expr IR, MAPE-K, FPGA targets

Full log: proposals/ directory (47 files).

References

1. J. Bachrach et al., “Chisel: Constructing hardware in a Scala embedded language,” in Proc. DAC, 2012.
2. C. Baaij et al., “CλaSH: Structural descriptions of synchronous hardware using Haskell,” in Proc. Euromicro Conf. on Digital System Design, 2010.
3. R. S. Nikhil, “Bluespec System Verilog: Efficient, correct RTL from high-level specifications,” in Proc. MEMOCODE, 2004.
4. A. Izraelevitz et al., “Reusability is FIRRTL ground: Hardware construction languages, compiler frameworks, and transformations,” in Proc. ICCAD, 2017.
5. C. Wolf, “Yosys Open SYnthesis Suite,” 2013. yosyshq.net/yosys
6. G. J. Holzmann, “The Power of 10: Rules for developing safety-critical code,” IEEE Computer, vol. 39, no. 6, pp. 95–97, 2006.
7. RTCA, “DO-254: Design Assurance Guidance for Airborne Electronic Hardware,” 2000.
8. RTCA, “DO-178C: Software Considerations in Airborne Systems and Equipment Certification,” 2011.
9. A. Pnueli, “The temporal logic of programs,” in 18th Annual Symp. on Foundations of Computer Science, IEEE, 1977.
10. R. Tarjan, “Depth-first search and linear graph algorithms,” SIAM J. Computing, vol. 1, no. 2, pp. 146–160, 1972.
11. J. McCarthy, “Recursive functions of symbolic expressions and their computation by machine, Part I,” Commun. ACM, vol. 3, no. 4, pp. 184–195, 1960.
12. J. O. Kephart and D. M. Chess, “The vision of autonomic computing,” IEEE Computer, vol. 36, no. 1, pp. 41–50, 2003.
13. Y. Wang et al., “FIRWINE: Formally verified width inference for FIRRTL,” in Proc. ASPLOS, 2026.
14. H. Nane et al., “A survey and evaluation of FPGA high-level synthesis tools,” IEEE Trans. CAD, vol. 35, no. 10, pp. 1591–1604, 2016.

How to Cite This Work

@software{mirr2026,
  title  = {MIRR: A Safety-Critical HDL Compiler},
  author = {Brandon},
  year   = {2026},
  url    = {https://github.com/brandonfromph/mirr-project},
  license = {GPL-3.0}
}
  

Or use CITATION.cff for citation managers. Cite by commit hash for exact reproducibility.