Use sizeof xlen instead of the value definitions of xlen.

14 files changed, 135 insertions, 143 deletions

diff --git a/model/main.sail b/model/main.sail
index 5a6dba1..c454c46 100644
--- a/model/main.sail
+++ b/model/main.sail
@@ -13,7 +13,7 @@ val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wre
 function main () = {
 
   // PC = __GetSlice_int(64, elf_entry(), 0);
-  PC = zero_extend(0x1000, xlen);
+  PC = zero_extend(0x1000, sizeof(xlen));
   print_bits("PC = ", PC);
   try {
     init_platform();
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 8593db1..8e483f8 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, 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),
+    (false, false, false) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data),
+    (false, true,  false) => __WriteRAM_release(sizeof(xlen), width, EXTZ(0x0), addr, data),
+    (false, false, true)  => __WriteRAM_conditional(sizeof(xlen), width, EXTZ(0x0), addr, data),
+    (false, true,  true)  => __WriteRAM_conditional_release(sizeof(xlen), width, EXTZ(0x0), addr, data),
+    (true,  true,  false) => __WriteRAM_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data),
+    (true,  true,  true)  => __WriteRAM_conditional_strong_release(sizeof(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, 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, false, false) => Some(__ReadRAM(sizeof(xlen), width, EXTZ(0x0), addr)),
+    (true,  false, false) => Some(__ReadRAM_acquire(sizeof(xlen), width, EXTZ(0x0), addr)),
+    (true,  true,  false) => Some(__ReadRAM_strong_acquire(sizeof(xlen), width, EXTZ(0x0), addr)),
+    (false, false, true)  => Some(__ReadRAM_reserved(sizeof(xlen), width, EXTZ(0x0), addr)),
+    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(sizeof(xlen), width, EXTZ(0x0), addr)),
+    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(sizeof(xlen), width, EXTZ(0x0), addr)),
     (false, true,  false) => None(),
     (false, true,  true)  => None()
   }
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 202dac2..c1ddebd 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -60,7 +60,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
     else match translateAddr(vaddr, Read, Data) {
            TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
            TR_Address(addr) =>
-             match (width, xlen) {
+             match (width, sizeof(xlen)) {
                (WORD, _)    => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
                (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
                _            => internal_error("LOADRES expected WORD or DOUBLE")
@@ -114,7 +114,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
           match translateAddr(vaddr, Write, Data) {
             TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
             TR_Address(addr) => {
-              let eares : MemoryOpResult(unit) = match (width, xlen) {
+              let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
                 (WORD, _)    => mem_write_ea(addr, 4, aq, rl, true),
                 (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true),
                 _            => internal_error("STORECON expected word or double")
@@ -123,7 +123,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
                 MemException(e) => { handle_mem_exception(addr, e); false },
                 MemValue(_) => {
                   rs2_val = X(rs2);
-                  let res : MemoryOpResult(bool) = match (width, xlen) {
+                  let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
                     (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
                     (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
                     _            => internal_error("STORECON expected word or double")
@@ -175,7 +175,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     match translateAddr(vaddr, ReadWrite, Data) {
       TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) => {
-        let eares : MemoryOpResult(unit) = match (width, xlen) {
+        let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
           (WORD, _)    => mem_write_ea(addr, 4, aq & rl, rl, true),
           (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
           _            => internal_error ("AMO expected WORD or DOUBLE")
@@ -184,7 +184,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
         match (eares) {
           MemException(e) => { handle_mem_exception(addr, e); false },
           MemValue(_) => {
-            let rval : MemoryOpResult(xlenbits) = match (width, xlen) {
+            let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
               (WORD, _)    => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
               (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
               _            => internal_error ("AMO expected WORD or DOUBLE")
@@ -203,13 +203,13 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                     /* These operations convert bitvectors to integer values using [un]signed,
                      * and back using to_bits().
                      */
-                    AMOMIN  => to_bits(xlen, min(signed(rs2_val),   signed(loaded))),
-                    AMOMAX  => to_bits(xlen, max(signed(rs2_val),   signed(loaded))),
-                    AMOMINU => to_bits(xlen, min(unsigned(rs2_val), unsigned(loaded))),
-                    AMOMAXU => to_bits(xlen, max(unsigned(rs2_val), unsigned(loaded)))
+                    AMOMIN  => to_bits(sizeof(xlen), min(signed(rs2_val),   signed(loaded))),
+                    AMOMAX  => to_bits(sizeof(xlen), max(signed(rs2_val),   signed(loaded))),
+                    AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
+                    AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
                   };
 
-                let wval : MemoryOpResult(bool) = match (width, xlen) {
+                let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
                   (WORD, _)    => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
                   (DOUBLE, 64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
                   _            => internal_error("AMO expected WORD or DOUBLE")
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index f570fb2..c612039 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -179,16 +179,16 @@ mapping encdec_sop : sop <-> bits(3) = {
   RISCV_SRAI <-> 0b101
 }
 
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == false
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == false
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == false
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
 
 function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = {
   let rs1_val = X(rs1);
   let result : xlenbits = match op {
     RISCV_SLLI => rs1_val << shamt,
     RISCV_SRLI => rs1_val >> shamt,
-    RISCV_SRAI => if   xlen == 32
+    RISCV_SRAI => if   sizeof(xlen) == 32
                        /* the decoder guard should ensure that shamt[5] = 0 for RV32 */
                   then shift_right_arith32(rs1_val, shamt[4..0])
                   else shift_right_arith64(rs1_val, shamt)
@@ -233,7 +233,7 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
     RISCV_SLL  => rs1_val << (rs2_val[5..0]),
     RISCV_SRL  => rs1_val >> (rs2_val[5..0]),
     RISCV_SUB  => rs1_val - rs2_val,
-    RISCV_SRA  => if   xlen == 32
+    RISCV_SRA  => if   sizeof(xlen) == 32
                   then shift_right_arith32(rs1_val, rs2_val[4..0])
                   else shift_right_arith64(rs1_val, rs2_val[5..0])
   };
@@ -294,7 +294,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   else match translateAddr(vaddr, Read, Data) {
     TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
     TR_Address(addr) =>
-      match (width, xlen) {
+      match (width, sizeof(xlen)) {
         (BYTE, _)   =>
 	  process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
         (HALF, _)   =>
@@ -354,7 +354,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
         MemException(e) => { handle_mem_exception(addr, e); false },
         MemValue(_) => {
           let rs2_val = X(rs2);
-          let res : MemoryOpResult(bool) = match (width, xlen) {
+          let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
             (BYTE, _)    => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
             (HALF, _)    => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
             (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
@@ -378,9 +378,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 == 64
+      if sizeof(xlen) == 64
   <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 function clause execute (ADDIW(imm, rs1, rd)) = {
   let result : xlenbits = EXTS(imm) + X(rs1);
@@ -389,25 +389,25 @@ function clause execute (ADDIW(imm, rs1, rd)) = {
 }
 
 mapping clause assembly = ADDIW(imm, rs1, rd)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)
 
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 function clause execute (SHIFTW(shamt, rs1, rd, op)) = {
   let rs1_val = (X(rs1))[31..0];
@@ -427,33 +427,33 @@ mapping shiftw_mnemonic : sop <-> string = {
 }
 
 mapping clause assembly = SHIFTW(shamt, rs1, rd, op)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)
 
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
   let rs1_val = (X(rs1))[31..0];
@@ -478,25 +478,25 @@ mapping rtypew_mnemonic : ropw <-> string = {
 }
 
 mapping clause assembly = RTYPEW(rs2, rs1, rd, op)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw)
 
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
   let rs1_val = X(rs1);
@@ -516,9 +516,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = {
 }
 
 mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_5(shamt)
-      if xlen == 64
+      if sizeof(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 3423f8e..70d4978 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 == 64
+      if sizeof(xlen) == 64
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000)
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000)
-      if xlen == 64
+      if sizeof(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 == 32
+      if sizeof(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 == 32
+      if sizeof(xlen) == 32
 
 function clause execute (C_JAL(imm)) =
   execute(RISCV_JAL(EXTS(imm @ 0b0), ra))
 
 mapping clause assembly = C_JAL(imm)
-      if xlen == 32
+      if sizeof(xlen) == 32
   <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0)
-      if xlen == 32
+      if sizeof(xlen) == 32
 
 /* ****************************************************************** */
 union clause ast = C_ADDIW : (bits(6), regbits)
 
 mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
-      if rsd != zreg & xlen == 64
+      if rsd != zreg & sizeof(xlen) == 64
   <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
-      if rsd != zreg & xlen == 64
+      if rsd != zreg & sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm)
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = C_ADDW : (cregbits, cregbits)
 
 /* TODO: invalid on RV32 */
 mapping clause encdec_compressed = C_ADDW(rsd, rs2)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
-      if xlen == 64
+      if sizeof(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 == 64
+      if rd != zreg & sizeof(xlen) == 64
   <-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if rd != zreg & xlen == 64
+      if rd != zreg & sizeof(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 == 64
+      if rd != zreg & sizeof(xlen) == 64
   <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm)
-      if rd != zreg & xlen == 64
+      if rd != zreg & sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = C_JR : (regbits)
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index 371966f..cab8d9c 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, rs1_int * rs2_int);
+    let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int);
     let result = if   high
-                 then result_wide[(2 * xlen - 1) .. xlen]
-                 else result_wide[(xlen - 1) .. 0];
+                 then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)]
+                 else result_wide[(sizeof(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, q');
+    X(rd) = to_bits(sizeof(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, r);
+    X(rd) = to_bits(sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = DIVW : (regbits, regbits, regbits, bool)
 
 mapping clause encdec = DIVW(rs2, rs1, rd, s)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen == 64
+      if sizeof(xlen) == 64
 
 /* ****************************************************************** */
 union clause ast = REMW : (regbits, regbits, regbits, bool)
 
 mapping clause encdec = REMW(rs2, rs1, rd, s)
-      if xlen == 64
+      if sizeof(xlen) == 64
   <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
-      if xlen == 64
+      if sizeof(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 == 64
+      if sizeof(xlen) == 64
   <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
-      if xlen == 64
+      if sizeof(xlen) == 64
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 521cf0c..749f20c 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -15,7 +15,7 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
 
 function readCSR csr : csreg -> xlenbits = {
   let res : xlenbits =
-  match (csr, xlen) {
+  match (csr, sizeof(xlen)) {
     /* machine mode */
     (0xF11,  _) => EXTZ(mvendorid),
     (0xF12,  _) => marchid,
@@ -38,8 +38,8 @@ function readCSR csr : csreg -> xlenbits = {
     (0x3B0,  _) => pmpaddr0,
 
     /* machine mode counters */
-    (0xB00,  _) => mcycle[(xlen - 1) .. 0],
-    (0xB02,  _) => minstret[(xlen - 1) .. 0],
+    (0xB00,  _) => mcycle[(sizeof(xlen) - 1) .. 0],
+    (0xB02,  _) => minstret[(sizeof(xlen) - 1) .. 0],
     (0xB80, 32) => mcycle[63 .. 32],
     (0xB82, 32) => minstret[63 .. 32],
 
@@ -61,9 +61,9 @@ function readCSR csr : csreg -> xlenbits = {
     (0x180,  _) => satp,
 
     /* user mode counters */
-    (0xC00,  _) => mcycle[(xlen - 1) .. 0],
-    (0xC01,  _) => mtime[(xlen - 1) .. 0],
-    (0xC02,  _) => minstret[(xlen - 1) .. 0],
+    (0xC00,  _) => mcycle[(sizeof(xlen) - 1) .. 0],
+    (0xC01,  _) => mtime[(sizeof(xlen) - 1) .. 0],
+    (0xC02,  _) => minstret[(sizeof(xlen) - 1) .. 0],
     (0xC80, 32) => mcycle[63 .. 32],
     (0xC81, 32) => mtime[63 .. 32],
     (0xC82, 32) => minstret[63 .. 32],
@@ -81,7 +81,7 @@ function readCSR csr : csreg -> xlenbits = {
 
 function writeCSR (csr : csreg, value : xlenbits) -> unit = {
   let res : option(xlenbits) =
-  match (csr, xlen) {
+  match (csr, sizeof(xlen)) {
     /* machine mode */
     (0x300,  _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) },
     (0x301,  _) => { misa = legalize_misa(misa, value); Some(misa.bits()) },
@@ -100,8 +100,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x3B0,  _) => { pmpaddr0 = value; Some(pmpaddr0) }, /* FIXME: legalize */
 
     /* machine mode counters */
-    (0xB00,  _) => { mcycle[(xlen - 1) .. 0] = value; Some(value) },
-    (0xB02,  _) => { minstret[(xlen - 1) .. 0] = value; minstret_written = true; Some(value) },
+    (0xB00,  _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB02,  _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_written = true; Some(value) },
     (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) },
     (0xB82, 32) => { minstret[63 .. 32] = value; minstret_written = true; Some(value) },
 
diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail
index 333f385..cd8174e 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 - 1) .. 1] @ 0b0;
+  nextPC = newPC[(sizeof(xlen) - 1) .. 1] @ 0b0;
   true
 }
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 3dcae61..25b9dbb 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 - 1) .. 1] @ 0b0;
+  let newPC : xlenbits = (X(rs1) + EXTS(imm))[(sizeof(xlen) - 1) .. 1] @ 0b0;
   if newPC[1] & (~ (haveRVC())) then {
     handle_mem_exception(newPC, E_Fetch_Addr_Align);
     false;
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 5238066..8a0e1cf 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -36,8 +36,8 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool =
     0xB00 => p == Machine, // mcycle
     0xB02 => p == Machine, // minstret
 
-    0xB80 => p == Machine & (xlen == 32), // mcycleh
-    0xB82 => p == Machine & (xlen == 32), // minstreth
+    0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh
+    0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth
 
     /* disabled trigger/debug module */
     0x7a0 => p == Machine,
@@ -65,9 +65,9 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool =
     0xC01 => p == User,    // time
     0xC02 => p == User,    // instret
 
-    0xC80 => p == User & (xlen == 32),     // cycleh
-    0xC81 => p == User & (xlen == 32),     // timeh
-    0xC82 => p == User & (xlen == 32),     // instreth
+    0xC80 => p == User & (sizeof(xlen) == 32),     // cycleh
+    0xC81 => p == User & (sizeof(xlen) == 32),     // timeh
+    0xC82 => p == User & (sizeof(xlen) == 32),     // instreth
 
     /* check extensions */
     _     => is_UExt_CSR_defined(csr, p)   // 'N' extension
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 36ef0bd..439d12d 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   xlen == 32
+  if   sizeof(xlen) == 32
   then arch_to_bits(RV32)
   else m.bits()[35 .. 34]
 }
 
 function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
-  if   xlen == 32
+  if   sizeof(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   xlen == 32
+  if   sizeof(xlen) == 32
   then arch_to_bits(RV32)
   else m.bits()[33 .. 32]
 }
 
 function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
-  if   xlen == 32
+  if   sizeof(xlen) == 32
   then m
   else {
     let m = vector_update_subrange(m.bits(), 33, 32,  a);
@@ -284,7 +284,7 @@ function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = {
 
 bitfield Mtvec : xlenbits = {
   Base : xlen - 1 .. 2,
-  Mode :  1 .. 0
+  Mode : 1 .. 0
 }
 register mtvec : Mtvec  /* Trap Vector */
 
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index c0e538f..8e8e163 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 - 1
-let xlen_max_signed = 2 ^ (xlen - 1) - 1
-let xlen_min_signed = 0 - 2 ^ (xlen - 1)
+let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1
+let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1
+let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1)
 
 type half = bits(16)
 type word = bits(32)
diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail
index de7cf74..e35ce57 100644
--- a/model/riscv_xlen32.sail
+++ b/model/riscv_xlen32.sail
@@ -4,7 +4,3 @@
 type xlen       : Int = 32
 type xlen_bytes : Int = 4
 type xlenbits         = bits(xlen)
-
-// value-level definitions
-let xlen : int(xlen) = 32
-let xlen_bytes       = 4     // byte-width of xlen bits
diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail
index 9130ec4..7b5e14a 100644
--- a/model/riscv_xlen64.sail
+++ b/model/riscv_xlen64.sail
@@ -4,7 +4,3 @@
 type xlen       : Int = 64
 type xlen_bytes : Int = 8
 type xlenbits         = bits(xlen)
-
-// value-level definitions
-let xlen : int(xlen)  = 64
-let xlen_bytes        = 8    // byte-width of xlen bits