| Certification date | 26 March 2026 |
| Certification program version | 1.0 |
| Organisation name | Codasip |
| Type of organisation | Commercial company |
| Website | www.codasip.com |
| Product link | https://codasip.com/solutions/riscv-processor-safety-security/cheri/x730-risc-v-application-processor/ |
| Full product name | X730-MP4-Lux |
| Product type | IP – CPU |
| Reference number / code | release-Orleans-Lux-1833-FRZ-rc01-11.3.1 |
| Version | 1.0 |
| Is the product a derivative of a qualified product? | No |
| Product description | The X730 is the first commercially licensable processor implementing CHERI-RISC-V. It is written using Codasip’s CodAL processor description language to maximize customization. The baseline X730 microarchitecture is a 64-bit, in-order, dual-issue, 9-stage pipeline with MMU. It has been extended to efficiently handle capabilities and implement CHERI’s new instructions and functions. |
| Extension | Version | Comment |
|---|---|---|
| I | v2.1 | base integer ISA |
| M | v2.0 | multiply and divide |
| A | v2.1 | Atomics |
| F | v2.2 | single precision floating point |
| D | v2.2 | double precision floating point |
| C | v2.0 | compressed encodings |
| Zicsr | v2.0 | Control and status registers |
| Zicntr | Frozen | Base counters and timers |
| Zihpm | Frozen | hardware performance monitors |
| Ziccif, Ziccrse, Ziccamoa | RVA22 | PMAs |
| Za64rs | RVA22 | Reservation set |
| Zicclsm | RVA22 | Misaligned load/stores |
| Zihintpause | v2.0 | Pause execution |
| Zba,Zbb,Zbs | v1.0 | bit-manipulation |
| Zcb | v1.0.2 | code-size |
| Zic64b | RVA22 | 64-byte cache block |
| Zicbom, Zicbop, Zicboz | v1.0 | cache management |
| Zfhmin | v1.0 | half precision floating point |
| Zifencei | v2.0 | I-fetch fence |
| Zam | v0.1 | Misaligned atomics |
| Zbkb | v1.0.1 | Bitmanip instructions for cryptography |
| Zbkc | v1.0.1 | Carry-less multiply instructions |
| Zkt | v1.0.1 | Data independent execution latency |
| Ss1p12 | v1.12 | Supervisor architecture |
| Svbare | RVA22 | Svbare mode – disable memory translation |
| Sv39 | RVA22 | 39-bit virtual addresses |
| Svade | RVA22 | Raise page fault on first access, or first write |
| Sscounterenw | RVA22 | All HPM counters have a writeable enable bit |
| Ssccptr | RVA22 | Hardware page table reading |
| Sstvecd | RVA22 | stvec supports direct mode |
| Sstvala | RVA22 | Update stval on fault |
| Svpbmt | v1.0 | Page-based memory types |
| Svinval | v1.0 | Fine-grained address translation cache invalidation |
| Sm1p12 | v1.12 | Machine architecture |
| Ssu64xl | RVA22 | 64-bit U-mode support |
| Sdext | v1.0-STABLE | External debug interface |
| Sdtrig | v1.0-STABLE | Debug triggers |
| Zcheripurecap | v0.9.3 | CHERI-RISC-V Extension |
| Zcherihybrid | v0.9.3 | Integer pointer mode support |
| Zabhlrsc | v0.9.3 | Byte and half loads and stores |
| Zstid | v0.9.3 | Software thread identification |
| Zish4add | v0.9.3 | Addition using wider registers |
| Zcheripte | v0.9.3 | PTE control of capability storage |
| Zcherilevels | v0.9.3 | CHERI capability levels |
Verification of X730 has been extensive. It has followed a strategy of deconstructing the design into its constituent components and major subsystems, then verifying those independently. This has been done with a mixture of formal property-based environments and simulation, and resulted in ~17 different verification environments, including:
CHERI checks and calculations have their own set of formal proofs to ensure accuracy and robustness.
The memory subsystem has its own simulation environment focused on data coherency in multi-core configurations.
The execution pipeline is simulated in isolation, allowing all instruction semantics to be verified by randomised instruction streams against the RISC-V Sail model.
Formal equivalence proofs are performed to ensure that power-saving techniques such as clock-gating do not change the functionality of the design.
These separate environments allow the verification of each component to explore corner cases far easier than if they were only tested when integrated into the full design. The layering of verification environments (like the CHERI formal and the full execution pipeline above) allows the detection and tracking of “escapes” from one layer to the next. These then drive the improvement of the verification.
All verification results are tracked against requirements to ensure that everything that has been specified has been covered by at least one of the environments and gaps do not form between environments. Codasip’s processes have been reviewed by TUV/SUD and 32-bit configurations generated from the same code-base has received ISO 26262 certification for use in automotive applications.
In total, over 40 person-years of engineering effort has been put into X730’s verification.
In pure-cap mode: None.
In hybrid/integer mode: PCC and DDC are implicitly added to integer pointers.
Page table walks are not bounded by capabilities.
Debug mode disables all CHERI checks. Debug mode is not expected to be active in normal operation. Debug mode can only be entered via RISC-V standard methods. SoC-level security controls are expected on the external debug interface.
None.
Our CPU core cannot make concurrent writes. When in a multi-core configuration the cores can make concurrent writes to the shared L2 cache. The L2 cache, by its nature, cannot make concurrent accesses to the system memories.
CHERI uses a combination of hardware and software to implement temporal safety on the MMU-based X730 core. CHERI allows temporal safety to be enforced by making it possible to accurately identify pointers, and check the memory which they are permitted to access. There have been various papers published on this topic (CHERIvoke, Cornucopia and Cornucopia Reloaded). Each offers improved performance over the previous paper. The X730 implements a 4-bit PTE scheme to accelerate revocation using the scheme from Cornucopia Reloaded allowing virtual memory pages (which do not have virtual aliases) to have their capabilities accurately tracked. It provides Capability Dirty Tracking to identify which pages have had capabilities stored to them, and a load barrier to prevent capabilties from being loaded from pages which have not yet been swept for stale capabilities which would allow use-after-realocation vulnerabilities. Freed memory regions are held in quarantine until all stale capabilities which refer to them have been swept (located and invalidated).
We perform formal verification of CHERI-related components within the microarchitecture to ensure compliance with the specification.
We perform a security analysis of the microarchitecture (including CHERI-specific threat modelling) and generate a set of security requirements and mitigations for required behaviour. For example, this includes the expected behaviour during transient execution.
We have a security test suite and fuzzing framework to cover known transient execution attacks, prediction-based non-transient execution attacks, cache attacks, timing attacks, etc.
We evaluate out-of-context attacks e.g. the impact of RowHammer on CHERI capability tag storage.
We run security test suites against OS and RTOS. e.g. the Juliet test suite as well as kernel test suites (such as syscall fuzzers) adapted for CHERI ABIs.
Vulnerabities have been identified and resolved in both hardware and software (e.g. an incorrectly ordered bounds check during speculative execution)
LLVM19.1.7 Clang and Rust