diff options
Diffstat (limited to 'mips/mips_extras_embed_sequential.lem')
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem index ad1231b6..73dc42ed 100644 --- a/mips/mips_extras_embed_sequential.lem +++ b/mips/mips_extras_embed_sequential.lem @@ -6,14 +6,21 @@ open import State 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) +val MEMr_tag : (vector bitU * integer) -> M (bitU * vector bitU) +val MEMr_tag_reserve : (vector bitU * integer) -> M (bitU * vector bitU) 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 -let MEMr_tag_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 : (vector bitU * integer) -> M unit @@ -30,17 +37,13 @@ let MEMea_tag_conditional (addr,size) = write_mem_ea Write_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 v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) -let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +val MEMval_tag : (vector bitU * integer * bitU * vector bitU) -> M unit +val MEMval_tag_conditional : (vector bitU * integer * bitU * vector bitU) -> M bitU -(* TODO *) -val TAGw : (vector bitU * vector bitU) -> M unit -let TAGw (addr, tag) = failwith "TAGw not implemented" +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +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 B1 else B0) val MEM_sync : unit -> M unit |