Make vector length (vl) calculation configurable

When `vl` is recalculated due to `vset[i]vl[i]`, the implementation can have some freedom about which value to use. Specifically when VLMAX < AVL < 2*VLMAX, the implementation can choose any `vl` such that ceil(AVL / 2) <= vl <= VLMAX. See "Constraints on Setting vl" in the spec for more details.

This adds a new option that allows you to pick between `ceil(AVL / 2)` and `VLMAX`. It is not yet hooked up to a CLI option but we will do that once the new config system is in place.

Note that this changes the default from `ceil(AVL / 2)` to `VLMAX`.

Co-authored-by: Yui5427 <[email protected]>

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;

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);
 

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);
 

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);
 

model/riscv_insts_vext_vset.sail

@@ -55,14 +55,21 @@ function handle_illegal_vtype() = {
   print_reg("CSR vl <- " ^ BitStr(vl))
 }
 
-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)
+val sys_vext_vl_use_ceil = pure "sys_vext_vl_use_ceil" : unit -> bool
+
+function calculate_new_vl(AVL : int, VLMAX : int) -> xlenbits = {
+  // See "Constraints on Setting vl" in the vector spec.
+  let new_vl =
+    if AVL <= VLMAX then AVL
+    else if AVL < 2 * VLMAX then {
+      // If VLMAX < AVL < 2 * VLMAX then we can use any value
+      // such that ceil(AVL / 2) <= vl <= VLMAX. Here we provide
+      // two options: ceil(AVL / 2) or VLMAX.
+      if sys_vext_vl_use_ceil() then (AVL + 1) / 2 else VLMAX
+    }
+    else VLMAX;
+
+  to_bits(xlen, new_vl)
 }
 
 /* *********************************** vsetvli *********************************** */