diff options
| -rw-r--r-- | mips/mips_extras_sequential_embed.lem | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/mips/mips_extras_sequential_embed.lem b/mips/mips_extras_sequential_embed.lem new file mode 100644 index 00000000..e765bd23 --- /dev/null +++ b/mips/mips_extras_sequential_embed.lem @@ -0,0 +1,49 @@ +open import Pervasives +open import Sail_impl_base +open import Sail_values +open import State + +let endian = E_big_endian + +val MEMr : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) +val MEMr_tag : (vector bitU * integer) -> M (vector bitU) +val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU) + +let MEMr (addr,size) = read_mem endian false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem endian false Read_reserve addr size +let MEMr_tag (addr,size) = read_mem endian false Read_tag addr size +let MEMr_tag_reserve (addr,size) = read_mem endian false Read_tag_reserve addr size + + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_conditional : (vector bitU * integer) -> M unit +val MEMea_tag : (vector bitU * integer) -> M unit +val MEMea_tag_conditional : (vector bitU * integer) -> M unit + +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size +let MEMea_tag (addr,size) = write_mem_ea Write_tag addr size +let MEMea_tag_conditional (addr,size) = write_mem_ea Write_tag_conditional addr size + + +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU +val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit +val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU + +let MEMval (_,_,v) = write_mem_val endian v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O) +let MEMval_tag (_,_,v) = write_mem_val endian v >>= fun _ -> return () +let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O) + + +val MEM_sync : unit -> M unit + +let MEM_sync () = barrier Barrier_Isync + + +let duplicate (bit,len) = + let bits = repeat [bit] len in + let start = len - 1 in + Vector bits start false |