From 31f809346e1020d191b46d519ad6435e2428be39 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Thu, 12 Sep 2024 20:53:07 +0100 Subject: [PATCH] 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 | 1 + model/riscv_xlen.sail | 11 +++++++++++ model/riscv_xlen32.sail | 9 ++++----- model/riscv_xlen64.sail | 9 ++++----- 4 files changed, 20 insertions(+), 10 deletions(-) create mode 100644 model/riscv_xlen.sail diff --git a/Makefile b/Makefile index 53459bd28..f19b6d591 100644 --- a/Makefile +++ b/Makefile @@ -18,6 +18,7 @@ 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 diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail new file mode 100644 index 000000000..75174fc8e --- /dev/null +++ b/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) diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail index fb883acdc..926f20f74 100644 --- a/model/riscv_xlen32.sail +++ b/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 diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail index 7a9030759..9878c7ffa 100644 --- a/model/riscv_xlen64.sail +++ b/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