diff options
Diffstat (limited to 'src/gen_lib/power_extras.lem')
| -rw-r--r-- | src/gen_lib/power_extras.lem | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem index f2941aff..8515a406 100644 --- a/src/gen_lib/power_extras.lem +++ b/src/gen_lib/power_extras.lem @@ -1,4 +1,5 @@ open import Pervasives +open import Vector open import State open import Sail_values @@ -33,3 +34,13 @@ let H_Sync () = return () let LW_Sync () = return () let EIEIO_Sync () = return () +let recalculate_dependency () = return () + +let trap () = () +(* this needs to change, but for that we'd have to make the type checker know about trap + * as an effect *) + +val countLeadingZeroes : vector bit * integer -> integer +let countLeadingZeroes (V bits _ _ ,n) = + let (_,bits) = List.splitAt (natFromInteger n) bits in + integerFromNat (List.length (takeWhile ((=) O) bits)) |