diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_extras.lem | 3 | ||||
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 2 | ||||
| -rw-r--r-- | mips/mips_regfp.sail | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index 74119914..4bbf368b 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -73,6 +73,5 @@ let memory_vals : memory_write_vals = let barrier_functions = [ - (*Need to know what barrier kind to install*) - ("MEM_sync", Barrier_Isync); + ("MEM_sync", Barrier_MIPS_SYNC); ] diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem index e765bd23..6070df09 100644 --- a/mips/mips_extras_embed_sequential.lem +++ b/mips/mips_extras_embed_sequential.lem @@ -40,7 +40,7 @@ let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return val MEM_sync : unit -> M unit -let MEM_sync () = barrier Barrier_Isync +let MEM_sync () = barrier Barrier_MIPS_SYNC let duplicate (bit,len) = diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail index 816cd1fe..1a290ec7 100644 --- a/mips/mips_regfp.sail +++ b/mips/mips_regfp.sail @@ -403,7 +403,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( case (PREF(base, op, imm)) = *) case (SYNC) -> { - iK := IK_barrier(Barrier_Sync); + iK := IK_barrier(Barrier_MIPS_SYNC); } (* case (MFC0(rt, rd, sel, double)) |