Skip to content

Commit fcd31da

Browse files
committed
Implement Zicbom, Zicboz (cbo.flush, cbo.inval, cbo.zero)
Note that Zicbop (prefetch hints) does not need to be implemented because all it does is label some existing base instructions as prefetch hints.
1 parent 05b845c commit fcd31da

18 files changed

+308
-2
lines changed

Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail
6060
SAIL_DEFAULT_INST += riscv_insts_vext_fp_vm.sail
6161
SAIL_DEFAULT_INST += riscv_insts_vext_red.sail
6262
SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail
63+
SAIL_DEFAULT_INST += riscv_insts_zicbom.sail
64+
SAIL_DEFAULT_INST += riscv_insts_zicboz.sail
6365

6466
SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
6567
SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail

c_emulator/riscv_platform.c

+15
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,16 @@ bool sys_enable_bext(unit u)
6262
return rv_enable_bext;
6363
}
6464

65+
bool sys_enable_zicbom(unit u)
66+
{
67+
return rv_enable_zicbom;
68+
}
69+
70+
bool sys_enable_zicboz(unit u)
71+
{
72+
return rv_enable_zicboz;
73+
}
74+
6575
uint64_t sys_pmp_count(unit u)
6676
{
6777
return rv_pmp_count;
@@ -112,6 +122,11 @@ mach_bits plat_rom_size(unit u)
112122
return rv_rom_size;
113123
}
114124

125+
mach_bits plat_cache_block_size_exp()
126+
{
127+
return rv_cache_block_size_exp;
128+
}
129+
115130
// Provides entropy for the scalar cryptography extension.
116131
mach_bits plat_get_16_random_bits(unit u)
117132
{

c_emulator/riscv_platform.h

+4
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ bool sys_enable_writable_misa(unit);
1111
bool sys_enable_writable_fiom(unit);
1212
bool sys_enable_vext(unit);
1313
bool sys_enable_bext(unit);
14+
bool sys_enable_zicbom(unit);
15+
bool sys_enable_zicboz(unit);
1416

1517
uint64_t sys_pmp_count(unit);
1618
uint64_t sys_pmp_grain(unit);
@@ -26,6 +28,8 @@ bool within_phys_mem(mach_bits, sail_int);
2628
mach_bits plat_rom_base(unit);
2729
mach_bits plat_rom_size(unit);
2830

31+
mach_bits plat_cache_block_size_exp(unit);
32+
2933
// Provides entropy for the scalar cryptography extension.
3034
mach_bits plat_get_16_random_bits(unit);
3135

c_emulator/riscv_platform_impl.c

+5
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ bool rv_enable_writable_misa = true;
1515
bool rv_enable_fdext = true;
1616
bool rv_enable_vext = true;
1717
bool rv_enable_bext = false;
18+
bool rv_enable_zicbom = false;
19+
bool rv_enable_zicboz = false;
1820

1921
bool rv_enable_dirty_update = false;
2022
bool rv_enable_misaligned = false;
@@ -27,6 +29,9 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
2729
uint64_t rv_rom_base = UINT64_C(0x1000);
2830
uint64_t rv_rom_size = UINT64_C(0x100);
2931

32+
// Default 64, which is mandated by RVA22.
33+
uint64_t rv_cache_block_size_exp = UINT64_C(6);
34+
3035
// Provides entropy for the scalar cryptography extension.
3136
uint64_t rv_16_random_bits(void)
3237
{

c_emulator/riscv_platform_impl.h

+4
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ extern bool rv_enable_next;
1919
extern bool rv_enable_fdext;
2020
extern bool rv_enable_vext;
2121
extern bool rv_enable_bext;
22+
extern bool rv_enable_zicbom;
23+
extern bool rv_enable_zicboz;
2224
extern bool rv_enable_writable_misa;
2325
extern bool rv_enable_dirty_update;
2426
extern bool rv_enable_misaligned;
@@ -31,6 +33,8 @@ extern uint64_t rv_ram_size;
3133
extern uint64_t rv_rom_base;
3234
extern uint64_t rv_rom_size;
3335

36+
extern uint64_t rv_cache_block_size_exp;
37+
3438
// Provides entropy for the scalar cryptography extension.
3539
extern uint64_t rv_16_random_bits(void);
3640

c_emulator/riscv_sim.c

+38
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,9 @@ enum {
5656
OPT_PMP_GRAIN,
5757
OPT_ENABLE_SVINVAL,
5858
OPT_ENABLE_ZCB,
59+
OPT_ENABLE_ZICBOM,
60+
OPT_ENABLE_ZICBOZ,
61+
OPT_CACHE_BLOCK_SIZE,
5962
};
6063

6164
static bool do_dump_dts = false;
@@ -151,6 +154,9 @@ static struct option options[] = {
151154
{"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM},
152155
{"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL },
153156
{"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB },
157+
{"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM },
158+
{"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ },
159+
{"cache-block-size", required_argument, 0, OPT_CACHE_BLOCK_SIZE },
154160
#ifdef SAILCOV
155161
{"sailcov-file", required_argument, 0, 'c' },
156162
#endif
@@ -234,6 +240,17 @@ static void read_dtb(const char *path)
234240
fprintf(stdout, "Read %zd bytes of DTB from %s.\n", dtb_len, path);
235241
}
236242

243+
// Return log2(x), or -1 if x is not a power of 2.
244+
static int ilog2(uint64_t x)
245+
{
246+
for (unsigned i = 0; i < sizeof(x) * 8; ++i) {
247+
if (x == (UINT64_C(1) << i)) {
248+
return i;
249+
}
250+
}
251+
return -1;
252+
}
253+
237254
/**
238255
* Parses the command line arguments and returns the argv index for the first
239256
* ELF file that should be loaded. As getopt transforms the argv array, all
@@ -247,6 +264,7 @@ static int process_args(int argc, char **argv)
247264
uint64_t ram_size = 0;
248265
uint64_t pmp_count = 0;
249266
uint64_t pmp_grain = 0;
267+
uint64_t block_size_exp = 0;
250268
while (true) {
251269
c = getopt_long(argc, argv,
252270
"a"
@@ -401,6 +419,26 @@ static int process_args(int argc, char **argv)
401419
fprintf(stderr, "enabling Zcb extension.\n");
402420
rv_enable_zcb = true;
403421
break;
422+
case OPT_ENABLE_ZICBOM:
423+
fprintf(stderr, "enabling Zicbom extension.\n");
424+
rv_enable_zicbom = true;
425+
break;
426+
case OPT_ENABLE_ZICBOZ:
427+
fprintf(stderr, "enabling Zicboz extension.\n");
428+
rv_enable_zicboz = true;
429+
break;
430+
case OPT_CACHE_BLOCK_SIZE:
431+
block_size_exp = ilog2(atol(optarg));
432+
433+
if (block_size_exp < 0 || block_size_exp > 12) {
434+
fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg);
435+
exit(1);
436+
}
437+
438+
fprintf(stderr, "setting cache-block-size to 2^%" PRIu64 " = %u B\n",
439+
block_size_exp, 1 << block_size_exp);
440+
rv_cache_block_size_exp = block_size_exp;
441+
break;
404442
case 'x':
405443
fprintf(stderr, "enabling Zfinx support.\n");
406444
rv_enable_zfinx = true;

handwritten_support/riscv_extras.lem

+4
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,10 @@ val plat_rom_size : unit -> bitvector
193193
let plat_rom_size () = []
194194
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
195195

196+
val plat_cache_block_size_exp : unit -> bitvector
197+
let plat_cache_block_size_exp () = []
198+
declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp`
199+
196200
val plat_clint_base : unit -> bitvector
197201
let plat_clint_base () = []
198202
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`

handwritten_support/riscv_extras_sequential.lem

+4
Original file line numberDiff line numberDiff line change
@@ -173,6 +173,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
173173
let plat_rom_size () = wordFromInteger 0
174174
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
175175

176+
val plat_cache_block_size_exp : unit -> integer
177+
let plat_cache_block_size_exp () = wordFromInteger 0
178+
declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp`
179+
176180
val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
177181
let plat_clint_base () = wordFromInteger 0
178182
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`

model/riscv_insts_zicbom.sail

+114
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/*=======================================================================================*/
2+
/* This Sail RISC-V architecture model, comprising all files and */
3+
/* directories except where otherwise noted is subject the BSD */
4+
/* two-clause license in the LICENSE file. */
5+
/* */
6+
/* SPDX-License-Identifier: BSD-2-Clause */
7+
/*=======================================================================================*/
8+
9+
// Cache Block Operations - Management
10+
11+
enum clause extension = Ext_Zicbom
12+
function clause extensionEnabled(Ext_Zicbom) = sys_enable_zicbom()
13+
14+
function cbo_clean_flush_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBCFE][0], senvcfg[CBCFE][0])
15+
function cbo_inval_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][0], senvcfg[CBIE][0])
16+
function cbo_inval_as_inval(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][1], senvcfg[CBIE][1])
17+
18+
/* ****************************************************************** */
19+
union clause ast = RISCV_ZICBOM : (cbop_zicbom, regidx)
20+
21+
mapping encdec_cbop : cbop_zicbom <-> bits(12) = {
22+
CBO_CLEAN <-> 0b000000000001,
23+
CBO_FLUSH <-> 0b000000000010,
24+
CBO_INVAL <-> 0b000000000000,
25+
}
26+
27+
mapping clause encdec = RISCV_ZICBOM(cbop, rs1) if extensionEnabled(Ext_Zicbom)
28+
<-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if extensionEnabled(Ext_Zicbom)
29+
30+
mapping cbop_mnemonic : cbop_zicbom <-> string = {
31+
CBO_CLEAN <-> "cbo.clean",
32+
CBO_FLUSH <-> "cbo.flush",
33+
CBO_INVAL <-> "cbo.inval"
34+
}
35+
36+
mapping clause assembly = RISCV_ZICBOM(cbop, rs1)
37+
<-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
38+
39+
val process_clean_inval : (regidx, cbop_zicbom) -> Retired
40+
function process_clean_inval(rs1, cbop) = {
41+
let rs1_val = X(rs1);
42+
let cache_block_size_exp = plat_cache_block_size_exp();
43+
let cache_block_size = 2 ^ cache_block_size_exp;
44+
45+
// Offset from rs1 to the beginning of the cache block. This is 0 if rs1
46+
// is aligned to the cache block, or negative if rs1 is misaligned.
47+
let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val;
48+
49+
// TODO: This is incorrect since CHERI only requires at least one byte
50+
// to be in bounds here, whereas `ext_data_get_addr()` checks that all bytes
51+
// are in bounds. We will need to add a new function, parameter or access type.
52+
match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) {
53+
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
54+
Ext_DataAddr_OK(vaddr) => {
55+
let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
56+
TR_Address(paddr, _) => {
57+
// "A cache-block management instruction is permitted to access the
58+
// specified cache block whenever a load instruction or store instruction
59+
// is permitted to access the corresponding physical addresses. If
60+
// neither a load instruction nor store instruction is permitted to
61+
// access the physical addresses, but an instruction fetch is permitted
62+
// to access the physical addresses, whether a cache-block management
63+
// instruction is permitted to access the cache block is UNSPECIFIED."
64+
//
65+
// In this implementation we currently don't allow access for fetches.
66+
let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size);
67+
let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size);
68+
match (exc_read, exc_write) {
69+
// Access is permitted if read OR write are allowed. If neither
70+
// are allowed then we always report a store exception.
71+
(Some(exc_read), Some(exc_write)) => Some(exc_write),
72+
_ => None(),
73+
}
74+
},
75+
TR_Failure(e, _) => Some(e)
76+
};
77+
// "If access to the cache block is not permitted, a cache-block management
78+
// instruction raises a store page fault or store guest-page fault exception
79+
// if address translation does not permit any access or raises a store access
80+
// fault exception otherwise."
81+
match res {
82+
// The model has no caches so there's no action required.
83+
None() => RETIRE_SUCCESS,
84+
Some(e) => {
85+
let e : ExceptionType = match e {
86+
E_Load_Access_Fault() => E_SAMO_Access_Fault(),
87+
E_SAMO_Access_Fault() => E_SAMO_Access_Fault(),
88+
E_Load_Page_Fault() => E_SAMO_Page_Fault(),
89+
E_SAMO_Page_Fault() => E_SAMO_Page_Fault(),
90+
// No other exceptions should be generated since we're not checking
91+
// for fetch access and it's can't be misaligned.
92+
_ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"),
93+
};
94+
handle_mem_exception(vaddr, e);
95+
RETIRE_FAIL
96+
}
97+
}
98+
}
99+
}
100+
}
101+
102+
function clause execute(RISCV_ZICBOM(cbop, rs1)) =
103+
match cbop {
104+
CBO_CLEAN if cbo_clean_flush_enabled(cur_privilege) =>
105+
process_clean_inval(rs1, cbop),
106+
CBO_FLUSH if cbo_clean_flush_enabled(cur_privilege) =>
107+
process_clean_inval(rs1, cbop),
108+
CBO_INVAL if cbo_inval_enabled(cur_privilege) =>
109+
process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH),
110+
_ => {
111+
handle_illegal();
112+
RETIRE_FAIL
113+
},
114+
}

model/riscv_insts_zicboz.sail

+65
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
/*=======================================================================================*/
2+
/* This Sail RISC-V architecture model, comprising all files and */
3+
/* directories except where otherwise noted is subject the BSD */
4+
/* two-clause license in the LICENSE file. */
5+
/* */
6+
/* SPDX-License-Identifier: BSD-2-Clause */
7+
/*=======================================================================================*/
8+
9+
// Cache Block Operations - Zero
10+
11+
enum clause extension = Ext_Zicboz
12+
function clause extensionEnabled(Ext_Zicboz) = sys_enable_zicboz()
13+
14+
function cbo_zero_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBZE][0], senvcfg[CBZE][0])
15+
16+
/* ****************************************************************** */
17+
union clause ast = RISCV_ZICBOZ : (regidx)
18+
19+
mapping clause encdec = RISCV_ZICBOZ(rs1) if extensionEnabled(Ext_Zicboz)
20+
<-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if extensionEnabled(Ext_Zicboz)
21+
22+
mapping clause assembly = RISCV_ZICBOZ(rs1)
23+
<-> "cbo.zero" ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
24+
25+
function clause execute(RISCV_ZICBOZ(rs1)) = {
26+
if cbo_zero_enabled(cur_privilege) then {
27+
let rs1_val = X(rs1);
28+
let cache_block_size_exp = plat_cache_block_size_exp();
29+
let cache_block_size = 2 ^ cache_block_size_exp;
30+
31+
// Offset from rs1 to the beginning of the cache block. This is 0 if rs1
32+
// is aligned to the cache block, or negative if rs1 is misaligned.
33+
let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val;
34+
35+
match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) {
36+
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
37+
Ext_DataAddr_OK(vaddr) => {
38+
// "An implementation may update the bytes in any order and with any granularity
39+
// and atomicity, including individual bytes."
40+
//
41+
// This implementation does a single atomic write.
42+
match translateAddr(vaddr, Write(Data)) {
43+
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
44+
TR_Address(paddr, _) => {
45+
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, cache_block_size, false, false, false);
46+
match (eares) {
47+
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
48+
MemValue(_) => {
49+
let res : MemoryOpResult(bool) = mem_write_value(paddr, cache_block_size, zeros(), false, false, false);
50+
match (res) {
51+
MemValue(true) => RETIRE_SUCCESS,
52+
MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
53+
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
54+
}
55+
}
56+
}
57+
}
58+
}
59+
},
60+
}
61+
} else {
62+
handle_illegal();
63+
RETIRE_FAIL
64+
}
65+
}

model/riscv_platform.sail

+5
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,11 @@ val elf_entry = {
2626
c: "elf_entry"
2727
} : unit -> int
2828

29+
// Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096)
30+
// because this model performs `cbo.zero` with a single write, and the behaviour
31+
// with cache blocks larger than a page is not clearly defined.
32+
val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12)
33+
2934
/* Main memory */
3035
val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
3136
val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits

model/riscv_sys_control.sail

+8
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,14 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) =
103103
function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
104104
not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1)
105105

106+
// There are several features that are controlled by machine/supervisor enable
107+
// bits (m/senvcfg, m/scounteren, etc.). This abstracts that logic.
108+
function feature_enabled_for_priv(p : Privilege, machine_enable_bit : bit, supervisor_enable_bit : bit) -> bool = match p {
109+
Machine => true,
110+
Supervisor => machine_enable_bit == bitone,
111+
User => machine_enable_bit == bitone & (not(extensionEnabled(Ext_S)) | supervisor_enable_bit == bitone),
112+
}
113+
106114
function check_Counteren(csr : csreg, p : Privilege) -> bool =
107115
match(csr, p) {
108116
(0xC00, Supervisor) => mcounteren[CY] == 0b1,

0 commit comments

Comments
 (0)