From 695cc0e427dc500b3516d2271e2658279f5b4d9d Mon Sep 17 00:00:00 2001 From: June Andronick Date: Wed, 3 Jan 2024 11:07:31 +0100 Subject: [PATCH] hardware and verified config: swap order - on the suported hardware page, moved x86 table after ARM and RISC-V (to reflect main focus) - on verified configuration page: also moved x86 last and also reordered the list to match the text Signed-off-by: June Andronick --- Hardware/index.md | 21 ++++++------- projects/sel4/verified-configurations.md | 38 ++++++++++++------------ 2 files changed, 30 insertions(+), 29 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index 024880b557..bddb4d7d68 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -47,16 +47,6 @@ See [Running It](/seL4Test#RunningIt) for how to run seL4 using Qemu. You can also [run seL4 on VMware](VMware). -## x86 - -We support PC99-style Intel Architecture Platforms. - -| 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 | - -[X64]: /projects/sel4/verified-configurations.html#x64 ## ARM @@ -85,3 +75,14 @@ We currently provide support for some of the RISC-V platforms. Support for the h | [{{ 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 }} | {% endif %} {%- endfor %} + +## x86 + +We support PC99-style Intel Architecture Platforms. + +| 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 | + +[X64]: /projects/sel4/verified-configurations.html#x64 diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md index b0dc27bbf0..1757624907 100644 --- a/projects/sel4/verified-configurations.md +++ b/projects/sel4/verified-configurations.md @@ -20,7 +20,7 @@ configuration of internal and hardware features, verified configurations are necessarily both less numerous and more specific. These configurations are also referred to as *verification platforms*, -currently constituting: AARCH64, ARM, ARM\_HYP, X64, RISCV64, ARM\_MCS, RISCV64\_MCS +currently constituting: ARM, ARM\_HYP, ARM\_MCS, AARCH64, RISCV64, RISCV64\_MCS, X64 Please consult [Frequently Asked Questions](/FrequentlyAskedQuestions), as well as the [proof and @@ -86,16 +86,6 @@ seL4 features), as well as proofs for AARCH64 are in progress. Refer to the | Hypervisor mode | No | **Verified properties** | functional correctness incl fast path -## ARM_MCS - -File | `ARM_MCS_verified.cmake` -Architecture | ARMv7 -Platform | i.MX 6 (Sabre Lite) -Floating-point support | No -Hypervisor mode | No -Mixed-Criticality-Systems API | Yes -**Verified properties** | in progress (design-level functional correctness completed) - ## ARM\_HYP TK1 File | `ARM_HYP_verified.cmake` @@ -114,6 +104,16 @@ Floating-point support | No Hypervisor mode | Yes **Verified properties** | functional correctness, incl fast path +## ARM_MCS + +File | `ARM_MCS_verified.cmake` +Architecture | ARMv7 +Platform | i.MX 6 (Sabre Lite) +Floating-point support | No +Hypervisor mode | No +Mixed-Criticality-Systems API | Yes +**Verified properties** | in progress (design-level functional correctness completed) + ## AARCH64 | File | `AARCH64_verified.cmake` @@ -123,14 +123,6 @@ Hypervisor mode | Yes | Hypervisor mode | Yes | **Verified properties** | in progress -## X64 - -File | `X64_verified.cmake` -Architecture/Platform | x86 64-bit -Floating-point support | Yes -Hypervisor mode | No -**Verified properties** | functional correctness, no fast path - ## RISCV64 File | `RISCV64_verified.cmake` @@ -149,3 +141,11 @@ Floating-point support | No Hypervisor mode | No Mixed-Criticality-Systems API | Yes **Verified properties** | C verification in progress (design-level functional correctness completed) + +## X64 + +File | `X64_verified.cmake` +Architecture/Platform | x86 64-bit +Floating-point support | Yes +Hypervisor mode | No +**Verified properties** | functional correctness, no fast path \ No newline at end of file