update verified platforms; adjust links

Signed-off-by: Gerwin Klein <[email protected]>

Hardware/CEI_TK1_SOM/index.md

@@ -8,7 +8,7 @@ virtualization: ARM HYP
 iommu: System MMU
 soc: NVIDIA Tegra K1
 cpu: Cortex-A15
-Status: "[FC (without System MMU)](/projects/sel4/verified-configurations.html#arm_hyp)"
+Status: "[FC with HYP, no SMMU](/projects/sel4/verified-configurations.html#arm_hyp-tk1)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0

Hardware/OdroidXU4.md

@@ -8,7 +8,7 @@ virtualization: ARM HYP
 iommu: limited System MMU
 soc: Exynos5
 cpu: Cortex-A15
-Status: FC with HYP, no System MMU
+Status: "[FC with HYP, no SMMU](/projects/sel4/verified-configurations.html#arm_hyp-exynos5)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0

Hardware/imx8mm.md

@@ -9,7 +9,7 @@ virtualization: "No"
 iommu: "No"
 soc: IMX8MM-EVK
 cpu: Cortex-A53 Quad 1.8 GHz
-Status: "FC"
+Status: "[FC](/projects/sel4/verified-configurations.html#arm-imx8-mm)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0

Hardware/sabreLite.md

@@ -9,7 +9,7 @@ virtualization: "No"
 iommu: "No"
 soc: i.MX6
 cpu: Cortex-A9
-Status: "[Verified](/projects/sel4/verified-configurations.html#arm)"
+Status: "[Verified](/projects/sel4/verified-configurations.html#arm-sabre-lite)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0

projects/sel4/verified-configurations.md

@@ -67,7 +67,7 @@ The proofs for RISCV64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time
 seL4 features), as well as proofs for AARCH64 are in progress. Refer to the
 [roadmap](/projects/roadmap.html) for status and upcoming features.
 
-## ARM
+## ARM Sabre Lite
 
 | File | `ARM_verified.cmake`
 | Architecture | ARMv7
@@ -76,6 +76,15 @@ seL4 features), as well as proofs for AARCH64 are in progress. Refer to the
 | Hypervisor mode | No
 | **Verified properties** | functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation
 
+## ARM iMX8 MM
+
+| File | `ARM_imx8mm_verified.cmake`
+| Architecture | ARMv7
+| Platform | IMX8MM-EVK
+| Floating-point support | Yes
+| Hypervisor mode | No
+| **Verified properties** | functional correctness incl fast path
+
 ## ARM_MCS
 
 File | `ARM_MCS_verified.cmake`
@@ -86,7 +95,7 @@ Hypervisor mode | No
 Mixed-Criticality-Systems API | Yes
 **Verified properties** | in progress (design-level functional correctness completed)
 
-## ARM\_HYP
+## ARM\_HYP TK1
 
 File | `ARM_HYP_verified.cmake`
 Architecture | ARMv7
@@ -95,6 +104,15 @@ Floating-point support | No
 Hypervisor mode | Yes
 **Verified properties** | functional correctness, incl fast path
 
+## ARM\_HYP Exynos5
+
+File | `ARM_HYP_exynos5_verified.cmake`
+Architecture | ARMv7
+Platform | Odroid XU4
+Floating-point support | No
+Hypervisor mode | Yes
+**Verified properties** | functional correctness, incl fast path
+
 ## AARCH64
 
 | File | `AARCH64_verified.cmake`