aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_sys_control.sail
diff options
context:
space:
mode:
authorPrashanth Mundkur <prashanth.mundkur@gmail.com>2020-01-07 17:09:57 -0800
committerPrashanth Mundkur <prashanth.mundkur@gmail.com>2020-01-07 17:09:57 -0800
commit778301c9a2f483523e83581d7cffb93effb75134 (patch)
tree3691b22682552587b8c50b3b63a32a366d6b3274 /model/riscv_sys_control.sail
parente15f302b12df29014c5dd6d19bbacf12be19ff4d (diff)
parentdfebc748f8a762718cfda1f1a1201debe754a9c6 (diff)
downloadsail-riscv-778301c9a2f483523e83581d7cffb93effb75134.zip
sail-riscv-778301c9a2f483523e83581d7cffb93effb75134.tar.gz
sail-riscv-778301c9a2f483523e83581d7cffb93effb75134.tar.bz2
Merge branch 'master' into rsnikhil.
Diffstat (limited to 'model/riscv_sys_control.sail')
-rw-r--r--model/riscv_sys_control.sail12
1 files changed, 12 insertions, 0 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 2886273..d906f5e 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -497,3 +497,15 @@ union MemoryOpResult ('a : Type) = {
MemValue : 'a,
MemException : ExceptionType
}
+
+val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta))
+function MemoryOpResult_add_meta(r, m) = match r {
+ MemValue(v) => MemValue(v, m),
+ MemException(e) => MemException(e)
+}
+
+val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t)
+function MemoryOpResult_drop_meta(r) = match r {
+ MemValue(v, m) => MemValue(v),
+ MemException(e) => MemException(e)
+}