Skip to content

Commit

Permalink
Derive xlen values from a logarithmic constant
Browse files Browse the repository at this point in the history
The motivation for this is that it makes deriving CHERI constants (field widths etc.) which vary between RV32 and RV64 a lot easier.
  • Loading branch information
Timmmm committed Aug 29, 2024
1 parent 05b845c commit 707a202
Show file tree
Hide file tree
Showing 4 changed files with 20 additions and 10 deletions.
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
11 changes: 11 additions & 0 deletions model/riscv_xlen.sail
Original file line number Diff line number Diff line change
@@ -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)
9 changes: 4 additions & 5 deletions model/riscv_xlen32.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
9 changes: 4 additions & 5 deletions model/riscv_xlen64.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 707a202

Please sign in to comment.