diff --git a/src/dev/arm/gic_v2.hh b/src/dev/arm/gic_v2.hh
index f9b66b8..4104140 100644
--- a/src/dev/arm/gic_v2.hh
+++ b/src/dev/arm/gic_v2.hh
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2010, 2013, 2015-2018 ARM Limited
+ * Copyright (c) 2010, 2013, 2015-2019 ARM Limited
  * All rights reserved
  *
  * The license below extends only to copyright in the software and shall
@@ -309,8 +309,11 @@
             if (gem5ExtensionsEnabled) {
                 ctx_mask = ctx;
             } else {
-            // convert the CPU id number into a bit mask
-                ctx_mask = power(2, ctx);
+                fatal_if(ctx >= 8,
+                    "%s requires the gem5_extensions parameter to support "
+                    "more than 8 cores\n", name());
+                // convert the CPU id number into a bit mask
+                ctx_mask = 1 << ctx;
             }
             return ctx_mask;
         } else {