X730

Certification and overview

The X730 is the first commercially licensable processor implementing the CHERI‑RISC‑V architecture. It was certified by the CHERI Alliance on 26 March 2026 under certification programme 1.0. Developed by Codasip, the processor is a 64‑bit, in‑order, dual‑issue design with a nine‑stage pipeline and a memory‑management unit【596381802337460†L148-L168】. The product is written in Codasip’s CodAL hardware description language to maximise customisation【596381802337460†L166-L169】.

Microarchitecture and product details

Codasip describes the product as an IP‑grade CPU core (type “IP – CPU”), version 1.0, with code name X730‑MP4‑Lux. It is not a derivative of an existing qualified product【596381802337460†L148-L165】. The baseline microarchitecture delivers CHERI capabilities via a 64‑bit pipeline and includes an MMU to support hybrid and pure‑capability modes【596381802337460†L166-L170】.

Verification strategy

The X730 has undergone an extensive verification campaign. Engineers broke the design into constituent components and subsystems and verified each one independently using a mixture of formal proofs and simulation, resulting in approximately 17 separate verification environments【596381802337460†L229-L247】. These included formal proofs for CHERI checks and calculations, memory‑subsystem simulation for data coherency, instruction stream simulation against the RISC‑V Sail model and formal equivalence proofs to ensure that power‑saving techniques do not change behaviour【596381802337460†L229-L247】. Verification results are tracked against requirements, and the processes have been reviewed by TÜV/SÜD; similar 32‑bit cores from the same code base have received ISO 26262 certification for automotive use【596381802337460†L255-L259】. In total, over 40 person‑years of engineering effort have been invested in verifying the X730【596381802337460†L262-L264】.

Security and safety features

The X730 runs in both pure‑capability and hybrid/integer modes. In pure‑cap mode no operations can access memory without an explicit capability operand【596381802337460†L265-L269】. Hybrid mode implicitly adds Program Counter Capability (PCC) and Default Data Capability (DDC) to integer pointers, while page‑table walks are unbounded【596381802337460†L265-L272】. Debug mode disables CHERI checks and must be protected at the SoC level【596381802337460†L273-L275】.

To handle temporal safety, the X730 combines hardware and software mechanisms to identify pointers and track the memory they may access【596381802337460†L289-L299】. The processor implements a four‑bit page‑table entry scheme to accelerate revocation, provides capability dirty tracking to identify pages storing capabilities and includes a load barrier to prevent loading capabilities from unswept pages【596381802337460†L289-L300】. Freed memory is quarantined until all stale capabilities referencing it have been invalidated【596381802337460†L289-L302】. These mechanisms enable enforcement of temporal safety without undue performance impact.