diff --git a/docs/device_model.md b/docs/device_model.md
index 825365de6..ee63da3a7 100644
--- a/docs/device_model.md
+++ b/docs/device_model.md
@@ -48,6 +48,10 @@ This device is built-in by default, but it can be compiled out with Rust
 features. When compiled in, it is always enabled, and cannot be disabled
 from the command line.
 
+For AArch64 machines, an ARM PrimeCell Real Time Clock(PL031) is implemented.
+This device is built-in by default for the AArch64 platform, and it is always
+enabled, and cannot be disabled from the command line.
+
 ### I/O APIC
 
 `cloud-hypervisor` supports a so-called split IRQ chip implementation by
@@ -69,6 +73,11 @@ enabled by default, the handling of reboot/shutdown goes through the dedicated
 ACPI device. In case ACPI is disabled, this device is enabled to bring to the
 VM some reboot/shutdown support.
 
+### ARM PrimeCell General Purpose Input/Output (PL061)
+
+Simplified ARM PrimeCell GPIO (PL061) implementation. Only supports key 3 to
+trigger a graceful shutdown of the AArch64 guest.
+
 ### ACPI device
 
 This is a dedicated device for handling ACPI shutdown and reboot when ACPI is