---

Time as a First-Class Citizen

MIRR is built on the philosophy that time is not an after-thought. In traditional HDL design, implementing a temporal rule (e.g., "if signal A is high for 500 cycles") requires manually managing counters, reset logic, and comparison operators. This is error-prone and verbose.

In MIRR, time is a first-class primitive:

guard sustained_error {
    when error_signal == true
    for  500 cycles;
}

The compiler automatically synthesizes this into a deterministic hardware structure:

• Shift Registers: For short delays (e.g., < 16 cycles), providing single-cycle response.
• Binary Counters: For long delays (e.g., > 16 cycles), optimizing for area efficiency.

This ensures your safety rules are enforced with cycle-accurate precision and zero jitter.

---

FuseSoC Integration

MIRR is fully integrated with the FuseSoC package manager. You can add the MIRR library to your project directly:

fusesoc library add mirr https://github.com/brandonfromph/mirr-project

Once added, you can use MIRR to generate verified hardware IP cores:

# In your .core file
dependencies:
  - brandonfromph:mirr:watchdog:1.0.0

---

What MIRR is

[!IMPORTANT] MIRR is a domain-specific language that compiles temporal safety rules into synthesizable hardware logic — directly, without an OS, scheduler, or interrupt handler in the loop.

You write a rule like: "if airway pressure drops for more than a second, close the valve." MIRR compiles that into a shift-register chain in RTL that enforces the rule in nanoseconds — with mathematical proof that it cannot be missed.

[!NOTE] The target domain is safety-critical embedded hardware: ventilators, flight controllers, autonomous vehicle brake systems. Places where a scheduling delay is not a crash report — it is a physical consequence.

---

Why this is hard

Most HDL compilers operate on one of two extremes: raw RTL (no safety abstractions) or high-level C++ synthesis (no hardware timing primitives). MIRR occupies the space between them — but building that space required solving three non-trivial problems:

---

Example

A neonatal respirator emergency clamp:

module neonatal_respirator {
    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;
        }
    }
}

If airway_pressure stays below 50 for 1000 consecutive clock cycles, clamp_valve is set to true. The compiler turns the for 1000 cycles rule into a shift register chain. No polling loop. No interrupt handler. No kernel.

[!TIP] Compiled output (--emit verilog):

module neonatal_respirator (
    input  logic        clk,
    input  logic        rst,
    input  logic [15:0] airway_pressure,
    output logic        clamp_valve
);
    // Shift-register chain: 1000-cycle temporal guard
    logic [999:0] sustained_pressure_drop_sr;
    // ... RTL implementation
endmodule

---

Compiler Architecture

graph LR
    A["MIRR Source (.mirr)"] --> B["Lexer / Parser\n(src/parser/)"]
    B --> C["Macro Expansion\n+ Pattern Resolution"]
    C --> D["Semantic Validation\n+ Type Checking"]
    D --> E["Width Inference\n(SCC Solver)"]
    E --> F["ECS Ingestion\nflat Vec arrays, EntityId = u32"]
    F --> G["Temporal Lowering\nguards → shift registers"]
    G --> H{Emit Backend}
    H --> I["SystemVerilog RTL"]
    H --> J["FIRRTL"]
    H --> K["R-SPU Assembly"]
    H --> L["S-Expression IR"]
    H --> M["SVA Assertions"]
    H --> N["ARM / RISC-V / DSP"]
    I --> O["Verilator lint"]
    I --> P["Icarus Verilog\ntestbench simulation"]
    I --> Q["Yosys\nequivalence check"]

The ECS Registry (src/ecs/registry.rs) is the compiler's source of truth for all synthesis passes. Hardware declarations (signals, guards, reflexes, properties) are stored as u32 entity IDs across 21 flat Vec<Option<Component>> arrays — pre-allocated at 100,000 entity capacity. No heap fragmentation. No pointer chasing.

---

Key Technical Facts

---

Design Philosophy

[!WARNING] MIRR enforces correctness guarantees at compile time, not runtime.

The language has exactly three constructs — Signal, Guard, Reflex — plus verification Properties and reusable Patterns. See the Tutorial for the full guide.

---

Living Research Artifact

MIRR is published as a Living Research Artifact (LRA) — an interactive paper where the compiler runs live in the browser.

Read the interactive paper →

The paper, the compiler, the Rocq proofs, and the browser demos are one GPL-3.0-or-later licensed artifact. To cite MIRR, use paper/CITATION.cff or cite the commit hash of the version you used.

Want this format for your own research? Fork the LRA Template — a reusable GPL-3.0-or-later scaffold for interactive papers. See the LRA-1.0 Specification for the formal standard.

---

Getting Started

Prerequisites

You need the Rust toolchain and (optionally) iverilog / verilator for RTL simulation:

# Rust toolchain
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

# RTL simulation tools (optional, for simulation tests)
# macOS:
brew install icarus-verilog verilator
# Ubuntu:
sudo apt-get install iverilog verilator

Build

git clone https://github.com/brandonfromph/mirr-project.git
cd mirr-project
cargo build --release

The mirr-compile binary is the primary compiler. Invoke it directly:

# Compile to SystemVerilog RTL
./target/release/mirr-compile examples/neonatal_respirator.mirr --emit verilog

# Compile to FIRRTL
./target/release/mirr-compile examples/flight_controller.mirr --emit firrtl

# All supported emit targets:
# verilog  firrtl  json  sexpr  sva  dot  rspu

Run the Test Suite

cargo nextest run --workspace --no-fail-fast

All 3,469+ tests run headlessly — no GPU, no window, no hardware required.

---

Toolchain

WASM demo — the compiler runs in-browser via WebAssembly. Build with:

rustup target add wasm32-unknown-unknown
cargo install wasm-pack
wasm-pack build crates/mirr-wasm --target web --out-dir ../../demos --release

---

Documentation

---

Roadmap

• Phase 0–6 — Foundation through integration pipeline
• Phase 7a — Safety properties and SVA assertion emission
• Phase 7b — Homoiconic pattern system (def/reflect)
• Phase 7c — Advanced type system (MEGA-1)
• Phase 7d — S-Expression homoiconic IR (MEGA-2)
• Phase 7e — R-SPU instruction set architecture (MEGA-3)
• Phase 7f — Proof-carrying code
• Phase 8 — Multi-core fabric & tape-out
• Phase 9 — Production certification (DO-178C, IEC 62304, ISO 26262)

See docs/roadmap.md for the full technical specification of each phase.

---

Contributing

Contributions are welcome — particularly from researchers in formal verification, hardware synthesis, and safety-critical systems. Read CONTRIBUTING.md before opening a PR.

All contributions must pass:

cargo nextest run --workspace   # all tests
cargo clippy -- -D warnings     # zero warnings
cargo fmt --check               # formatting

---

License

Distributed under the GPL-3.0-or-later License. See LICENSE for the full terms.

The interactive paper, compiler, proofs, and WASM demos are one unified GPL-3.0-or-later artifact and cannot be separated for journal submission under a copyright transfer agreement.

---

Acknowledgments

Built on the work of:

• Xiao et al. (2025) — Cement2: Temporal Hardware Transactions
• Li et al. (2025) — SmaRTLy: RTL Optimization with Logic Inferencing
• Wang et al. (2026) — FIRWINE: Formally Verified Width Inference
• Pnueli, A. (1977) — The Temporal Logic of Programs