diff --git a/arch/arm/armv7-m/src/arch_nvic.c b/arch/arm/armv7-m/src/arch_nvic.c
index d4f1f27a4295768438f0952cf6d3c3c81b0aa583..7f11ad6d63ccd2d8fa00cd67ac6617ae335990d3 100644
--- a/arch/arm/armv7-m/src/arch_nvic.c
+++ b/arch/arm/armv7-m/src/arch_nvic.c
@@ -9,6 +9,7 @@
  */
 
 #include <fwk_arch.h>
+#include <fwk_assert.h>
 #include <fwk_interrupt.h>
 #include <fwk_macros.h>
 #include <fwk_mm.h>
@@ -19,13 +20,26 @@
 
 #include <fmw_cmsis.h>
 
+#include <limits.h>
 #include <stdbool.h>
 #include <stddef.h>
 #include <stdint.h>
 #include <string.h>
 
-static unsigned int isr_count;
-static unsigned int irq_count;
+/* We use short enums, so avoid truncation of larger unsigned IRQ numbers */
+#define IRQN_TYPE_MAX \
+    ((uint64_t)(((UINT64_C(1) << (sizeof(IRQn_Type) * CHAR_BIT)) - 1U) / 2U))
+
+static uint32_t isr_count;
+static uint32_t irq_count;
+
+static_assert(
+    UINT32_MAX >= IRQN_TYPE_MAX,
+    "`uint32_t` cannot hold all possible IRQ numbers");
+
+static_assert(
+    UINT_MAX >= IRQN_TYPE_MAX,
+    "`unsigned int` cannot hold all possible IRQ numbers");
 
 /*
  * For interrupts with parameters, their entry in the vector table points to a
@@ -238,7 +252,7 @@ int arch_nvic_init(const struct fwk_arch_interrupt_driver **driver)
     uint32_t align_entries;
     uint32_t align_word;
     uint32_t *vector;
-    char irq;
+    uint32_t irq;
 
     if (driver == NULL) {
         return FWK_E_PARAM;
@@ -249,6 +263,8 @@ int arch_nvic_init(const struct fwk_arch_interrupt_driver **driver)
     irq_count = (ictr_intlinesnum + 1) * 32;
     isr_count = NVIC_USER_IRQ_OFFSET + irq_count;
 
+    fwk_assert(irq_count <= IRQN_TYPE_MAX);
+
     /*
      * Allocate and initialize a table for the callback functions and their
      * corresponding parameters.
@@ -287,7 +303,7 @@ int arch_nvic_init(const struct fwk_arch_interrupt_driver **driver)
     SCB->VTOR = (uint32_t)vector;
 
     /* Initialize IRQs */
-    for (irq = 0; irq < (char)irq_count; irq++) {
+    for (irq = 0; irq < irq_count; irq++) {
         /* Ensure IRQs are disabled during boot sequence */
         NVIC_DisableIRQ((IRQn_Type)irq);
         NVIC_ClearPendingIRQ((IRQn_Type)irq);
diff --git a/product/rdn2/include/fmw_cmsis.h b/product/rdn2/include/fmw_cmsis.h
index 28fc050513d2fc2825dd5c8a540492bc29875f54..ee386ca273f3646f1e4bb4396858ee765b43cf70 100644
--- a/product/rdn2/include/fmw_cmsis.h
+++ b/product/rdn2/include/fmw_cmsis.h
@@ -47,6 +47,7 @@ typedef enum IRQn {
     PPU_CLUSTERS_IRQ = 54, /* Consolidated clusters PPU */
     MHU_AP_SEC_IRQ = 83, /* MHU secure IRQ between SCP and AP */
 
+    IRQn_MAX = INT16_MAX,
 } IRQn_Type;
 
 #include <core_cm7.h>
diff --git a/product/tc0/include/fmw_cmsis.h b/product/tc0/include/fmw_cmsis.h
index ebc684c260a3af7616599ce88fcbef1192ba2ce4..c7add15cbfc0cfeac98a5c44ad6ca57821f0206c 100644
--- a/product/tc0/include/fmw_cmsis.h
+++ b/product/tc0/include/fmw_cmsis.h
@@ -44,6 +44,8 @@ typedef enum IRQn {
     PPU_CORES2_IRQ = 66, /* PPU core 2 IRQ */
     PPU_CORES3_IRQ = 67, /* PPU core 3 IRQ */
     PPU_CLUSTERS_IRQ = 54, /* Consolidated clusters PPU */
+
+    IRQn_MAX = INT16_MAX,
 } IRQn_Type;
 
 #include <core_cm3.h>