diff options
| author | Kathy Gray | 2014-08-18 18:43:14 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-08-18 18:43:14 +0100 |
| commit | 3c86cf03071bef70c1909b13dcb1db28f8cd5c33 (patch) | |
| tree | 01d6230242279088bde252c6323e80193a1029c6 /src/test/power.sail | |
| parent | 9f2ec1fcb16191ad9c54f68152f03ca80f85522e (diff) | |
Handling many register reads, writes, and memory reads.
There are problems that warrant discussion about handling special registers that hold records or data structures previously.
Diffstat (limited to 'src/test/power.sail')
| -rw-r--r-- | src/test/power.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/test/power.sail b/src/test/power.sail index 5f1f532b..9a89c9e4 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -333,8 +333,8 @@ register (bit[64]) NIA (* next instruction address *) register (bit[64]) CIA (* current instruction address *) -val extern forall Nat 'n. ( nat , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw -val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr (* XXX effect for trap? *) val extern unit -> unit effect pure trap |