summaryrefslogtreecommitdiff
path: root/aarch64
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64')
-rw-r--r--aarch64/full.sail1
-rw-r--r--aarch64/no_devices.sail35
-rw-r--r--aarch64/no_vector.sail1
3 files changed, 37 insertions, 0 deletions
diff --git a/aarch64/full.sail b/aarch64/full.sail
index b05b1829..b02b8333 100644
--- a/aarch64/full.sail
+++ b/aarch64/full.sail
@@ -1,6 +1,7 @@
// Prelude
$include "prelude.sail"
+$include "no_devices.sail"
// Specification
$include "full/spec.sail"
diff --git a/aarch64/no_devices.sail b/aarch64/no_devices.sail
new file mode 100644
index 00000000..882aa6b3
--- /dev/null
+++ b/aarch64/no_devices.sail
@@ -0,0 +1,35 @@
+
+val ___WriteRAM = "write_ram" : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem}
+
+val __InitRAM : forall 'm. (atom('m), int, bits('m), bits(8)) -> unit
+
+function __InitRAM (_, _, _, _) = ()
+
+val ___ReadRAM = "read_ram" : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+function __ReadRAM(addr_length, bytes, hex_ram, addr) =
+{
+ ___ReadRAM(addr_length, bytes, hex_ram, addr)
+}
+
+val __TraceMemoryWrite : forall 'n 'm.
+ (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+val __WriteRAM : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem}
+
+function __WriteRAM(addr_length, bytes, hex_ram, addr, data) =
+{
+ ___WriteRAM(addr_length, bytes, hex_ram, addr, data)
+}
+
+function __TraceMemoryWrite(bytes, addr, data) = ()
+
+val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+function __TraceMemoryRead(bytes, addr, data) = () \ No newline at end of file
diff --git a/aarch64/no_vector.sail b/aarch64/no_vector.sail
index 61fc7b4f..6c96d070 100644
--- a/aarch64/no_vector.sail
+++ b/aarch64/no_vector.sail
@@ -1,6 +1,7 @@
// Prelude
$include "prelude.sail"
+$include "no_devices.sail"
// Specification
$include "no_vector/spec.sail"