Skip to content

Commit

Permalink
hardware: consistency in verification status
Browse files Browse the repository at this point in the history
- changed "pending" and "in progress" to "ongoing"
- removed the "pending status" for the Ariane platform
- changed column title from "Status" to "Verification Status" (it wraps
  so doesn't take much more space)

Signed-off-by: June Andronick <june.andronick@proofcraft.systems>
  • Loading branch information
june-andronick authored and lsf37 committed Dec 19, 2023
1 parent 31df039 commit cb5305c
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 7 deletions.
2 changes: 1 addition & 1 deletion Hardware/JetsonTX2.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ virtualization: "Yes"
iommu: "Yes"
soc: NVIDIA Tegra X2
cpu: Cortex-A57 Quad, Dual NVIDIA Denver
Status: "[in progress](/projects/sel4/verified-configurations.html#aarch64)"
Status: "[Ongoing](/projects/sel4/verified-configurations.html#aarch64)"
Contrib: Data61
Maintained: seL4 Foundation
SPDX-License-Identifier: CC-BY-SA-4.0
Expand Down
2 changes: 1 addition & 1 deletion Hardware/ariane.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ arch: RV64IMAC
virtualization: "No"
iommu: "No"
simulation_target: false
Status: "Pending"
Status: "Unverified"
Contrib: "Data61"
Maintained: "Hensoldt Cyber"
cpu: Ariane
Expand Down
10 changes: 5 additions & 5 deletions Hardware/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
The seL4 proofs are only for specific platforms, as noted in the *Status* column as follows:

* Unverified: this platform is not verified at all and is not scheduled for verification.
* Pending: this feature is currently undergoing verification.
* Ongoing: this feature is currently undergoing verification.
* FC: the functional correctness proofs are complete.
* Verified: all proofs for this platform are complete, including functional correctness, integrity and information flow.

Expand All @@ -26,7 +26,7 @@ See [Running It](/seL4Test#RunningIt) for how to run seL4 using Qemu.

We support PC99-style Intel Architecture Platforms.

| Platform | Arch | Virtualisation | IOMMU | Status | Contributed by | Maintained by |
| Platform | Arch | Virtualisation | IOMMU | Verification Status | Contributed by | Maintained by |
| - | - | - | - | - | - | - |
| [PC99 (32-bit)](IA32) | x86 | VT-X | VT-D | Unverified | Data61 | seL4 Foundation |
| [PC99 (64-bit)](IA32) | x64 | VT-X | VT-D | [FC (without VT-X, VT-D and fastpath)][X64] | Data61 | seL4 Foundation |
Expand All @@ -39,7 +39,7 @@ seL4 has support for select ARMv7 and ARMv8 Platforms.

* [General info on ARM Platforms](GeneralARM)

| Platform | System-on-chip | Core | Arch | Virtualisation | SMMU | Status | Contributed by | Maintained by |
| Platform | System-on-chip | Core | Arch | Virtualisation | SMMU | Verification Status | Contributed by | Maintained by |
| - | - | - | - | - | - | - | - | - |
{%- assign sorted = site.pages | sort: 'platform' %}
{% for page in sorted %}
Expand All @@ -53,8 +53,8 @@ seL4 has support for select ARMv7 and ARMv8 Platforms.

We currently provide support for some of the RISC-V platforms. Support for the hypervisor extension is yet to be mainlined.

| Platform | Simulation | System-on-chip | Core | Arch | Virtualisation | Status | Contributed by | Maintained by |
| - | - | - | - | - | - | - | - | - |
| Platform | Simulation | System-on-chip | Core | Arch | Virtualisation | Verification Status | Contributed by | Maintained by |
| - | - | - | - | - | - | - | - | - |
{% for page in sorted %}
{%- if page.riscv_hardware -%}
| [{{ page.platform }}]({{page.url}}) | {% if page.simulation_target %}Yes{% else %}No{% endif %} | {{ page.soc }} | {{ page.cpu }} | {{ page.arch }} | {{ page.virtualization }} | {{ page.Status }} | {{ page.Contrib }} | {{ page.Maintained }} |
Expand Down

0 comments on commit cb5305c

Please sign in to comment.