Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909482612686848 |
|---|---|
| author | Ploix, Louis-Emile Armstrong, Alasdair Melham, Tom Lin, Ray Wang, Haolong Courtney, Anastasia |
| author_facet | Ploix, Louis-Emile Armstrong, Alasdair Melham, Tom Lin, Ray Wang, Haolong Courtney, Anastasia |
| contents | The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compartmentalisation. Architectural capabilities replace conventional integer pointers with memory addresses bound to permissions constraining their use. We present the first comprehensive formal verification of a capability extended RISC-V processor with internally 'compressed' capabilities - a concise encoding of capabilities with some resemblance to floating point number representations.
The reference model for RTL correctness is a minor variant of the full and definitive ISA description written in the Sail ISA specification language. This is made accessible to formal verification tools by a prototype flow for translation of Sail into SystemVerilog. Our verification demonstrates a methodology for establishing that the processor always produces a stream of interactions with memory that is identical to that specified in Sail, when started in the same initial state. We additionally establish liveness. This abstract, microarchitecture-independent observational correctness property provides a comprehensive and clear assurance of functional correctness for the CHERIoT-Ibex processor's observable interactions with memory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_04738 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor Ploix, Louis-Emile Armstrong, Alasdair Melham, Tom Lin, Ray Wang, Haolong Courtney, Anastasia Hardware Architecture B.6.2; J.6 The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compartmentalisation. Architectural capabilities replace conventional integer pointers with memory addresses bound to permissions constraining their use. We present the first comprehensive formal verification of a capability extended RISC-V processor with internally 'compressed' capabilities - a concise encoding of capabilities with some resemblance to floating point number representations. The reference model for RTL correctness is a minor variant of the full and definitive ISA description written in the Sail ISA specification language. This is made accessible to formal verification tools by a prototype flow for translation of Sail into SystemVerilog. Our verification demonstrates a methodology for establishing that the processor always produces a stream of interactions with memory that is identical to that specified in Sail, when started in the same initial state. We additionally establish liveness. This abstract, microarchitecture-independent observational correctness property provides a comprehensive and clear assurance of functional correctness for the CHERIoT-Ibex processor's observable interactions with memory. |
| title | Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor |
| topic | Hardware Architecture B.6.2; J.6 |
| url | https://arxiv.org/abs/2502.04738 |