Minor architecture cleanup

model/riscv_insts_base.sail

@@ -712,9 +712,8 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
   match cur_privilege {
     User       => { handle_illegal(); RETIRE_FAIL },
     Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) {
-                    (Some(_), 0b1)  => { handle_illegal(); RETIRE_FAIL },
-                    (Some(_), 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
-                    (_, _)           => internal_error(__FILE__, __LINE__, "unimplemented sfence architecture")
+                    (_, 0b1)  => { handle_illegal(); RETIRE_FAIL },
+                    (_, 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
                   },
     Machine    => { flush_TLB(asid, addr); RETIRE_SUCCESS }
   }

model/riscv_sys_control.sail

@@ -315,7 +315,7 @@ function init_sys() -> unit = {
   mhartid     = zeros();
   mconfigptr  = zeros();
 
-  misa[MXL] = arch_to_bits(if xlen == 32 then RV32 else RV64);
+  misa[MXL] = architecture(if xlen == 32 then RV32 else RV64);
   misa[A]   = 0b1;                             /* atomics */
   misa[C]   = bool_to_bits(sys_enable_rvc());  /* RVC */
   misa[B]   = bool_to_bits(sys_enable_bext()); /* Bit-manipulation */

model/riscv_sys_regs.sail

@@ -212,13 +212,13 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv :
 
 function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
   if   xlen == 32
-  then arch_to_bits(RV32)
+  then architecture(RV32)
   else m[SXL]
 }
 
 function get_mstatus_UXL(m : Mstatus) -> arch_xlen = {
   if   xlen == 32
-  then arch_to_bits(RV32)
+  then architecture(RV32)
   else m[UXL]
 }
 
@@ -302,21 +302,18 @@ function clause write_CSR((0x310, value) if xlen == 32) = { mstatus = legalize_m
 
 /* architecture and extension checks */
 
-function cur_Architecture() -> Architecture = {
+function cur_architecture() -> Architecture = {
   let a : arch_xlen =
-    match (cur_privilege) {
+    match cur_privilege {
       Machine    => misa[MXL],
       Supervisor => get_mstatus_SXL(mstatus),
       User       => get_mstatus_UXL(mstatus)
     };
-  match architecture(a) {
-    Some(a) => a,
-    None()  => internal_error(__FILE__, __LINE__, "Invalid current architecture")
-  }
+  architecture(a)
 }
 
 function in32BitMode() -> bool = {
-  cur_Architecture() == RV32
+  cur_architecture() == RV32
 }
 
 // envcfg Resisters

model/riscv_types.sail

@@ -60,20 +60,13 @@ type amo    = bits(1)  /* amo opcode flags */
 
 enum Architecture = {RV32, RV64, RV128}
 type arch_xlen = bits(2)
-function architecture(a : arch_xlen) -> option(Architecture) =
-  match (a) {
-    0b01 => Some(RV32),
-    0b10 => Some(RV64),
-    0b11 => Some(RV128),
-    _    => None()
-  }
 
-function arch_to_bits(a : Architecture) -> arch_xlen =
-  match (a) {
-    RV32  => 0b01,
-    RV64  => 0b10,
-    RV128 => 0b11
-  }
+mapping architecture : Architecture <-> arch_xlen = {
+  RV32  <-> 0b01,
+  RV64  <-> 0b10,
+  RV128 <-> 0b11,
+  backwards 0b00 => internal_error(__FILE__, __LINE__, "architecture(0b00) is invalid")
+}
 
 /* privilege levels */
 

model/riscv_vmem.sail

@@ -203,7 +203,7 @@ register satp : xlenbits
 mapping clause csr_name_map = 0x180  <-> "satp"
 function clause is_CSR_defined(0x180) = extensionEnabled(Ext_S)
 function clause read_CSR(0x180) = satp
-function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_Architecture(), satp, value); satp }
+function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_architecture(), satp, value); satp }
 
 // ----------------
 // Fields of SATP
@@ -240,18 +240,18 @@ function translationMode(priv : Privilege) -> SATPMode = {
     // Translation mode is based on mstatus.SXL, which could be RV32 when xlen==64
     let arch = architecture(get_mstatus_SXL(mstatus));
     match arch {
-      Some(RV64) => { let mbits : bits(4) = satp[63 .. 60];
-                      match satp64Mode_of_bits(RV64, mbits) {    // see riscv_types.sail
-                        Some(m) => m,
-                        None()  => internal_error(__FILE__, __LINE__,
-                                                  "invalid RV64 translation mode in satp")
-                      }
-                    },
-      Some(RV32) => match Mk_Satp32(satp[31 .. 0])[Mode] {    // Note: satp is 64bits here
-                      // When xlen is 64, mstatus.SXL (for S privilege) can be RV32
-                      0b0 => Sbare,
-                      0b1  => Sv32
-                    },
+      RV64 => { let mbits : bits(4) = satp[63 .. 60];
+                match satp64Mode_of_bits(RV64, mbits) {    // see riscv_types.sail
+                  Some(m) => m,
+                  None()  => internal_error(__FILE__, __LINE__,
+                                            "invalid RV64 translation mode in satp")
+                }
+              },
+      RV32 => match Mk_Satp32(satp[31 .. 0])[Mode] {    // Note: satp is 64bits here
+                // When xlen is 64, mstatus.SXL (for S privilege) can be RV32
+                0b0 => Sbare,
+                0b1  => Sv32
+              },
       _    => internal_error(__FILE__, __LINE__, "unsupported address translation arch")
     }
   }