summaryrefslogtreecommitdiff
path: root/test/typecheck
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-07-25 15:06:23 +0100
committerAlasdair Armstrong2017-07-25 15:06:23 +0100
commit3ff8009f1dc81593a972eb2050f7e1159aba718a (patch)
tree6cad4b9def8550d02fb67032a6598c3985ddfc19 /test/typecheck
parent5c306614427179282c8747a6fa6c34637c64ca68 (diff)
Improved l-expressions
- Fixed a bug where some l-expressions which wrote registers wern't picking up register writes. - Can now write to registers with record types. e.g. ARM's ProcState record from ASL.
Diffstat (limited to 'test/typecheck')
-rw-r--r--test/typecheck/fail/procstate1.sail16
-rw-r--r--test/typecheck/pass/arm_FPEXC1.sail53
-rw-r--r--test/typecheck/pass/procstate1.sail16
3 files changed, 85 insertions, 0 deletions
diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail
new file mode 100644
index 00000000..00dc1ab1
--- /dev/null
+++ b/test/typecheck/fail/procstate1.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+typedef ProcState = const struct forall Num 'n.
+{
+ bit['n] N;
+ bit[1] Z;
+ bit[1] C;
+ bit[1] V
+}
+
+register ProcState<2> PSTATE
+
+function unit test () =
+{
+ PSTATE.N := 0b1
+}
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
new file mode 100644
index 00000000..cfae86a1
--- /dev/null
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -0,0 +1,53 @@
+default Order dec
+
+val forall Num 'n. (bit['n], int) -> bit effect pure vector_access
+
+val forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1.
+ (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange
+
+register vector<32 - 1, 32, dec, bit> _FPEXC32_EL2
+
+val vector<32 - 1, 32, dec, bit> -> unit effect {wreg} set_FPEXC32_EL2
+
+function set_FPEXC32_EL2 value_name =
+ {
+ _FPEXC32_EL2[0..0] := [value_name[0]];
+ _FPEXC32_EL2[1..1] := [value_name[1]];
+ _FPEXC32_EL2[2..2] := [value_name[2]];
+ _FPEXC32_EL2[3..3] := [value_name[3]];
+ _FPEXC32_EL2[4..4] := [value_name[4]];
+ _FPEXC32_EL2[6..5] := value_name[6 .. 5];
+ _FPEXC32_EL2[7..7] := [value_name[7]];
+ _FPEXC32_EL2[20..11] := value_name[20 .. 11];
+ _FPEXC32_EL2[29..29] := [value_name[29]];
+ _FPEXC32_EL2[30..30] := [value_name[30]]
+ }
+
+val unit -> vector<32 - 1, 32, dec, bit> effect {rreg} get_FPEXC32_EL2
+
+function get_FPEXC32_EL2 () =
+ {
+ (vector<32 - 1, 32, dec, bit> ) value_name := 0x04000700;
+ value_name[0..0] := [_FPEXC32_EL2[0]];
+ value_name[1..1] := [_FPEXC32_EL2[1]];
+ value_name[2..2] := [_FPEXC32_EL2[2]];
+ value_name[3..3] := [_FPEXC32_EL2[3]];
+ value_name[4..4] := [_FPEXC32_EL2[4]];
+ value_name[6..5] := _FPEXC32_EL2[6 .. 5];
+ value_name[7..7] := [_FPEXC32_EL2[7]];
+ value_name[20..11] := _FPEXC32_EL2[20 .. 11];
+ value_name[26..26] := [_FPEXC32_EL2[26]];
+ value_name[29..29] := [_FPEXC32_EL2[29]];
+ value_name[30..30] := [_FPEXC32_EL2[30]];
+ value_name
+ }
+
+val vector<32 - 1, 32, dec, bit> -> unit effect {rreg, wreg} set_FPEXC
+
+function set_FPEXC val_name =
+ {
+ (vector<32 - 1, 32, dec, bit> ) r := val_name;
+ (vector<32 - 1, 32, dec, bit> ) __tmp_45 := get_FPEXC32_EL2();
+ __tmp_45[31..0] := r;
+ set_FPEXC32_EL2(__tmp_45)
+ }
diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail
new file mode 100644
index 00000000..95ba97db
--- /dev/null
+++ b/test/typecheck/pass/procstate1.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+typedef ProcState = const struct forall Num 'n.
+{
+ bit['n] N;
+ bit[1] Z;
+ bit[1] C;
+ bit[1] V
+}
+
+register ProcState<1> PSTATE
+
+function unit test () =
+{
+ PSTATE.N := 0b1
+}