Add configuration option for reserved mtvec[MODE] values

config/config.json.in

@@ -59,6 +59,10 @@
       // "Xenvcfg_Fatal"  – raise a Sail exception, stopping execution.
       // "Xenvcfg_ClearPermissions" – convert CBIE with 0b10 to 0b00.
       "xenvcfg_cbie": "Xenvcfg_ClearPermissions",
+      // The configuration option determines how to handle the reserved behavior `xtvec[Mode] >= 2`.
+      // "Xtvec_Fatal"  – raise a Sail exception, stopping execution.
+      // "Xtvec_Ignore" – use old Mode of xtvec.
+      "xtvec_mode": "Xtvec_Ignore",
       // The configuration option determines how to handle the reserved behavior: Odd-numbered registers for RV32Zdinx.
       // "Zdinx_Fatal"  – raise a Sail exception, stopping execution.
       // "Zdinx_Illegal" – treat it as an illegal instruction.

model/core/platform_config.sail

@@ -81,6 +81,23 @@ enum XenvcfgCbieReservedBehavior = {
   Xenvcfg_ClearPermissions,
 }
 
+mapping XenvcfgCbieReservedBehavior_str : XenvcfgCbieReservedBehavior <-> string = {
+  Xenvcfg_Fatal <-> "Xenvcfg_Fatal",
+  Xenvcfg_ClearPermissions <-> "Xenvcfg_ClearPermissions",
+}
+overload to_str = {XenvcfgCbieReservedBehavior_str}
+
+enum XtvecModeReservedBehavior = {
+  Xtvec_Fatal,
+  Xtvec_Ignore,
+}
+
+mapping XtvecModeReservedBehavior_str : XtvecModeReservedBehavior <-> string = {
+  Xtvec_Fatal <-> "Xtvec_Fatal",
+  Xtvec_Ignore <-> "Xtvec_Ignore",
+}
+overload to_str = {XtvecModeReservedBehavior_str}
+
 enum RV32ZdinxOddRegisterReservedBehavior = {
   Zdinx_Fatal,
   Zdinx_Illegal,
@@ -90,4 +107,5 @@ let amocas_odd_register_reserved_behavior : AmocasOddRegisterReservedBehavior =
 let fcsr_rm_reserved_behavior : FcsrRmReservedBehavior = config base.reserved_behavior.fcsr_rm
 let pmp_write_only_reserved_behavior : PmpWriteOnlyReservedBehavior = config base.reserved_behavior.pmpcfg_write_only
 let xenvcfg_cbie_reserved_behavior : XenvcfgCbieReservedBehavior = config base.reserved_behavior.xenvcfg_cbie
+let xtvec_mode_reserved_behavior : XtvecModeReservedBehavior = config base.reserved_behavior.xtvec_mode
 let rv32zdinx_odd_register_reserved_behavior : RV32ZdinxOddRegisterReservedBehavior = config base.reserved_behavior.rv32zdinx_odd_register

model/core/sys_regs.sail

@@ -578,12 +578,15 @@ register mtvec : Mtvec  // Trap Vector
 
 // PUBLIC: invoked from set_{ms}tvec() [exceptions/sys_exceptions.sail]
 function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = {
- let v = Mk_Mtvec(v);
- match (trapVectorMode_of_bits(v[Mode])) {
-   TV_Direct => v,
-   TV_Vector => v,
-   _         => [v with Mode = o[Mode]]
- }
+  let v = Mk_Mtvec(v);
+  match trapVectorMode_of_bits(v[Mode]) {
+    TV_Direct => v,
+    TV_Vector => v,
+    _         => match xtvec_mode_reserved_behavior {
+      Xtvec_Fatal => reserved_behavior("Tried to write a reserved value (" ^ dec_str(unsigned(v[Mode])) ^ ") to the MODE field of xtvec."),
+      Xtvec_Ignore => [v with Mode = o[Mode]],
+    },
+  }
 }
 
 bitfield Mcause : xlenbits = {