diff options
| author | Christopher Pulte | 2016-10-11 08:18:22 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-10-11 08:18:22 +0100 |
| commit | fd67067a8adc95617a70152f8a896016d210d604 (patch) | |
| tree | b157095dd802cc473a57a1033fbf4870bf75177e /src/gen_lib/power_extras.lem | |
| parent | 966daf663e0e5c816f5d2dad2a181e27bfcb7148 (diff) | |
move armv8_extras and power_extras to idl/power and idlarm, fixes
Diffstat (limited to 'src/gen_lib/power_extras.lem')
| -rw-r--r-- | src/gen_lib/power_extras.lem | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem deleted file mode 100644 index c16b197f..00000000 --- a/src/gen_lib/power_extras.lem +++ /dev/null @@ -1,47 +0,0 @@ -open import Pervasives -open import Sail_impl_base -open import Vector -open import Sail_values -open import Prompt - -val MEMr : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) -val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) - -let MEMr (addr,size) = read_memory Read_plain addr size -let MEMr_reserve (addr,size) = read_memory Read_reserve addr size - - -val MEMw_EA : forall 'e. (vector bitU * integer) -> M 'e unit -val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit - -let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size -let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size - - -val MEMw : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit -val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU - -let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return () -let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b) - - -val I_Sync : forall 'e. unit -> M 'e unit -val H_Sync : forall 'e. unit -> M 'e unit -val LW_Sync : forall 'e. unit -> M 'e unit -val EIEIO_Sync : forall 'e. unit -> M 'e unit - -let I_Sync () = barrier Isync -let H_Sync () = barrier Sync -let LW_Sync () = barrier LwSync -let EIEIO_Sync () = 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 ((=) O) bits)) |