diff options
Diffstat (limited to 'mips_new_tc')
| -rw-r--r-- | mips_new_tc/mips_extras_embed_sequential.lem | 51 | ||||
| -rw-r--r-- | mips_new_tc/mips_insts.sail | 28 |
2 files changed, 65 insertions, 14 deletions
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem new file mode 100644 index 00000000..ad567598 --- /dev/null +++ b/mips_new_tc/mips_extras_embed_sequential.lem @@ -0,0 +1,51 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values +open import State + +val MEMr : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) +val MEMr_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) +val MEMr_tag : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) +val MEMr_tag_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) + +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size + +let MEMr_tag (addr,size) = + read_mem false Read_plain addr size >>= fun v -> + read_tag false Read_plain addr >>= fun t -> + return (t, v) + +let MEMr_tag_reserve (addr,size) = + read_mem false Read_plain addr size >>= fun v -> + read_tag false Read_plain addr >>= fun t -> + return (t, v) + + +val MEMea : forall 'a. (bitvector 'a * integer) -> M unit +val MEMea_conditional : forall 'a. (bitvector 'a * integer) -> M unit +val MEMea_tag : forall 'a. (bitvector 'a * integer) -> M unit +val MEMea_tag_conditional : forall 'a. (bitvector 'a * 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_plain addr size +let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size + + +val MEMval : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M unit +val MEMval_conditional : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M bool +val MEMval_tag : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M unit +val MEMval_tag_conditional : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M bool + +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false) +let MEMval_tag (_,_,t,v) = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return () +let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then true else false) + +val MEM_sync : unit -> M unit + +let MEM_sync () = barrier Barrier_MIPS_SYNC + diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail index 1d3c5f4a..96826dae 100644 --- a/mips_new_tc/mips_insts.sail +++ b/mips_new_tc/mips_insts.sail @@ -1136,24 +1136,24 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = else let pAddr = (TLBTranslate(vAddr, LoadData)) in { - (bit[64]) memResult := if (linked) then + (bit[64]) memResult := if (linked) then { CP0LLBit := 0b1; - CP0LLAddr := pAddr; - switch wordWidthBytes(width) { - case ([:1:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed) - case ([:2:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed) - case ([:4:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed) - case ([:8:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed) - } + CP0LLAddr := pAddr; + w := wordWidthBytes(width); + if w == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signed) + else if w == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signed) + else if w == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signed) + else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signed) } else - switch wordWidthBytes(width) { - case ([:1:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed) - case ([:2:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed) - case ([:4:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed) - case ([:8:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed) - }; + { + w := wordWidthBytes(width); + if w == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signed) + else if w == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signed) + else if w == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signed) + else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signed); + }; wGPR(rt) := memResult } } |