Glossary

Terminology and acronyms used throughout the MIRR project.

Term	Definition
AHL	Adaptive Hold Logic — circuit-level mitigation that pauses the clock on timing violations
BMC	Bounded Model Checking — formal verification technique checking properties up to a bounded depth
Cement2	Temporal hardware transaction model replacing absolute timing with shift-register delays
Claims	Verifiable statements in an LRA paper backed by evidence
DAC	Design Automation Conference — target venue for the MIRR living research paper
DPR	Dynamic Partial Reconfiguration — loading partial FPGA bitstreams at runtime
DSL	Domain-Specific Language
Dual-Mode Execution	R-SPU execution mode switching between normal and exception handling
EDA	Electronic Design Automation
EQY	Yosys Equivalence Checker tool
Exception Code	Numeric identifier for R-SPU trap conditions (E7xx range)
FIRRTL	Flexible Intermediate Representation for RTL — Chisel's IR, used as a MIRR emission target
FIRWINE	Formally verified width inference procedure (Wang et al. 2026)
FPGA	Field-Programmable Gate Array
Guard	MIRR temporal condition monitoring signals over time; triggers when condition holds for N cycles
HLS	High-Level Synthesis
Homoiconic	Property where code and data share the same representation (S-expressions)
ISA	Instruction Set Architecture
JSON-RPC	Remote procedure call protocol used by the LRA Service Worker
Living Research Artifact (LRA)	A paper that bundles code, proofs, and GUI into a single GPL-licensed repository
LPF	Lattice Preference File — ECP5 constraint format
LRA-1.0	The specification standard for Living Research Artifacts
LTL	Linear Temporal Logic — formal language for specifying temporal properties
Macro Hygiene	Ensuring macro-expanded identifiers do not capture surrounding bindings
MAPE-K	Monitor–Analyze–Plan–Execute–Knowledge — autonomic computing feedback loop
MIRR	The hardware rule language this project implements
MinGW	Minimalist GNU for Windows — used by oss-cad-suite on Windows
NBTI	Negative Bias Temperature Instability — silicon aging mechanism
NASA P10	NASA Power-of-10 coding rules for safety-critical software
nextpnr	Open-source FPGA place-and-route tool (supports iCE40, ECP5, Nexus)
oss-cad-suite	YosysHQ open-source EDA toolchain distribution
PCF	Physical Constraints File — iCE40 pin assignment format
PDC	Physical Design Constraints — Lattice Nexus constraint format
Provenance	Type-level tracking of a signal's origin through tagged words
Quasiquote	S-expression template with unquote splicing for code generation
R-SPU	Reflex Signal Processing Unit — the custom processor MIRR targets
Reader Macro	User-defined syntax extension in the S-expression parser
Reflex	MIRR action that fires when a guard triggers; the only way to drive outputs
Rocq	Interactive theorem prover (formerly Coq); used for FIRWINE proofs
RTL	Register Transfer Level — hardware description abstraction
S-expression	Symbolic expression — the homoiconic IR used by MIRR
SCC	Strongly Connected Component — cycle in the width dependency graph
SDC	Synopsys Design Constraints — timing constraint format
Service Worker	Browser-side proxy that enables offline operation and the LRA protocol
Signal	MIRR named data path carrying a typed value every clock cycle
SmaRTLy	Inference-driven RTL logic optimization (Li et al. 2025)
SVA	SystemVerilog Assertions — property specification language
Tagged Architecture	R-SPU ISA v2 feature where values carry type metadata at runtime
Tagged Word	R-SPU machine word carrying type and provenance metadata
sby	SymbiYosys — formal verification front-end for Yosys
WASM	WebAssembly — portable binary format; used for running MIRR compiler in the browser
XDC	Xilinx Design Constraints — Vivado constraint format
Yosys	Open-source synthesis tool
zext	Zero-extension — explicit widening of an unsigned value

MIRR Documentation

Glossary

See Also