diff options
| author | Alasdair Armstrong | 2018-07-09 17:44:07 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-07-09 17:56:25 +0100 |
| commit | b71a0574ee9b9ae1d80e91a13915b16fbdf0f405 (patch) | |
| tree | ba6dc0c8050fac129671819360e47d116573bd6e /aarch64 | |
| parent | c2b19f7a89df122daf56b22fa25a53202eddaab0 (diff) | |
Add no_devices.sail to be compatible with latest AArch64 prelude and
update aarch64 model
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/full.sail | 1 | ||||
| -rw-r--r-- | aarch64/no_devices.sail | 35 | ||||
| -rw-r--r-- | aarch64/no_vector.sail | 1 |
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" |