Overview
Ariane is an open-source, single-issue, in-order 64-bit RISC-V application-class processor core. It is designed to support a Linux-capable application environment and serves as a publicly available implementation target for research on RISC-V microarchitecture, security, and formal verification.
Description and Implementation
Ariane implements the 64-bit variant of the RISC-V ISA (RV64GC) in its baseline open-source configuration, with the tape-out measured instance corresponding to the RV64IMC subset. The core targets baseline "application class" functionality, including support for the Linux operating system and its application environment, virtual memory, caches, and multiple modes of privileged operation [arxiv:1904.05442v1].
Key measured characteristics of the taped-out Ariane instance fabricated in GlobalFoundries 22 FDX technology include:
- Clock frequency: up to 1.7 GHz
- Peak energy efficiency: up to 40 Gop/sW
- ISA support: RV64GC baseline; measured silicon instance at RV64IMC [arxiv:1904.05442v1]
Role in Security Research
Ariane has been used as the experimental platform for evaluating microarchitectural covert-channel mitigations in combination with the seL4 microkernel's time-protection support. In that work, Ariane is described as "an open-source 64-bit application-class RISC-V core" used to evaluate five known covert channels and the efficacy of hardware time-protection mechanisms. The study reports that a single-instruction RISC-V ISA extension that flushes microarchitectural state enables the OS to close all five evaluated covert channels with low increases in context-switch costs and negligible hardware overhead [arxiv:2005.02193v1].
Role in Formal Verification Research
Ariane is one of three open-source RISC-V cores (alongside PicoRV32 and Rocket Core) used in a comparative study of formal verification methods for RISC-V control paths. The review reports the following verification runtime and bug-finding metrics for Ariane [1]:
- Method: Parametric Invariants
- Runtime: 4.8 hours
- Bugs found: 5
- Maximum memory: 5.5 GB
This places Ariane alongside Rocket Core and PicoRV32 as a representative open-source RISC-V target for empirical evaluation of proof-based, SMT-based, symbolic-execution-based, and AI-assisted verification techniques.
Related Research
The review [1] evaluates Ariane as a target for scalable formal verification strategies applied to RISC-V-based control paths, including:
- Symbolic execution combined with bounded model checking (BMC), used to find assertion violations in RISC-V control FSMs with optimized solver backends such as Z3 and Yices.
- Parameterized invariant-based proof frameworks that reuse property sets across different RISC-V configurations.
- AI-enhanced proof-strategy prediction trees to streamline interactive theorem proving on industrial-scale RISC-V designs.