Derive xlen values from a logarithmic constant

The motivation for this is that it makes deriving CHERI constants (field widths etc.) which vary between RV32 and RV64 a lot easier.

Makefile

@@ -17,6 +17,7 @@ else ifeq ($(ARCH),RV64)
 else
   $(error '$(ARCH)' is not a valid architecture, must be one of: RV32, RV64)
 endif
+SAIL_XLEN += riscv_xlen.sail
 
 SAIL_FLEN := riscv_flen_D.sail
 SAIL_VLEN := riscv_vlen.sail

model/riscv_xlen.sail

@@ -0,0 +1,11 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+type xlen_bytes : Int = 2 ^ log2_xlen_bytes
+type xlen       : Int = xlen_bytes * 8
+type xlenbits         = bits(xlen)

model/riscv_xlen32.sail

@@ -6,8 +6,7 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-/* Define the XLEN value for the architecture. */
-
-type xlen       : Int = 32
-type xlen_bytes : Int = 4
-type xlenbits         = bits(xlen)
+// Define the XLEN value for the architecture.
+// This is done using the smallest/most logarithmic possible value since Sail's
+// type system works well for multiply and 2^ but not divide and log2.
+type log2_xlen_bytes : Int = 2

model/riscv_xlen64.sail

@@ -6,8 +6,7 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-/* Define the XLEN value for the architecture. */
-
-type xlen       : Int = 64
-type xlen_bytes : Int = 8
-type xlenbits         = bits(xlen)
+// Define the XLEN value for the architecture.
+// This is done using the smallest/most logarithmic possible value since Sail's
+// type system works well for multiply and 2^ but not divide and log2.
+type log2_xlen_bytes : Int = 3