Fix xlen variable name.

13 files changed, 114 insertions, 114 deletions

diff --git a/Makefile b/Makefile
index d3806fa..d4bf887 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@ SAIL_SYS_SRCS = riscv_csr_map.sail riscv_sys_regs.sail riscv_next_regs.sail risc
 # non-instruction sources
 PRELUDE = prelude.sail prelude_mapping.sail riscv_xlen.sail prelude_mem.sail
 SAIL_OTHER_SRCS = $(PRELUDE) riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail
-SAIL_OTHER_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_xlen.sail riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail
+SAIL_OTHER_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail
 
 PRELUDE_SRCS   = $(addprefix model/,$(PRELUDE))
 SAIL_SRCS      = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail)
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 532d0fd..8593db1 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -23,12 +23,12 @@ val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_relea
 val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
 function __RISCV_write (addr, width, data, aq, rl, con) =
   match (aq, rl, con) {
-    (false, false, false) => __WriteRAM(xlen_val, width, EXTZ(0x0), addr, data),
-    (false, true,  false) => __WriteRAM_release(xlen_val, width, EXTZ(0x0), addr, data),
-    (false, false, true)  => __WriteRAM_conditional(xlen_val, width, EXTZ(0x0), addr, data),
-    (false, true,  true)  => __WriteRAM_conditional_release(xlen_val, width, EXTZ(0x0), addr, data),
-    (true,  true,  false) => __WriteRAM_strong_release(xlen_val, width, EXTZ(0x0), addr, data),
-    (true,  true,  true)  => __WriteRAM_conditional_strong_release(xlen_val, width, EXTZ(0x0), addr, data),
+    (false, false, false) => __WriteRAM(xlen, width, EXTZ(0x0), addr, data),
+    (false, true,  false) => __WriteRAM_release(xlen, width, EXTZ(0x0), addr, data),
+    (false, false, true)  => __WriteRAM_conditional(xlen, width, EXTZ(0x0), addr, data),
+    (false, true,  true)  => __WriteRAM_conditional_release(xlen, width, EXTZ(0x0), addr, data),
+    (true,  true,  false) => __WriteRAM_strong_release(xlen, width, EXTZ(0x0), addr, data),
+    (true,  true,  true)  => __WriteRAM_conditional_strong_release(xlen, width, EXTZ(0x0), addr, data),
     (true,  false, false) => false,
     (true,  false, true)  => false
   }
@@ -57,12 +57,12 @@ val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _
 val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
 function __RISCV_read (addr, width, aq, rl, res) =
   match (aq, rl, res) {
-    (false, false, false) => Some(__ReadRAM(xlen_val, width, EXTZ(0x0), addr)),
-    (true,  false, false) => Some(__ReadRAM_acquire(xlen_val, width, EXTZ(0x0), addr)),
-    (true,  true,  false) => Some(__ReadRAM_strong_acquire(xlen_val, width, EXTZ(0x0), addr)),
-    (false, false, true)  => Some(__ReadRAM_reserved(xlen_val, width, EXTZ(0x0), addr)),
-    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(xlen_val, width, EXTZ(0x0), addr)),
-    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(xlen_val, width, EXTZ(0x0), addr)),
+    (false, false, false) => Some(__ReadRAM(xlen, width, EXTZ(0x0), addr)),
+    (true,  false, false) => Some(__ReadRAM_acquire(xlen, width, EXTZ(0x0), addr)),
+    (true,  true,  false) => Some(__ReadRAM_strong_acquire(xlen, width, EXTZ(0x0), addr)),
+    (false, false, true)  => Some(__ReadRAM_reserved(xlen, width, EXTZ(0x0), addr)),
+    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(xlen, width, EXTZ(0x0), addr)),
+    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(xlen, width, EXTZ(0x0), addr)),
     (false, true,  false) => None(),
     (false, true,  true)  => None()
   }
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail
index c68a5a5..99dbbba 100644
--- a/model/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
@@ -73,7 +73,7 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0
 
 function clause execute(LOAD(imm, rs1, rd)) =
     let addr : xlenbits = X(rs1) + EXTS(imm) in
-    let result : xlenbits = MEMr(addr, xlen_val_bytes) in
+    let result : xlenbits = MEMr(addr, xlen_bytes) in
     X(rd) = result
 
 /* ****************************************************************** */
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index f54e078..bfd6551 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -373,9 +373,9 @@ mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl)
 union clause ast = ADDIW : (bits(12), regbits, regbits)
 
 mapping clause encdec = ADDIW(imm, rs1, rd)
-      if xlen_val == 64
+      if xlen == 64
   <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (ADDIW(imm, rs1, rd)) = {
   let result : xlenbits = EXTS(imm) + X(rs1);
@@ -384,25 +384,25 @@ function clause execute (ADDIW(imm, rs1, rd)) = {
 }
 
 mapping clause assembly = ADDIW(imm, rs1, rd)
-      if xlen_val == 64
+      if xlen == 64
   <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)
 
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (SHIFTW(shamt, rs1, rd, op)) = {
   let rs1_val = (X(rs1))[31..0];
@@ -422,33 +422,33 @@ mapping shiftw_mnemonic : sop <-> string = {
 }
 
 mapping clause assembly = SHIFTW(shamt, rs1, rd, op)
-      if xlen_val == 64
+      if xlen == 64
   <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)
 
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
   let rs1_val = (X(rs1))[31..0];
@@ -473,25 +473,25 @@ mapping rtypew_mnemonic : ropw <-> string = {
 }
 
 mapping clause assembly = RTYPEW(rs2, rs1, rd, op)
-      if xlen_val == 64
+      if xlen == 64
   <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw)
 
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
   let rs1_val = X(rs1);
@@ -511,9 +511,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = {
 }
 
 mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op)
-      if xlen_val == 64
+      if xlen == 64
   <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_5(shamt)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = FENCE : (bits(4), bits(4))
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index d2b0695..3423f8e 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -56,9 +56,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc)
 union clause ast = C_LD : (bits(5), cregbits, cregbits)
 
 mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (C_LD(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -68,9 +68,9 @@ function clause execute (C_LD(uimm, rsc, rdc)) = {
 }
 
 mapping clause assembly = C_LD(uimm, rsc, rdc)
-      if xlen_val == 64
+      if xlen == 64
   <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_SW : (bits(5), cregbits, cregbits)
@@ -92,9 +92,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2)
 union clause ast = C_SD : (bits(5), cregbits, cregbits)
 
 mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (C_SD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -104,9 +104,9 @@ function clause execute (C_SD(uimm, rsc1, rsc2)) = {
 }
 
 mapping clause assembly = C_SD(uimm, rsc1, rsc2)
-      if xlen_val == 64
+      if xlen == 64
   <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_ADDI : (bits(6), regbits)
@@ -130,25 +130,25 @@ mapping clause assembly = C_ADDI(nzi, rsd)
 union clause ast = C_JAL : (bits(11))
 
 mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31)
-      if xlen_val == 32
+      if xlen == 32
   <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01
-      if xlen_val == 32
+      if xlen == 32
 
 function clause execute (C_JAL(imm)) =
   execute(RISCV_JAL(EXTS(imm @ 0b0), ra))
 
 mapping clause assembly = C_JAL(imm)
-      if xlen_val == 32
+      if xlen == 32
   <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0)
-      if xlen_val == 32
+      if xlen == 32
 
 /* ****************************************************************** */
 union clause ast = C_ADDIW : (bits(6), regbits)
 
 mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
-      if rsd != zreg & xlen_val == 64
+      if rsd != zreg & xlen == 64
   <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
-      if rsd != zreg & xlen_val == 64
+      if rsd != zreg & xlen == 64
 
 function clause execute (C_ADDIW(imm, rsd)) = {
   let imm : bits(32) = EXTS(imm);
@@ -159,9 +159,9 @@ function clause execute (C_ADDIW(imm, rsd)) = {
 }
 
 mapping clause assembly = C_ADDIW(imm, rsd)
-      if xlen_val == 64
+      if xlen == 64
   <-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_LI : (bits(6), regbits)
@@ -332,9 +332,9 @@ union clause ast = C_SUBW : (cregbits, cregbits)
 
 /* TODO: invalid on RV32 */
 mapping clause encdec_compressed = C_SUBW(rsd, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (C_SUBW(rsd, rs2)) = {
   let rsd = creg2reg_bits(rsd);
@@ -343,18 +343,18 @@ function clause execute (C_SUBW(rsd, rs2)) = {
 }
 
 mapping clause assembly = C_SUBW(rsd, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_ADDW : (cregbits, cregbits)
 
 /* TODO: invalid on RV32 */
 mapping clause encdec_compressed = C_ADDW(rsd, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (C_ADDW(rsd, rs2)) = {
   let rsd = creg2reg_bits(rsd);
@@ -363,9 +363,9 @@ function clause execute (C_ADDW(rsd, rs2)) = {
 }
 
 mapping clause assembly = C_ADDW(rsd, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_J : (bits(11))
@@ -436,9 +436,9 @@ mapping clause assembly = C_LWSP(uimm, rd)
 union clause ast = C_LDSP : (bits(6), regbits)
 
 mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd)
-      if rd != zreg & xlen_val == 64
+      if rd != zreg & xlen == 64
   <-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if rd != zreg & xlen_val == 64
+      if rd != zreg & xlen == 64
 
 function clause execute (C_LDSP(uimm, rd)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -446,9 +446,9 @@ function clause execute (C_LDSP(uimm, rd)) = {
 }
 
 mapping clause assembly = C_LDSP(uimm, rd)
-      if rd != zreg & xlen_val == 64
+      if rd != zreg & xlen == 64
   <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm)
-      if rd != zreg & xlen_val == 64
+      if rd != zreg & xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_SWSP : (bits(6), regbits)
@@ -468,9 +468,9 @@ mapping clause assembly = C_SWSP(uimm, rd)
 union clause ast = C_SDSP : (bits(6), regbits)
 
 mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (C_SDSP(uimm, rs2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -478,9 +478,9 @@ function clause execute (C_SDSP(uimm, rs2)) = {
 }
 
 mapping clause assembly = C_SDSP(uimm, rs2)
-      if xlen_val == 64
+      if xlen == 64
   <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = C_JR : (regbits)
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index c4ca7e5..371966f 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -22,10 +22,10 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
     let rs2_val = X(rs2);
     let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val);
     let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val);
-    let result_wide = to_bits(2 * xlen_val, rs1_int * rs2_int);
+    let result_wide = to_bits(2 * xlen, rs1_int * rs2_int);
     let result = if   high
-                 then result_wide[(2 * xlen_val - 1) .. xlen_val]
-                 else result_wide[(xlen_val - 1) .. 0];
+                 then result_wide[(2 * xlen - 1) .. xlen]
+                 else result_wide[(xlen - 1) .. 0];
     X(rd) = result;
     true
   } else {
@@ -59,7 +59,7 @@ function clause execute (DIV(rs2, rs1, rd, s)) = {
     let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int);
     /* check for signed overflow */
     let q': int = if s & q > xlen_max_signed then xlen_min_signed else q;
-    X(rd) = to_bits(xlen_val, q');
+    X(rd) = to_bits(xlen, q');
     true
   } else {
     handle_illegal();
@@ -89,7 +89,7 @@ function clause execute (REM(rs2, rs1, rd, s)) = {
     let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
     let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
     /* signed overflow case returns zero naturally as required due to -1 divisor */
-    X(rd) = to_bits(xlen_val, r);
+    X(rd) = to_bits(xlen, r);
     true
   } else {
     handle_illegal();
@@ -104,9 +104,9 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
 union clause ast = MULW : (regbits, regbits, regbits)
 
 mapping clause encdec = MULW(rs2, rs1, rd)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (MULW(rs2, rs1, rd)) = {
   if haveMulDiv() then {
@@ -126,17 +126,17 @@ function clause execute (MULW(rs2, rs1, rd)) = {
 }
 
 mapping clause assembly = MULW(rs2, rs1, rd)
-      if xlen_val == 64
+      if xlen == 64
   <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = DIVW : (regbits, regbits, regbits, bool)
 
 mapping clause encdec = DIVW(rs2, rs1, rd, s)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (DIVW(rs2, rs1, rd, s)) = {
   if haveMulDiv() then {
@@ -156,17 +156,17 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = {
 }
 
 mapping clause assembly = DIVW(rs2, rs1, rd, s)
-      if xlen_val == 64
+      if xlen == 64
   <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen_val == 64
+      if xlen == 64
 
 /* ****************************************************************** */
 union clause ast = REMW : (regbits, regbits, regbits, bool)
 
 mapping clause encdec = REMW(rs2, rs1, rd, s)
-      if xlen_val == 64
+      if xlen == 64
   <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
-      if xlen_val == 64
+      if xlen == 64
 
 function clause execute (REMW(rs2, rs1, rd, s)) = {
   if haveMulDiv() then {
@@ -185,6 +185,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = {
 }
 
 mapping clause assembly = REMW(rs2, rs1, rd, s)
-      if xlen_val == 64
+      if xlen == 64
   <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen_val == 64
+      if xlen == 64
diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail
index 3069582..333f385 100644
--- a/model/riscv_jalr_rmem.sail
+++ b/model/riscv_jalr_rmem.sail
@@ -5,6 +5,6 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
   /* write rd before anything else to prevent unintended strength */
   X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
   let newPC : xlenbits = X(rs1) + EXTS(imm);
-  nextPC = newPC[(xlen_val - 1) .. 1] @ 0b0;
+  nextPC = newPC[(xlen - 1) .. 1] @ 0b0;
   true
 }
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index d4982c6..3dcae61 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -7,7 +7,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
    some manner, but for now, we just keep a reordered definition to improve simulator
    performance.
 */
-  let newPC : xlenbits = (X(rs1) + EXTS(imm))[(xlen_val) - 1 .. 1] @ 0b0;
+  let newPC : xlenbits = (X(rs1) + EXTS(imm))[(xlen - 1) .. 1] @ 0b0;
   if newPC[1] & (~ (haveRVC())) then {
     handle_mem_exception(newPC, E_Fetch_Addr_Align);
     false;
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 25739fc..c43ab52 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -117,12 +117,12 @@ function clint_load(addr, width) = {
   else if addr == MTIMECMP_BASE & ('n == 8)
   then {
     print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
-    MemValue(zero_extend(mtimecmp, xlen_val)) /* FIXME: Redundant zero_extend currently required by Lem backend */
+    MemValue(zero_extend(mtimecmp, xlen)) /* FIXME: Redundant zero_extend currently required by Lem backend */
   }
   else if addr == MTIME_BASE & ('n == 8)
   then {
     print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
-    MemValue(zero_extend(mtime, xlen_val))
+    MemValue(zero_extend(mtime, xlen))
   }
   else {
     print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
@@ -150,7 +150,7 @@ function clint_store(addr, width, data) = {
     MemValue(true)
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
     print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
-    mtimecmp = zero_extend(data, xlen_val); /* FIXME: Redundant zero_extend currently required by Lem backend */
+    mtimecmp = zero_extend(data, xlen); /* FIXME: Redundant zero_extend currently required by Lem backend */
     clint_dispatch();
     MemValue(true)
   } else {
@@ -194,7 +194,7 @@ function htif_load(addr, width) = {
   print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost));
   /* FIXME: For now, only allow the expected access widths. */
   if width == 8
-  then MemValue(zero_extend(htif_tohost, xlen_val))  /* FIXME: Redundant zero_extend currently required by Lem backend */
+  then MemValue(zero_extend(htif_tohost, xlen))  /* FIXME: Redundant zero_extend currently required by Lem backend */
   else MemException(E_Load_Access_Fault)
 }
 
@@ -213,7 +213,7 @@ function htif_store(addr, width, data) = {
       if cmd.payload()[0] == 0b1
       then {
            htif_done = true;
-           htif_exit_code = (zero_extend(cmd.payload(), xlen_val) >> 0b01) : xlenbits
+           htif_exit_code = (zero_extend(cmd.payload(), xlen) >> 0b01) : xlenbits
       }
       else ()
     },
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 03f5520..46a2f77 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -120,13 +120,13 @@ bitfield Mstatus : xlenbits = {
 register mstatus : Mstatus
 
 function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
-  if   sizeof(xlen) == 32
+  if   xlen == 32
   then arch_to_bits(RV32)
   else m.bits()[35 .. 34]
 }
 
 function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
-  if   sizeof(xlen) == 32
+  if   xlen == 32
   then m
   else {
     let m = vector_update_subrange(m.bits(), 35, 34,  a);
@@ -135,13 +135,13 @@ function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
 }
 
 function get_mstatus_UXL(m : Mstatus) -> arch_xlen = {
-  if   sizeof(xlen) == 32
+  if   xlen == 32
   then arch_to_bits(RV32)
   else m.bits()[33 .. 32]
 }
 
 function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
-  if   sizeof(xlen) == 32
+  if   xlen == 32
   then m
   else {
     let m = vector_update_subrange(mstatus.bits(), 33, 32,  a);
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 94ca69b..e081e68 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -1,8 +1,8 @@
 /* Basic type and function definitions used pervasively in the model. */
 
-let xlen_max_unsigned = 2 ^ xlen_val - 1
-let xlen_max_signed = 2 ^ (xlen_val - 1) - 1
-let xlen_min_signed = 0 - 2 ^ (xlen_val - 1)
+let xlen_max_unsigned = 2 ^ xlen - 1
+let xlen_max_signed = 2 ^ (xlen - 1) - 1
+let xlen_min_signed = 0 - 2 ^ (xlen - 1)
 
 type half = bits(16)
 type word = bits(32)
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index eb0e957..8a61f1c 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -146,7 +146,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
                                 PTE39_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
   /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */
-  match (phys_mem_read(Data, EXTZ(pte_addr), xlen_val_bytes, false, false, false)) {
+  match (phys_mem_read(Data, EXTZ(pte_addr), xlen_bytes, false, false, false)) {
     MemException(_) => {
 /*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)
@@ -313,7 +313,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
               n_ent.pte = update_BITS(ent.pte, pbits.bits());
               writeTLB39(idx, n_ent);
               /* update page table */
-              match checked_mem_write(EXTZ(ent.pteAddr), xlen_val_bytes, ent.pte.bits(), false, false, false) {
+              match checked_mem_write(EXTZ(ent.pteAddr), xlen_bytes, ent.pte.bits(), false, false, false) {
                 MemValue(_) => (),
                 MemException(e) => internal_error("invalid physical address in TLB")
               };
@@ -339,7 +339,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
                 TR39_Failure(PTW_PTE_Update)
               } else {
                 w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
-                match checked_mem_write(EXTZ(pteAddr), xlen_val_bytes, w_pte.bits(), false, false, false) {
+                match checked_mem_write(EXTZ(pteAddr), xlen_bytes, w_pte.bits(), false, false, false) {
                   MemValue(_) => {
                     addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
                     TR39_Address(pAddr)
diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail
index 801aca8..d4b1b53 100644
--- a/model/riscv_xlen.sail
+++ b/model/riscv_xlen.sail
@@ -5,5 +5,5 @@ type xlen : Int = 64
 type xlenbits   = bits(xlen)
 
 // value-level definitions
-let xlen_val       = 64
-let xlen_val_bytes = 8      // byte-width of xlen bits
+let xlen : int(xlen) = 64
+let xlen_bytes       = 8    // byte-width of xlen bits