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 Sep 12, 2024
1 parent 9063a2b commit 31f8093
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 @@ -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

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 31f8093

Please sign in to comment.