diff options
Diffstat (limited to 'riscv/riscv_extras_sequential.lem')
| -rw-r--r-- | riscv/riscv_extras_sequential.lem | 135 |
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))) *) |