diff options
| author | Alasdair | 2020-07-31 13:30:53 +0100 |
|---|---|---|
| committer | Alasdair | 2020-07-31 13:30:53 +0100 |
| commit | dd76fdfd819bb1a5423cea369df0e7f2ae449b62 (patch) | |
| tree | 88d8d69e39b724902b280beaa8ce874e444f5dbc /power/power_extras_embed_sequential.lem | |
| parent | 71db59830383b7db5316b5c99ccebe776fc837dc (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.lem | 50 |
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 |
