summaryrefslogtreecommitdiff
path: root/aarch64_small/mono-splices/ASR_C.sail
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64_small/mono-splices/ASR_C.sail')
-rw-r--r--aarch64_small/mono-splices/ASR_C.sail8
1 files changed, 8 insertions, 0 deletions
diff --git a/aarch64_small/mono-splices/ASR_C.sail b/aarch64_small/mono-splices/ASR_C.sail
new file mode 100644
index 00000000..0a47d8d7
--- /dev/null
+++ b/aarch64_small/mono-splices/ASR_C.sail
@@ -0,0 +1,8 @@
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
+ (bits('N), int('S)) -> (bits('N), bit) effect {escape}
+
+function ASR_C (x, shift) = {
+ result : bits('N) = sail_arith_shiftright(x, shift);
+ carry_out : bit = if shift > 'N then x['N - 1] else x[shift - 1];
+ return((result, carry_out))
+}