diff --git a/include/arch/riscv/arch/machine/registerset.h b/include/arch/riscv/arch/machine/registerset.h
index da1f8b586..2415bfd46 100644
--- a/include/arch/riscv/arch/machine/registerset.h
+++ b/include/arch/riscv/arch/machine/registerset.h
@@ -89,8 +89,30 @@ extern const register_t msgRegisters[] VISIBLE;
 extern const register_t frameRegisters[] VISIBLE;
 extern const register_t gpRegisters[] VISIBLE;
 
+#ifdef CONFIG_HAVE_FPU
+
+#define RISCV_NUM_FP_REGS   32
+
+#if defined(CONFIG_RISCV_EXT_D)
+typedef uint64_t fp_reg_t;
+#elif defined(CONFIG_RISCV_EXT_F)
+typedef uint32_t fp_reg_t;
+#else
+#error Unknown RISCV FPU extension
+#endif
+
+typedef struct user_fpu_state {
+    fp_reg_t regs[RISCV_NUM_FP_REGS];
+    uint32_t fcsr;
+} user_fpu_state_t;
+
+#endif
+
 struct user_context {
     word_t registers[n_contextRegisters];
+#ifdef CONFIG_HAVE_FPU
+    user_fpu_state_t fpuState;
+#endif
 };
 typedef struct user_context user_context_t;
 
diff --git a/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
index e70a8b5c8..768846599 100644
--- a/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
@@ -24,7 +24,11 @@
 #endif
 #define seL4_EndpointBits       4
 #define seL4_IPCBufferSizeBits  10
+#ifdef CONFIG_HAVE_FPU
+#define seL4_TCBBits            11
+#else
 #define seL4_TCBBits            10
+#endif
 
 /* Sv39/Sv48 pages/ptes sizes */
 #define seL4_PageTableEntryBits 3