Skip to content

Commit 1b6404d

Browse files
committed
Add support for Zcmt extension
1 parent 8387b14 commit 1b6404d

12 files changed

+144
-1
lines changed

c_emulator/riscv_platform.c

+10
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,16 @@ bool sys_enable_zcb(unit u)
3737
return rv_enable_zcb;
3838
}
3939

40+
bool sys_enable_zcd(unit u)
41+
{
42+
return rv_enable_zcd;
43+
}
44+
45+
bool sys_enable_zcmt(unit u)
46+
{
47+
return rv_enable_zcmt;
48+
}
49+
4050
bool sys_enable_zfinx(unit u)
4151
{
4252
return rv_enable_zfinx;

c_emulator/riscv_platform.h

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ bool sys_enable_rvc(unit);
55
bool sys_enable_fdext(unit);
66
bool sys_enable_svinval(unit);
77
bool sys_enable_zcb(unit);
8+
bool sys_enable_zcd(unit);
9+
bool sys_enable_zcmt(unit);
810
bool sys_enable_zfinx(unit);
911
bool sys_enable_writable_misa(unit);
1012
bool sys_enable_writable_fiom(unit);

c_emulator/riscv_platform_impl.c

+2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ uint64_t rv_vector_elen_exp = 0x6;
1111

1212
bool rv_enable_svinval = false;
1313
bool rv_enable_zcb = false;
14+
bool rv_enable_zcd = true;
15+
bool rv_enable_zcmt = false;
1416
bool rv_enable_zfinx = false;
1517
bool rv_enable_rvc = true;
1618
bool rv_enable_writable_misa = true;

c_emulator/riscv_platform_impl.h

+2
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ extern uint64_t rv_vector_elen_exp;
1616

1717
extern bool rv_enable_svinval;
1818
extern bool rv_enable_zcb;
19+
extern bool rv_enable_zcd;
20+
extern bool rv_enable_zcmt;
1921
extern bool rv_enable_zfinx;
2022
extern bool rv_enable_rvc;
2123
extern bool rv_enable_fdext;

c_emulator/riscv_sim.c

+6
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ enum {
5050
OPT_PMP_GRAIN,
5151
OPT_ENABLE_SVINVAL,
5252
OPT_ENABLE_ZCB,
53+
OPT_ENABLE_ZCMT,
5354
OPT_ENABLE_ZICBOM,
5455
OPT_ENABLE_ZICBOZ,
5556
OPT_ENABLE_SSTC,
@@ -148,6 +149,7 @@ static struct option options[] = {
148149
{"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM},
149150
{"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL },
150151
{"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB },
152+
{"enable-zcmt", no_argument, 0, OPT_ENABLE_ZCMT },
151153
{"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM },
152154
{"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ },
153155
{"cache-block-size", required_argument, 0, OPT_CACHE_BLOCK_SIZE },
@@ -387,6 +389,10 @@ static int process_args(int argc, char **argv)
387389
case OPT_ENABLE_ZCB:
388390
fprintf(stderr, "enabling Zcb extension.\n");
389391
rv_enable_zcb = true;
392+
case OPT_ENABLE_ZCMT:
393+
fprintf(stderr, "enabling Zcmt extension.\n");
394+
rv_enable_zcd = false;
395+
rv_enable_zcmt = true;
390396
break;
391397
case OPT_ENABLE_ZICBOM:
392398
fprintf(stderr, "enabling Zicbom extension.\n");

model/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ foreach (xlen IN ITEMS 32 64)
6666
"riscv_insts_zbc.sail"
6767
"riscv_insts_zbs.sail"
6868
"riscv_insts_zcb.sail"
69+
"riscv_insts_zcmt.sail"
6970
"riscv_insts_zfh.sail"
7071
# Zfa needs to be added after fext, dext and Zfh (as it needs
7172
# definitions from those)

model/riscv_addr_checks.sail

+5
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,11 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex
5959
let addr = virtaddr(X(base) + offset) in
6060
Ext_DataAddr_OK(addr)
6161

62+
function ext_data_get_addr_from_bits(addr_ext : xlenbits, acc : AccessType(ext_access_type), width : mem_access_width)
63+
-> Ext_DataAddr_Check(ext_data_addr_error) =
64+
let addr = virtaddr(addr_ext) in
65+
Ext_DataAddr_OK(addr)
66+
6267
function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
6368
()
6469

model/riscv_extensions.sail

+2
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,8 @@ enum clause extension = Ext_Zdinx
6767
enum clause extension = Ext_Zca
6868
// Code Size Reduction: additional 16-bit aliases
6969
enum clause extension = Ext_Zcb
70+
// Code Size Reduction: compressed table jump instructions
71+
enum clause extension = Ext_Zcmt
7072
// Code Size Reduction: compressed double precision floating point loads and stores
7173
enum clause extension = Ext_Zcd
7274
// Code Size Reduction: compressed single precision floating point loads and stores

model/riscv_insts_zcd.sail

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
/* SPDX-License-Identifier: BSD-2-Clause */
77
/*=======================================================================================*/
88

9-
function clause extensionEnabled(Ext_Zcd) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_D) & (xlen == 32 | xlen == 64)
9+
function clause extensionEnabled(Ext_Zcd) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_D) & sys_enable_zcd() & not(sys_enable_zcmt()) & (xlen == 32 | xlen == 64)
1010

1111
union clause ast = C_FLDSP : (bits(6), regidx)
1212

model/riscv_insts_zcmt.sail

+95
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
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+
function clause extensionEnabled(Ext_Zcmt) = extensionEnabled(Ext_Zca) & sys_enable_zcmt() & not(sys_enable_zcd()) & (xlen == 32 | xlen == 64)
10+
11+
type target_address = bits(xlen)
12+
13+
union FJT_Result = {
14+
FJT_Success : target_address,
15+
FJT_Failure : unit
16+
}
17+
18+
function fetch_jump_table(table_address : bits(xlen)) -> FJT_Result = {
19+
/* Fetching jump table address needs execute permission */
20+
match ext_data_get_addr_from_bits(table_address, Execute(), xlen_bytes) {
21+
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); FJT_Failure() },
22+
Ext_DataAddr_OK(vaddr) => {
23+
if check_misaligned(vaddr, size_bytes(xlen_bytes))
24+
then { handle_mem_exception(vaddr, E_Load_Addr_Align()); FJT_Failure() }
25+
else match translateAddr(vaddr, Execute()) {
26+
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); FJT_Failure() },
27+
TR_Address(paddr, _) =>
28+
match mem_read(Execute(), paddr, xlen_bytes, false, false, false) {
29+
Ok(result) => { FJT_Success(result) },
30+
Err(e) => { handle_mem_exception(vaddr, e); FJT_Failure() },
31+
},
32+
}
33+
},
34+
};
35+
}
36+
37+
union clause ast = CM_JALT : (bits(8))
38+
39+
mapping clause encdec_compressed = CM_JALT(index) if extensionEnabled(Ext_Zcmt) & 32 <= unsigned(index)
40+
<-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 if extensionEnabled(Ext_Zcmt) & 32 <= unsigned(index)
41+
42+
function clause execute (CM_JALT(index)) = {
43+
let base : bits(xlen) = jvt.bits & ~(zero_extend(0x3F));
44+
let index : bits(xlen) = zero_extend(index);
45+
if jvt[mode] == 0b000000 then {
46+
let table_address : bits(xlen) = match xlen {
47+
32 => base + index << 2,
48+
64 => base + index << 3,
49+
_ => internal_error(__FILE__, __LINE__, "Unsupported xlen")
50+
};
51+
match fetch_jump_table(table_address) {
52+
FJT_Failure(_) => {
53+
return RETIRE_FAIL
54+
},
55+
FJT_Success(target_address) => {
56+
X(0b00001) = get_next_pc();
57+
set_next_pc(target_address & ~(zero_extend(0x1)));
58+
}
59+
};
60+
};
61+
RETIRE_SUCCESS
62+
}
63+
64+
mapping clause assembly = CM_JALT(index) if (xlen == 32 | xlen == 64) <->
65+
"cm.jalt" ^ spc() ^ hex_bits_8(index) if (xlen == 32 | xlen == 64)
66+
67+
/* ****************************************************************** */
68+
union clause ast = CM_JT : (bits(8))
69+
70+
mapping clause encdec_compressed = CM_JT(index) if extensionEnabled(Ext_Zcmt) & unsigned(index) < 32
71+
<-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 if extensionEnabled(Ext_Zcmt) & unsigned(index) < 32
72+
73+
function clause execute (CM_JT(index)) = {
74+
let base : bits(xlen) = jvt.bits & ~(zero_extend(0x3F));
75+
let index : bits(xlen) = zero_extend(index);
76+
if jvt[mode] == 0b000000 then {
77+
let table_address : bits(xlen) = match xlen {
78+
32 => base + index << 2,
79+
64 => base + index << 3,
80+
_ => internal_error(__FILE__, __LINE__, "Unsupported xlen")
81+
};
82+
match fetch_jump_table(table_address) {
83+
FJT_Failure(_) => {
84+
return RETIRE_FAIL
85+
},
86+
FJT_Success(target_address) => {
87+
set_next_pc(target_address & ~(zero_extend(0x1)));
88+
}
89+
};
90+
};
91+
RETIRE_SUCCESS
92+
}
93+
94+
mapping clause assembly = CM_JT(index) if (xlen == 32 | xlen == 64) <->
95+
"cm.jt" ^ spc() ^ hex_bits_8(index) if (xlen == 32 | xlen == 64)

model/riscv_sys_regs.sail

+17
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,10 @@ val sys_enable_fdext = pure "sys_enable_fdext" : unit -> bool
9292
val sys_enable_svinval = pure "sys_enable_svinval" : unit -> bool
9393
/* whether Zcb was enabled at boot */
9494
val sys_enable_zcb = pure "sys_enable_zcb" : unit -> bool
95+
/* whether Zcd was enabled at boot */
96+
val sys_enable_zcd = pure "sys_enable_zcd" : unit -> bool
97+
/* whether Zcmt was enabled at boot */
98+
val sys_enable_zcmt = pure "sys_enable_zcmt" : unit -> bool
9599
/* whether zfinx was enabled at boot */
96100
val sys_enable_zfinx = pure "sys_enable_zfinx" : unit -> bool
97101
/* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
@@ -508,6 +512,16 @@ function clause write_CSR((0x302, value) if xlen == 32) = { medeleg = legalize_m
508512
function clause write_CSR((0x312, value) if xlen == 32) = { medeleg = legalize_medeleg(medeleg, value @ medeleg.bits[31 .. 0]); medeleg.bits[63 .. 32] }
509513
function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
510514

515+
bitfield Jvt : xlenbits = {
516+
base : xlen - 1 .. 6,
517+
mode : 5 .. 0
518+
}
519+
register jvt : Jvt
520+
mapping clause csr_name_map = 0x017 <-> "jvt"
521+
function clause is_CSR_defined (0x017) = sys_enable_zcmt()
522+
function clause write_CSR(0x017, value) = { jvt.bits = (value >> 6 ) << 6; jvt.bits }
523+
function clause read_CSR(0x017) = jvt.bits
524+
511525
/* registers for trap handling */
512526

513527
bitfield Mtvec : xlenbits = {
@@ -902,6 +916,9 @@ function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
902916

903917
/*
904918
* Entropy Source - Platform access to random bits.
919+
* WARNING: This function currently lacks a proper side-effect annotation.
920+
* If you are using theorem prover tool flows, you
921+
* may need to modify or stub out this function for now.
905922
* NOTE: This would be better placed in riscv_platform.sail, but that file
906923
* appears _after_ this one in the compile order meaning the valspec
907924
* for this function is unavailable when it's first encountered in

model/riscv_termination.sail

+1
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ function extensionEnabled_measure(ext : extension) -> int =
5656
Ext_Zcb => 2, // Ext_Zca
5757
Ext_Zcd => 2, // Ext_Zca, (Ext_D)
5858
Ext_Zcf => 2, // Ext_Zca, (Ext_F)
59+
Ext_Zcmt => 2, // Ext_Zcmt
5960
_ => 0
6061
}
6162
termination_measure extensionEnabled(ext) = extensionEnabled_measure(ext)

0 commit comments

Comments
 (0)