diff --git a/sw/device/lib/base/README.md b/sw/device/lib/base/README.md
index d7cc3859cd8ef..3c2f0618f2b21 100644
--- a/sw/device/lib/base/README.md
+++ b/sw/device/lib/base/README.md
@@ -9,3 +9,9 @@ This subtree provides headers and libraries known collectively as `libbase`, whi
 
 In general, a library exposing general utilities for working close to the hardware should live in this subtree: for example, a library providing `memcpy` and related symbols.
 A library for talking to a particular peripheral, like a UART port, is a non-example.
+
+## Policy regarding 64-bit division
+
+`libbase` does not provide the `__divdi3` and `__udivdi3` (signed/unsigned 64-bit division) symbols.
+The rationale is that users of the library may have different needs when it comes to the trade-off between the size and speed of the implementation.
+Instead, `libbase` provides `udiv64_slow` which is a relatively slow but compact unsigned 64-bit division.
diff --git a/sw/device/silicon_creator/rom/BUILD b/sw/device/silicon_creator/rom/BUILD
index a0ddb261bc04b..039c8eb5128e0 100644
--- a/sw/device/silicon_creator/rom/BUILD
+++ b/sw/device/silicon_creator/rom/BUILD
@@ -240,6 +240,7 @@ opentitan_binary(
     ],
 )
 
+# 64-bit division is forbidden in the ROM (or needs to use udiv64_slow)
 check_elf_symbols_test(
     name = "mask_rom_symbol_check",
     forbidden = [
diff --git a/sw/device/silicon_creator/rom_ext/BUILD b/sw/device/silicon_creator/rom_ext/BUILD
index 5e60019c2f033..2c73c5f7c3f6d 100644
--- a/sw/device/silicon_creator/rom_ext/BUILD
+++ b/sw/device/silicon_creator/rom_ext/BUILD
@@ -18,6 +18,7 @@ load(
 )
 load("@bazel_skylib//rules:common_settings.bzl", "string_flag")
 load("//rules:signing.bzl", "signature_test")
+load("//rules:symbols.bzl", "check_elf_symbols_test")
 
 package(default_visibility = ["//visibility:public"])
 
@@ -358,6 +359,20 @@ ROM_EXT_FEATURES = [
     for slot in SLOTS
 ]
 
+# 64-bit division is forbidden in the ROM_EXT (or needs to use udiv64_slow)
+[
+    check_elf_symbols_test(
+        name = "rom_ext_{}_slot_{}_symbol_check".format(variation_name, slot),
+        forbidden = [
+            "__udivdi3",
+            "__divdi3",
+        ],
+        target = ":rom_ext_{}_slot_{}".format(variation_name, slot),
+    )
+    for variation_name, variation_deps in ROM_EXT_VARIATIONS.items()
+    for slot in SLOTS
+]
+
 [
     opentitan_binary(
         name = "rom_ext_{}".format(name),