diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/no_vector/spec.sail | 46 | ||||
| -rwxr-xr-x | aarch64/prelude.sail | 3 |
2 files changed, 24 insertions, 25 deletions
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index c91da297..149ddcd9 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -742,21 +742,21 @@ val __UNKNOWN_MemOp : unit -> MemOp function __UNKNOWN_MemOp () = return(MemOp_LOAD) -let MemHint_RWA : vector(2, dec, bit) = 0b11 +let MemHint_RWA : bits(2) = 0b11 -let MemHint_RA : vector(2, dec, bit) = 0b10 +let MemHint_RA : bits(2) = 0b10 -let MemHint_No : vector(2, dec, bit) = 0b00 +let MemHint_No : bits(2) = 0b00 val __UNKNOWN_MemBarrierOp : unit -> MemBarrierOp function __UNKNOWN_MemBarrierOp () = return(MemBarrierOp_DSB) -let MemAttr_WT : vector(2, dec, bit) = 0b10 +let MemAttr_WT : bits(2) = 0b10 -let MemAttr_WB : vector(2, dec, bit) = 0b11 +let MemAttr_WB : bits(2) = 0b11 -let MemAttr_NC : vector(2, dec, bit) = 0b00 +let MemAttr_NC : bits(2) = 0b00 val __UNKNOWN_MemAtomicOp : unit -> MemAtomicOp @@ -782,23 +782,23 @@ register MAIR_EL2 : bits(64) register MAIR_EL1 : bits(64) -let M32_User : vector(5, dec, bit) = 0b10000 +let M32_User : bits(5) = 0b10000 -let M32_Undef : vector(5, dec, bit) = 0b11011 +let M32_Undef : bits(5) = 0b11011 -let M32_System : vector(5, dec, bit) = 0b11111 +let M32_System : bits(5) = 0b11111 -let M32_Svc : vector(5, dec, bit) = 0b10011 +let M32_Svc : bits(5) = 0b10011 -let M32_Monitor : vector(5, dec, bit) = 0b10110 +let M32_Monitor : bits(5) = 0b10110 -let M32_IRQ : vector(5, dec, bit) = 0b10010 +let M32_IRQ : bits(5) = 0b10010 -let M32_Hyp : vector(5, dec, bit) = 0b11010 +let M32_Hyp : bits(5) = 0b11010 -let M32_FIQ : vector(5, dec, bit) = 0b10001 +let M32_FIQ : bits(5) = 0b10001 -let M32_Abort : vector(5, dec, bit) = 0b10111 +let M32_Abort : bits(5) = 0b10111 val __UNKNOWN_LogicalOp : unit -> LogicalOp @@ -1113,13 +1113,13 @@ register ELR_EL2 : bits(64) register ELR_EL1 : bits(64) -let EL3 : vector(2, dec, bit) = 0b11 +let EL3 : bits(2) = 0b11 -let EL2 : vector(2, dec, bit) = 0b10 +let EL2 : bits(2) = 0b10 -let EL1 : vector(2, dec, bit) = 0b01 +let EL1 : bits(2) = 0b01 -let EL0 : vector(2, dec, bit) = 0b00 +let EL0 : bits(2) = 0b00 register EDSCR : bits(32) @@ -1149,13 +1149,13 @@ function DecodeRegExtend op = match op { 0b111 => return(ExtendType_SXTX) } -let DebugHalt_Watchpoint : vector(6, dec, bit) = 0b101011 +let DebugHalt_Watchpoint : bits(6) = 0b101011 -let DebugHalt_HaltInstruction : vector(6, dec, bit) = 0b101111 +let DebugHalt_HaltInstruction : bits(6) = 0b101111 -let DebugHalt_Breakpoint : vector(6, dec, bit) = 0b000111 +let DebugHalt_Breakpoint : bits(6) = 0b000111 -let DebugException_VectorCatch : vector(4, dec, bit) = 0x5 +let DebugException_VectorCatch : bits(4) = 0x5 val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 21fcbe92..7bf0d9f9 100755 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -2,9 +2,8 @@ default Order dec $include <smt.sail> $include <arith.sail> -// $include <trace.sail> -type bits ('n : Int) = vector('n, dec, bit) +type bits ('n : Int) = bitvector('n, dec) val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool |