hardware: improve the text (#216)

* hardware: improve the text - added a high-level summary - added a description of the table - added a link to the verified configuration page - small language tweaks Signed-off-by: June Andronick <[email protected]> Co-authored-by: Gerwin Klein <[email protected]>
seL4 · Dec 20, 2023 · 94d4151 · 94d4151
1 parent 8dba742
commit 94d4151
Showing 1 changed file with 31 additions and 6 deletions.
diff --git a/Hardware/index.md b/Hardware/index.md
@@ -4,23 +4,48 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
 ---
 # Supported Platforms
 
-## Verification status
+### Summary
 
-The seL4 proofs are only for specific platforms, as noted in the *Status* column as follows:
+seL4 is available on 3 major hardware architectures, [ARM](#arm),
+[RISC-V](#risc-v) and [x86](#x86), for a number of platforms with varying
+hardware features.
+
+seL4 is formally verified for specific configurations for a subset of these
+platforms. The depth of the proofs and which properties are verified depend on
+the platform.
+
+The tables below provide more details.
+
+
+### Platforms' attributes
+
+The tables below list the platforms for which seL4 is available. For each
+platform, the tables list:
+
+- whether specific features are supported (e.g. *Virtualisation*, *IOMMU/SSMU*, etc) and to which degree (where applicable);
+- the *verification status* (see more [below](#verification-status));
+- who has contributed this platform port;
+- who is maintaining this platform port.
+
+### Verification status
+
+The seL4 proofs only hold for specific configurations, as noted in the *Verification Status* column in the tables, as follows:
 
 * Unverified: this platform is not verified at all and is not scheduled for 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.
 
-## Simulating seL4
+More information can be found on the [Verified Configurations](../projects/sel4/verified-configurations.md) page.
+
 
-Running seL4 in a simulator is a quick way to test it out and iteratively develop software. However,
-note that feature support is limited by the simulator.
+### Simulating seL4
 
+Running seL4 in a simulator is a quick way to test it out and iteratively develop software.
+Note that feature support is then limited by the simulator.
 See [Running It](/seL4Test#RunningIt) for how to run seL4 using Qemu.
 
-* [Running seL4 on VMware](VMware)
+You can also [run seL4 on VMware](VMware).
 
 ## x86