RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it and tests.

1 files changed, 0 insertions, 135 deletions

diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
deleted file mode 100644
index 7028d5b8..00000000
--- a/riscv/riscv_extras_sequential.lem
+++ /dev/null
@@ -1,135 +0,0 @@
-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_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 addr size
-let MEMr_acquire addrsize size hexRAM addr                 = read_mem Read_RISCV_acquire addr size
-let MEMr_strong_acquire addrsize size hexRAM addr          = read_mem Read_RISCV_strong_acquire addr size
-let MEMr_reserved addrsize size hexRAM addr                = read_mem Read_RISCV_reserved addr size
-let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV_reserved_acquire addr size
-let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size
-
-val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-let write_ram addrsize size hexRAM address value =
-  write_mem_val value
-
-val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-let read_ram addrsize size hexRAM address =
-  read_mem Read_plain address size
-
-val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
-let load_reservation addr = ()
-
-let speculate_conditional_success _ = excl_result ()
-
-let cancel_reservation () = ()
-
-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_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 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))) *)