Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

hardware and verified config: swap order #217

Merged
merged 1 commit into from
Jan 3, 2024
Merged

hardware and verified config: swap order #217

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 11 additions & 10 deletions Hardware/index.md
View file
Open in desktop
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
View file
Open in desktop
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