Skip to content

Commit

Permalink
hardware and verified config: swap order
Browse files Browse the repository at this point in the history
- 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 <[email protected]>
  • Loading branch information
june-andronick authored and lsf37 committed Jan 3, 2024
1 parent 94d4151 commit cdd362e
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 29 deletions.
21 changes: 11 additions & 10 deletions Hardware/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
38 changes: 19 additions & 19 deletions projects/sel4/verified-configurations.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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`
Expand All @@ -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`
Expand All @@ -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`
Expand All @@ -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

0 comments on commit cdd362e

Please sign in to comment.