diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index ae67bac42..4d6fe77b9 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -97,6 +97,11 @@ mach_bits sys_writable_hpm_counters(unit u)
   return rv_writable_hpm_counters;
 }
 
+bool sys_vext_vl_use_ceil(unit u)
+{
+  return rv_vext_vl_use_ceil;
+}
+
 bool plat_enable_dirty_update(unit u)
 {
   return rv_enable_dirty_update;
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index fe81c901b..c3d9e3694 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -16,6 +16,7 @@ bool sys_enable_zicboz(unit);
 uint64_t sys_pmp_count(unit);
 uint64_t sys_pmp_grain(unit);
 
+bool sys_vext_vl_use_ceil(unit);
 uint64_t sys_vector_vlen_exp(unit);
 uint64_t sys_vector_elen_exp(unit);
 
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index 2713715cc..f71c248f1 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -32,6 +32,8 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
 uint64_t rv_rom_base = UINT64_C(0x1000);
 uint64_t rv_rom_size = UINT64_C(0x100);
 
+bool rv_vext_vl_use_ceil = false;
+
 // Default 64, which is mandated by RVA22.
 uint64_t rv_cache_block_size_exp = UINT64_C(6);
 
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index 8bda5e624..2ce9bfeef 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -38,6 +38,8 @@ extern uint64_t rv_rom_size;
 
 extern uint64_t rv_cache_block_size_exp;
 
+extern bool rv_vext_vl_use_ceil;
+
 // Provides entropy for the scalar cryptography extension.
 extern uint64_t rv_16_random_bits(void);
 
diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index 9cbed51fd..17ee78011 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -55,14 +55,18 @@ function handle_illegal_vtype() = {
   print_reg("CSR vl <- " ^ BitStr(vl))
 }
 
+val sys_vext_vl_use_ceil = pure "sys_vext_vl_use_ceil" : unit -> bool
+
 val calculate_new_vl : (int, int) -> xlenbits
 function calculate_new_vl(AVL, VLMAX) = {
-  /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
-   * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
-   */
-  if AVL <= VLMAX then to_bits(xlen, AVL)
-  else if AVL < 2 * VLMAX then to_bits(xlen, (AVL + 1) / 2)
-  else to_bits(xlen, VLMAX)
+  if(sys_vext_vl_use_ceil()) then {
+    if AVL <= VLMAX then to_bits(xlen, AVL)
+    else if AVL < 2 * VLMAX then to_bits(xlen, (AVL + 1) / 2)
+    else to_bits(xlen, VLMAX)
+  } else {
+    if AVL <= VLMAX then to_bits(xlen, AVL)
+    else to_bits(xlen, VLMAX)
+  }
 }
 
 /* *********************************** vsetvli *********************************** */