diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-26 15:13:59 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-26 15:13:59 -0800 |
| commit | 026d08247408c49828e38221fd0899349a82e1b6 (patch) | |
| tree | f537174ec580e31a94c459cd3bca01d1ab342e35 /handwritten_support | |
| parent | 930ce615f4b7052b4b33f070f315152aa798bf7d (diff) | |
| download | sail-riscv-026d08247408c49828e38221fd0899349a82e1b6.zip sail-riscv-026d08247408c49828e38221fd0899349a82e1b6.tar.gz sail-riscv-026d08247408c49828e38221fd0899349a82e1b6.tar.bz2 | |
Restore riscv_extras damaged by merge.
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 2919d77..ed572be 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -49,15 +49,19 @@ let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV 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 Write_plain address size 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 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 addr size +let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addr size +let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addr size +let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addr size +let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addr size +let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addr size val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit let load_reservation addr = () |