summaryrefslogtreecommitdiff
path: root/power/power_extras_embed_sequential.lem
diff options
context:
space:
mode:
authorAlasdair2020-07-31 13:30:53 +0100
committerAlasdair2020-07-31 13:30:53 +0100
commitdd76fdfd819bb1a5423cea369df0e7f2ae449b62 (patch)
tree88d8d69e39b724902b280beaa8ce874e444f5dbc /power/power_extras_embed_sequential.lem
parent71db59830383b7db5316b5c99ccebe776fc837dc (diff)
Remove old specs that have more up to date version
Move outdated things into old subdirectory
Diffstat (limited to 'power/power_extras_embed_sequential.lem')
-rw-r--r--power/power_extras_embed_sequential.lem50
1 files changed, 0 insertions, 50 deletions
diff --git a/power/power_extras_embed_sequential.lem b/power/power_extras_embed_sequential.lem
deleted file mode 100644
index 4ec33151..00000000
--- a/power/power_extras_embed_sequential.lem
+++ /dev/null
@@ -1,50 +0,0 @@
-open import Pervasives
-open import Sail_impl_base
-open import Sail_values
-open import State
-
-val MEMr' : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserve' : (vector bitU * integer) -> M (vector bitU)
-
-let MEMr' (addr,size) = read_mem true Read_plain addr size
-let MEMr_reserve' (addr,size) = read_mem true Read_reserve addr size
-
-
-val MEMw_EA : (vector bitU * integer) -> M unit
-val MEMr_EA_cond : (vector bitU * integer) -> M unit
-
-let MEMw_EA (addr,size) = write_mem_ea Write_plain addr size
-let MEMw_EA_cond (addr,size) = write_mem_ea Write_conditional addr size
-
-
-val MEMw' : (vector bitU * integer * vector bitU) -> M unit
-val MEMw_conditional' : (vector bitU * integer * vector bitU) -> M bitU
-
-let MEMw' (_,_,value) = write_mem_val value >>= fun _ -> return ()
-let MEMw_conditional' (_,_,value) = write_mem_val value >>= fun b -> return (bool_to_bitU b)
-
-
-val I_Sync : unit -> M unit
-val H_Sync : unit -> M unit
-val LW_Sync : unit -> M unit
-val EIEIO_Sync : unit -> M unit
-
-let I_Sync () = barrier Barrier_Isync
-let H_Sync () = barrier Barrier_Sync
-let LW_Sync () = barrier Barrier_LwSync
-let EIEIO_Sync () = barrier Barrier_Eieio
-
-let recalculate_dependency () = footprint
-
-let trap () = exit "error"
-(* this needs to change, but for that we'd have to make the type checker know about trap
- * as an effect *)
-
-val countLeadingZeroes : vector bitU * integer -> integer
-let countLeadingZeroes (Vector bits _ _ ,n) =
- let (_,bits) = List.splitAt (natFromInteger n) bits in
- integerFromNat (List.length (takeWhile ((=) B0) bits))
-
-
-let duplicate (bit,length) =
- Vector (List.replicate (natFromInteger length) bit) 0 true