Skip to content

Commit 71ae7dc

Browse files
rmn30rmn30
committed
Work in progress on integrating rv_config output. Note generated riscv_config.sail committed for convenience at the moment.
1 parent 96e4dcc commit 71ae7dc

File tree

10 files changed

+727
-33
lines changed

10 files changed

+727
-33
lines changed

‎Makefile

Lines changed: 23 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,15 @@ else
1515
$(error '$(ARCH)' is not a valid architecture, must be one of: RV32, RV64)
1616
endif
1717

18+
19+
CONFIG_PLATFORM=config/platform.yaml
20+
CONFIG_ISA=config/isa.yaml
21+
GENERATED_CONFIG_DIR=generated_definitions/config
22+
RV_CONFIG=riscv-config
23+
RV_CONFIG2SAIL=rv_conf2sail
24+
RV_CONFIG_SAIL=$(GENERATED_CONFIG_DIR)/riscv_config.sail
25+
RV_CONFIG_TYPES:=$(shell opam config var riscv_config2sail:share)/riscv_config_types.sail
26+
1827
# Instruction sources, depending on target
1928
SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail
2029
SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail
@@ -67,12 +76,13 @@ SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS) riscv_analysis.sail
6776
SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail riscv_analysis.sail
6877
endif
6978

79+
RV_CONFIG_SRCS = $(RV_CONFIG_TYPES) $(RV_CONFIG_SAIL)
7080

71-
PRELUDE_SRCS = $(addprefix model/,$(PRELUDE))
72-
SAIL_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS))
73-
SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS))
74-
SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS))
75-
SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS))
81+
PRELUDE_SRCS = $(RV_CONFIG_SRCS) $(addprefix model/,$(PRELUDE))
82+
SAIL_SRCS = $(RV_CONFIG_SRCS) $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS))
83+
SAIL_RMEM_SRCS = $(RV_CONFIG_SRCS) $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS))
84+
SAIL_RVFI_SRCS = $(RV_CONFIG_SRCS) $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS))
85+
SAIL_COQ_SRCS = $(RV_CONFIG_SRCS) $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS))
7686

7787
PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml riscv_ocaml_sim.ml)
7888

@@ -121,10 +131,10 @@ C_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
121131
endif
122132

123133
# SAIL_FLAGS = -dtc_verbose 4
134+
SAIL_FLAGS += -O -Oconstant_fold
124135

125136
ifneq (,$(COVERAGE))
126137
C_FLAGS += --coverage -O1
127-
SAIL_FLAGS += -Oconstant_fold
128138
else
129139
C_FLAGS += -O3 -flto
130140
endif
@@ -198,7 +208,7 @@ ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml
198208

199209
generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
200210
mkdir -p generated_definitions/c
201-
$(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
211+
$(SAIL) $(SAIL_FLAGS) -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
202212

203213
# convenience target
204214
.PHONY: csim
@@ -209,9 +219,14 @@ rvfi: c_emulator/riscv_rvfi
209219
c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) Makefile
210220
gcc -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
211221

222+
$(RV_CONFIG_SAIL): $(CONFIG_ISA) $(CONFIG_PLATFORM)
223+
mkdir -p $(GENERATED_CONFIG_DIR)
224+
$(RV_CONFIG) --isa_spec $(CONFIG_ISA) --platform_spec $(CONFIG_PLATFORM) --work_dir $(GENERATED_CONFIG_DIR)
225+
$(RV_CONFIG2SAIL) -i $(GENERATED_CONFIG_DIR)/isa_checked.yaml -p $(GENERATED_CONFIG_DIR)/platform_checked.yaml -o $@
226+
212227
generated_definitions/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
213228
mkdir -p generated_definitions/c
214-
$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
229+
$(SAIL) $(SAIL_FLAGS) -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
215230
sed -i -e '/^[[:space:]]*$$/d' $@
216231

217232
c_emulator/riscv_rvfi: generated_definitions/c/riscv_rvfi_model.c $(C_INCS) $(C_SRCS) Makefile

‎config/isa.yaml

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
User_Spec_Version: "2.3"
2+
ISA: "RV64IMACSUZicsr_Zifencei"
3+
Privilege_Spec_Version: "1.11"
4+
misa:
5+
implemented: True
6+
MXL:
7+
range:
8+
# only 64-bit supported
9+
rangelist: [[2]]
10+
mode: "Unchanged"
11+
Extensions:
12+
bitmask:
13+
# Only C is writable currently
14+
mask: 0x4
15+
# Zy xwvU tSrq ponM lkjI hgfe dcbA
16+
default: 0x2141101
17+
mvendorid:
18+
implemented: True
19+
id: 0x565656
20+
marchid:
21+
implemented: True
22+
id: 0x569895
23+
mimpid:
24+
implemented: True
25+
id: 0x987562
26+
mhartid: 0x669994
27+
mstatus:
28+
XS:
29+
is_hardwired: False
30+
SD:
31+
is_hardwired: False
32+
FS:
33+
range:
34+
rangelist: [[0,3]]
35+
mode: "Unchanged"
36+
MPP:
37+
range:
38+
rangelist: [[0,1],[3]]
39+
mode: "Nextdown"
40+
SXL:
41+
# is_hardwired: True
42+
# hardwired_field: "MXL"
43+
range:
44+
rangelist: [[1,2]]
45+
UXL:
46+
#is_hardwired: True
47+
# hardwired_field: "MXL"
48+
range:
49+
rangelist: [[1]]
50+
mtvec:
51+
BASE:
52+
range:
53+
rangelist: [[0x00,0x3fffffffffffffff]]
54+
mode: Addr
55+
MODE:
56+
range:
57+
rangelist: [[0,1]]
58+
mideleg:
59+
bitmask:
60+
mask: 0xFFF0FFFFFFFFFFFF
61+
default: 0x00
62+
medeleg:
63+
bitmask:
64+
mask: 0xFFFFFFFFFFFFF7FF
65+
default: 0x00
66+
mip:
67+
bitmask:
68+
mask: 0xF7AFFFFFFFFFFFFF
69+
default: 0x00
70+
mie:
71+
bitmask:
72+
mask: 0xF7AFFFFFFFFFFFFF
73+
default: 0x00
74+
mepc:
75+
# bitmask:
76+
# mask: 0xFFFFFFFFFFFFFFFE
77+
# default: 0x00
78+
range:
79+
rangelist: [[0x00,0xFFFFFFFFFFFFFFFF]]
80+
mcountinhibit:
81+
bitmask:
82+
mask: 0x1F
83+
default: 0x00
84+
# is_hardwired: True
85+
# hardwired_val: 0
86+
mcounteren:
87+
bitmask:
88+
mask: 0x1F
89+
default: 0x00
90+
# is_hardwired: True
91+
# hardwired_val: 0
92+
mhpmcounter3:
93+
is_hardwired: False
94+
mhpmcounter4:
95+
is_hardwired: False
96+
mhpmcounter5:
97+
is_hardwired: False
98+
satp:
99+
MODE:
100+
range:
101+
rangelist: [[0],[8]]
102+
mode: "Unchanged"
103+
ASID:
104+
bitmask:
105+
mask: 0x1FF
106+
default: 0x00
107+
# range:
108+
# rangelist: [[0,0x1FF]]
109+
# mode: "Unchanged"
110+
PPN:
111+
bitmask:
112+
mask: 0xFFFFFFFFFFF
113+
default: 0x00
114+
# range:
115+
# rangelist: [[0,0xFFFFFFFFFFF]]
116+
# mode: "Unchanged"
117+
sepc:
118+
# bitmask:
119+
# mask: 0xFFFFFFFFFFFFFFFE
120+
# default: 0x00
121+
range:
122+
rangelist: [[0x00,0xFFFFFFFFFFFFFFFF]]
123+
sip:
124+
bitmask:
125+
mask: 0xF7AFFFFFFFFFFFFF
126+
default: 0x00
127+
sie:
128+
bitmask:
129+
mask: 0xF7AFFFFFFFFFFFFF
130+
default: 0x00
131+
scounteren:
132+
bitmask:
133+
mask: 0x1F
134+
default: 0x00
135+
# is_hardwired: True
136+
# hardwired_val: 0

‎config/platform.yaml

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
nmi:
2+
address: 0x3000
3+
reset:
4+
address: 0x4000
5+
mtime:
6+
address: 0x5000
7+
implemented: True
8+
mtimecmp:
9+
address: 0x5008
10+
implemented: True
11+
mcause:
12+
values: [16,17,18,19,20,21]
13+
implemented: True
14+
scause:
15+
values: [16,17,18,19,20,21]
16+
implemented: True
17+
mhpmevent3:
18+
bitmask:
19+
mask: 0xFC
20+
default: 0x00
21+
# readonly: True
22+
# hardwired: '0'
23+
mhpmevent4:
24+
range:
25+
rangelist: [[256,0xFFFFFFFFFFFFFF00]]
26+
mode: Unchanged
27+
# readonly: True
28+
# hardwired: '0'
29+
mhpmevent5:
30+
range:
31+
rangelist: [[0],[2]]
32+
mode: "Unchanged"
33+
# readonly: True
34+
# hardwired: '0'

0 commit comments

Comments
 (0)