summaryrefslogtreecommitdiff
path: root/aarch64_small/armV8_A64_sys_regs.sail
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64_small/armV8_A64_sys_regs.sail')
-rw-r--r--aarch64_small/armV8_A64_sys_regs.sail292
1 files changed, 292 insertions, 0 deletions
diff --git a/aarch64_small/armV8_A64_sys_regs.sail b/aarch64_small/armV8_A64_sys_regs.sail
new file mode 100644
index 00000000..b051c87d
--- /dev/null
+++ b/aarch64_small/armV8_A64_sys_regs.sail
@@ -0,0 +1,292 @@
+/*========================================================================*/
+/* */
+/* Copyright (c) 2015-2017 Shaked Flur */
+/* Copyright (c) 2015-2017 Kathyrn Gray */
+/* All rights reserved. */
+/* */
+/* This software was developed by the University of Cambridge Computer */
+/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */
+/* (REMS) project, funded by EPSRC grant EP/K008528/1. */
+/* */
+/* Redistribution and use in source and binary forms, with or without */
+/* modification, are permitted provided that the following conditions */
+/* are met: */
+/* 1. Redistributions of source code must retain the above copyright */
+/* notice, this list of conditions and the following disclaimer. */
+/* 2. Redistributions in binary form must reproduce the above copyright */
+/* notice, this list of conditions and the following disclaimer in */
+/* the documentation and/or other materials provided with the */
+/* distribution. */
+/* */
+/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */
+/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */
+/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */
+/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */
+/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */
+/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */
+/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */
+/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */
+/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */
+/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */
+/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */
+/* SUCH DAMAGE. */
+/*========================================================================*/
+
+/*************************************************************************/
+/* General system control registers */
+
+
+bitfield HCR_type : bits(64) =
+{
+ /*RES0 : 63..34,*/
+ ID : 33,
+ CD : 32,
+ RW : 31,
+ TRVM : 30,
+ HCD : 29,
+ TDZ : 28,
+ TGE : 27,
+ TVM : 26,
+ TTLB : 25,
+ TPU : 24,
+ TPC : 23,
+ TSW : 22,
+ TACR : 21,
+ TIDCP : 20,
+ TSC : 19,
+ TID3 : 18,
+ TID2 : 17,
+ TID1 : 16,
+ TID0 : 15,
+ TWE : 14,
+ TWI : 13,
+ DC : 12,
+ BSU : 11..10,
+ FB : 9,
+ VSE : 8,
+ VI : 7,
+ VF : 6,
+ AMO : 5,
+ IMO : 4,
+ FMO : 3,
+ PTW : 2,
+ SWIO : 1,
+ VM : 0,
+}
+register HCR_EL2 : HCR_type /* Hypervisor Configuration Register */
+
+
+bitfield ID_AA64MMFR0_type : bits(64) =
+{
+ /*RES0 : 63..32,*/
+ TGran4 : 31..28,
+ TGran64 : 27..24,
+ TGran16 : 23..20,
+ BigEndEL0 : 19..16,
+ SNSMem : 15..12,
+ BigEnd : 11..8,
+ ASIDBits : 7..4,
+ PARange : 3..0,
+}
+register ID_AA64MMFR0_EL1 : ID_AA64MMFR0_type /* AArch64 Memory Model Feature Register 0 */
+
+register RVBAR_EL1 : bits(64) /* Reset Vector Base Address Register (if EL2 and EL3 not implemented) */
+register RVBAR_EL2 : bits(64) /* Reset Vector Base Address Register (if EL3 not implemented) */
+register RVBAR_EL3 : bits(64) /* Reset Vector Base Address Register (if EL3 implemented) */
+
+bitfield SCRType : bits(32) =
+{
+ /*RES0 : 31..14,*/
+ TWE : 13,
+ TWI : 12,
+ ST : 11,
+ RW : 10,
+ SIF : 9,
+ HCE : 8,
+ SMD : 7,
+ /*RES0 : 6,*/
+ /*RES1 : 5..4,*/
+ EA : 3,
+ FIQ : 2,
+ IRQ : 1,
+ NS : 0,
+}
+register SCR_EL3 : SCRType /* Secure Configuration Register */
+
+bitfield SCTLR_EL1_type : bits(32) =
+{
+ /*RES0 : 31..30,*/
+ /*RES1 : 29..28,*/
+ /*RES0 : 27,*/
+ UCI : 26,
+ EE : 25,
+ E0E : 24,
+ /*RES1 : 23..22,*/
+ /*RES0 : 21,*/
+ /*RES1 : 20,*/
+ WXN : 19,
+ nTWE : 18,
+ /*RES0 : 17,*/
+ nTWI : 16,
+ UCT : 15,
+ DZE : 14,
+ /*RES0 : 13,*/
+ I : 12,
+ /*RES1 : 11,*/
+ /*RES0 : 10,*/
+ UMA : 9,
+ SED : 8,
+ ITD : 7,
+ /*RES0 : 6,*/
+ CP15BEN : 5,
+ SA0 : 4,
+ SA : 3,
+ C : 2,
+ A : 1,
+ M : 0,
+}
+register SCTLR_EL1 : SCTLR_EL1_type /* System Control Register (EL1) */
+
+bitfield SCTLR_type : bits(32) =
+{
+ /*RES0 : 31..30,*/
+ /*RES1 : 29..28,*/
+ /*RES0 : 27..26,*/
+ EE : 25,
+ /*RES0 : 24,*/
+ /*RES1 : 23..22,*/
+ /*RES0 : 21..20,*/
+ WXN : 19,
+ /*RES1 : 18,*/
+ /*RES0 : 17,*/
+ /*RES1 : 16,*/
+ /*RES0 : 15..13,*/
+ I : 12,
+ /*RES1 : 11,*/
+ /*RES0 : 10..6,*/
+ /*RES1 : 5..4,*/
+ SA : 3,
+ C : 2,
+ A : 1,
+ M : 0,
+}
+register SCTLR_EL2 : SCTLR_type /* System Control Register (EL2) */
+register SCTLR_EL3 : SCTLR_type /* System Control Register (EL3) */
+
+bitfield TCR_EL1_type : bits(64) =
+{
+ /*RES0 : 63..39,*/
+ TBI1 : 38,
+ TBI0 : 37,
+ AS : 36,
+ /*RES0 : 35,*/
+ IPS : 34..32,
+ TG1 : 31..30,
+ SH1 : 29..28,
+ ORGN1 : 27..26,
+ IRGN1 : 25..24,
+ EPD1 : 23,
+ A1 : 22,
+ T1SZ : 21..16,
+ TG0 : 15..14,
+ SH0 : 13..12,
+ ORGN0 : 11..10,
+ IRGN0 : 9..8,
+ EPD0 : 7,
+ /*RES0 : 6,*/
+ T0SZ : 5..0,
+}
+register TCR_EL1 : TCR_EL1_type /* Translation Control Register (EL1) */
+
+bitfield TCR_type : bits(32) =
+{
+ /*RES1 : 31,*/
+ /*RES0 : 30..24,*/
+ /*RES1 : 23,*/
+ /*RES0 : 22..21,*/
+ TBI : 20,
+ /*RES0 : 19,*/
+ PS : 18..16,
+ TG0 : 15..14,
+ SH0 : 13..12,
+ ORGN0 : 11..10,
+ IRGN0 : 9..8,
+ /*RES0 : 7..6,*/
+ T0SZ : 5..0,
+}
+register TCR_EL2 : TCR_type /* Translation Control Register (EL2) */
+register TCR_EL3 : TCR_type /* Translation Control Register (EL3) */
+
+register TPIDR_EL0 : bits(64) /* EL0 Read/Write Software Thread ID Register */
+register TPIDR_EL1 : bits(64) /* EL1 Read/Write Software Thread ID Register */
+register TPIDR_EL2 : bits(64) /* EL2 Read/Write Software Thread ID Register */
+register TPIDR_EL3 : bits(64) /* EL3 Read/Write Software Thread ID Register */
+
+/*************************************************************************/
+/* Debug registers */
+
+bitfield DBGPRCR_type : bits(32) =
+{
+ /*RES0 : 31..1,*/
+ CORENPDRQ : 0,
+}
+register DBGPRCR_EL1 : DBGPRCR_type /* Debug Power Control Register */
+
+bitfield OSDLR_type : bits(32) =
+{
+ /*RES0 : 31..1,*/
+ DLK : 0,
+}
+register OSDLR_EL1 : OSDLR_type /* OS Double Lock Register */
+
+/*************************************************************************/
+/* Performance Monitors registers */
+
+/*************************************************************************/
+/* Generic Timer registers */
+
+/*************************************************************************/
+/* Generic Interrupt Controller CPU interface registers */
+
+/*************************************************************************/
+/* External Debug Register */
+
+bitfield EDSCR_type : bits(32) =
+{
+ /*RES0 : 31,*/
+ RXfull : 30,
+ TXfull : 29,
+ ITO : 28,
+ RXO : 27,
+ TXU : 26,
+ PipeAdv : 25,
+ ITE : 24,
+ INTdis : 23..22,
+ TDA : 21,
+ MA : 20,
+ /*RES0 : 19,*/
+ NS : 18,
+ /*RES0 : 17,*/
+ SDD : 16,
+ /*RES0 : 15,*/
+ HDE : 14,
+ RW : 13..10,
+ EL : 9..8,
+ A : 7,
+ ERR : 6,
+ STATUS : 5..0,
+}
+register EDSCR : EDSCR_type /* External Debug Status and Control Register */
+
+/* transactional memory, not part of the official spec */
+bitfield TXIDR_EL0_type : bits(64) =
+{
+ /*RES0 : 63..8,*/
+ DEPTH : 7..0,
+}
+register TXIDR_EL0 : TXIDR_EL0_type /* Transaction ID Register */
+
+
+val AArch64_ResetControlRegisters : boolean -> unit effect pure
+function AArch64_ResetControlRegisters(cold_reset) = ()
+