1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
open import Pervasives
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt
type bitvector 'a = mword 'a
let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ())
let MEM_fence_r_rw () = barrier (Barrier_RISCV_r_rw ())
let MEM_fence_r_r () = barrier (Barrier_RISCV_r_r ())
let MEM_fence_rw_w () = barrier (Barrier_RISCV_rw_w ())
let MEM_fence_w_w () = barrier (Barrier_RISCV_w_w ())
let MEM_fence_w_rw () = barrier (Barrier_RISCV_w_rw ())
let MEM_fence_rw_r () = barrier (Barrier_RISCV_rw_r ())
let MEM_fence_r_w () = barrier (Barrier_RISCV_r_w ())
let MEM_fence_w_r () = barrier (Barrier_RISCV_w_r ())
let MEM_fence_tso () = barrier (Barrier_RISCV_tso ())
let MEM_fence_i () = barrier (Barrier_RISCV_i ())
val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_conditional : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_conditional_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
let MEMea addr size = write_mem_ea Write_plain () addr size
let MEMea_release addr size = write_mem_ea Write_RISCV_release () addr size
let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_release () addr size
let MEMea_conditional addr size = write_mem_ea Write_RISCV_conditional () addr size
let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_release () addr size
let MEMea_conditional_strong_release addr size
= write_mem_ea Write_RISCV_conditional_strong_release () addr size
val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
let MEMr addrsize size hexRAM addr = read_mem Read_plain addrsize addr size
let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addrsize addr size
let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addrsize addr size
let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addrsize addr size
let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addrsize addr size
let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addrsize addr size
val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
let MEMw addrsize size hexRAM addr = write_mem Write_plain addrsize addr size
let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addrsize addr size
let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addrsize addr size
let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addrsize addr size
let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addrsize addr size
let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addrsize addr size
val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
let load_reservation addr = ()
let speculate_conditional_success () = excl_result ()
let match_reservation _ = true
let cancel_reservation () = ()
val sys_enable_writable_misa : unit -> bool
let sys_enable_writable_misa () = true
declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa`
val sys_enable_rvc : unit -> bool
let sys_enable_rvc () = true
declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
val sys_enable_next : unit -> bool
let sys_enable_next () = true
declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
val sys_enable_fdext : unit -> bool
let sys_enable_fdext () = true
declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`
val sys_enable_zfinx : unit -> bool
let sys_enable_zfinx () = false
declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_base () = wordFromInteger 0
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_size () = wordFromInteger 0
declare ocaml target_rep function plat_ram_size = `Platform.dram_size`
val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_base () = wordFromInteger 0
declare ocaml target_rep function plat_rom_base = `Platform.rom_base`
val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_size () = wordFromInteger 0
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_clint_base () = wordFromInteger 0
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_clint_size () = wordFromInteger 0
declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
val plat_enable_dirty_update : unit -> bool
let plat_enable_dirty_update () = false
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`
val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
val plat_enable_pmp : unit -> bool
let plat_enable_pmp () = false
declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp`
val plat_mtval_has_illegal_inst_bits : unit -> bool
let plat_mtval_has_illegal_inst_bits () = false
declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
val plat_insns_per_tick : unit -> integer
let plat_insns_per_tick () = 1
declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
let plat_htif_tohost () = wordFromInteger 0
declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit
let plat_term_write _ = ()
declare ocaml target_rep function plat_term_write = `Platform.term_write`
val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
let plat_term_read () = wordFromInteger 0
declare ocaml target_rep function plat_term_read = `Platform.term_read`
val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
let plat_get_16_random_bits () = wordFromInteger 0
declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`
val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_right v m = shiftr v (uint m)
val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_left v m = shiftl v (uint m)
val print_string : string -> string -> unit
let print_string msg s = () (* print_endline (msg ^ s) *)
val prerr_string : string -> string -> unit
let prerr_string msg s = prerr_endline (msg ^ s)
val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
val print_dbg : string -> unit
let print_dbg msg = ()
|
