Hypervisor extension

model/riscv_hext_regs.sail

@@ -5,3 +5,293 @@
 /*                                                                                       */
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
+
+/* Current Virtualization Mode */
+
+register cur_virtualization : Virtualization
+
+/* Hypervisor Status Register */
+
+bitfield Hstatus : xlenbits = {
+  /* VSXL only exists if HSXLEN == 64 so it's modelled via
+   * explicit an getter and setter below. */
+  /* VSXL : 33 .. 32 */
+  VTSR  : 22,
+  VTW   : 21,
+  VTVM  : 20,
+  VGEIN : 17 .. 12,
+  HU    : 9,
+  SPVP  : 8,
+  SPV   : 7,
+  GVA   : 6,
+  VSBE  : 5
+}
+register hstatus : Hstatus
+
+function get_hstatus_VSXL(h : Hstatus) -> arch_xlen = {
+  if sizeof(xlen) == 32
+  then arch_to_bits(RV32)
+  else h.bits[33 .. 32]
+}
+
+function set_hstatus_VSXL(h : Hstatus, a : arch_xlen) -> Hstatus = {
+  if sizeof(xlen) == 32
+  then h
+  else Mk_Hstatus([h.bits with 33..32 = a])
+}
+
+function legalize_hstatus(o : Hstatus, v : xlenbits) -> Hstatus = {
+  let v = Mk_Hstatus(v);
+
+  let h = [Mk_Hstatus(zeros()) with
+    VTSR = v[VTSR],
+    VTW = v[VTW],
+    VTVM = v[VTVM],
+    VGEIN = v[VGEIN], /* Note: 0 <= hstatus.VGEIN <= GEILEN */
+    HU = v[HU],
+    SPVP = v[SPVP],
+    SPV = v[SPV],
+    GVA = v[GVA],
+    VSBE = v[VSBE]
+  ];
+
+  /* Dynamic XLEN changes are not (yet) supported */
+  let h = set_hstatus_VSXL(h, get_hstatus_VSXL(o));
+
+  h
+}
+
+/* Hypervisor Trap Delegation Registers */
+
+register hedeleg : Medeleg
+
+function legalize_hedeleg(o: Medeleg, v: xlenbits) -> Medeleg = {
+  let h = Mk_Medeleg(v);
+  /* Mask read-only zero bits */
+  let h = [h with SAMO_GPage_Fault  = 0b0];
+  let h = [h with Virtual_Instr     = 0b0];
+  let h = [h with Load_GPage_Fault  = 0b0];
+  let h = [h with Fetch_GPage_Fault = 0b0];
+  let h = [h with MEnvCall          = 0b0];
+  let h = [h with VSEnvCall         = 0b0];
+  let h = [h with SEnvCall          = 0b0];
+  h
+}
+
+register hideleg : Minterrupts
+
+function legalize_hideleg(h : Minterrupts, v : xlenbits) -> Minterrupts = {
+  let v = Mk_Minterrupts(v);
+  /* VS-level interrupts can be delegated */
+  let h = [h with VSEI = v[VSEI]];
+  let h = [h with VSTI = v[VSTI]];
+  let h = [h with VSSI = v[VSSI]];
+  /* Other interrupts can't be delegated to VS-mode */
+  h
+}
+
+/* Hypervisor Interrupt enable/pending registers */
+
+/*! Returns new mip from the previous mip (m) and the written hvip (v) */
+function legalize_hvip(m: Minterrupts, v : xlenbits) -> Minterrupts = {
+  let v = Mk_Minterrupts(v);
+  let m = [m with VSEI = v[VSEI]];
+  let m = [m with VSTI = v[VSTI]];
+  let m = [m with VSSI = v[VSSI]];
+  // TODO: Hook to update non-standard portion
+  m
+}
+
+/*! Returns hvip view of mip (m) */
+function lower_mip_to_hvip(m : Minterrupts) -> Minterrupts = {
+  let h = Mk_Minterrupts(zeros());
+  let h = [h with VSEI = m[VSEI]];
+  let h = [h with VSTI = m[VSTI]];
+  let h = [h with VSSI = m[VSSI]];
+  // TODO: Hook to read non-standard portion
+  h
+}
+
+/*! Returns new mip from the previous mip (m) and the written hip (v) */
+function legalize_hip(m : Minterrupts, v : xlenbits) -> Minterrupts = {
+  let v = Mk_Minterrupts(v);
+  let m = [m with VSSI = v[VSSI]];
+  // TODO: Hook to update non-standard portion
+  m
+}
+
+/*! Returns hip view of mip (m) */
+function lower_mip_to_hip(m : Minterrupts) -> Minterrupts = {
+  let h = Mk_Minterrupts(zeros());
+  let h = [h with SGEI = m[SGEI]];
+  let h = [h with VSEI = m[VSEI]];
+  let h = [h with VSTI = m[VSTI]];
+  let h = [h with VSSI = m[VSSI]];
+  // TODO: Hook to read non-standard portion
+  h
+}
+
+/*! Returns new mie from the previous mie (m) and the written hie (v) */
+function legalize_hie(m : Minterrupts, v : xlenbits) -> Minterrupts = {
+  let v = Mk_Minterrupts(v);
+  let m = [m with SGEI = v[SGEI]];
+  let m = [m with VSEI = v[VSEI]];
+  let m = [m with VSTI = v[VSTI]];
+  let m = [m with VSSI = v[VSSI]];
+  /* Note: Writable bits in sie are read-only zero in hie */
+  // TODO: Hook to update non-standard portion
+  m
+}
+
+/*! Returns hie view of mie */
+function lower_mie_to_hie(m : Minterrupts) -> Minterrupts = {
+  let h = Mk_Minterrupts(zeros());
+  let h = [h with SGEI = m[SGEI]];
+  let h = [h with VSEI = m[VSEI]];
+  let h = [h with VSTI = m[VSTI]];
+  let h = [h with VSSI = m[VSSI]];
+  /* Note: Writable bits in sie are read-only zero in hie */
+  // TODO: Hook to read non-standard portion
+  h
+}
+
+/* Hypervisor Guest External Interrupts */
+
+register hgeie : xlenbits
+register hgeip : xlenbits
+
+// FIXME: hgeip should be written by interrupt controller
+// TODO: hip.SGEI is 1 if bitwise and of hgeip and hgeie is nonzero in any bit
+// TODO: hip.VSEI is 1 if hgeip[hstatus.VGEIN] is 1
+
+function legalize_hgeie(v : xlenbits) -> xlenbits = {
+  [v with 0 = bitzero]
+}
+
+/* Hypervisor environment configuration register */
+
+bitfield HEnvcfg : bits(64) = {
+  // Supervisor TimeCmp Extension
+  STCE   : 63,
+  // Page Based Memory Types Extension
+  PBMTE  : 62,
+  // Reserved WPRI bits.
+  wpri_1 : 61 .. 8,
+  // Cache Block Zero instruction Enable
+  CBZE   : 7,
+  // Cache Block Clean and Flush instruction Enable
+  CBCFE  : 6,
+  // Cache Block Invalidate instruction Enable
+  CBIE   : 5 .. 4,
+  // Reserved WPRI bits.
+  wpri_0 : 3 .. 1,
+  // Fence of I/O implies Memory
+  FIOM   : 0,
+}
+register henvcfg : HEnvcfg
+
+function legalize_henvcfg(o : HEnvcfg, v : bits(64)) -> HEnvcfg = {
+  let v = Mk_HEnvcfg(v);
+  let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
+  // Other extensions are not implemented yet so all other fields are read only zero.
+  o
+}
+
+/* Hypervisor hpm-related registers */
+
+register hcounteren : Counteren
+
+function legalize_hcounteren(c : Counteren, v : xlenbits) -> Counteren = {
+  /* no HPM counters yet */
+  [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]]
+}
+
+register htimedelta : bits(64)
+
+/* Machine & Hypervisor trap information */
+
+register mtinst : xlenbits
+register mtval2 : xlenbits
+
+register htinst : xlenbits
+register htval  : xlenbits
+
+/* Hypervisor Guest Address Translation and Protection */
+
+// TODO: Second Level Address Translation
+
+/* Virtual Supervisor Status Register */
+
+register vsstatus : Sstatus
+
+function legalize_vsstatus(vs: Sstatus, v: xlenbits) -> Sstatus = {
+  let m = Mk_Mstatus(vs.bits);    /* Convert to Mstatus   */
+  let s = legalize_sstatus(m, v); /* Legalize Mstatus for sstatus */
+  Mk_Sstatus(s.bits)              /* Convert back to Sstatus  */
+}
+
+/* Virtual Supervisor Trap Vector Base Address Register */
+
+register vstvec : Mtvec
+
+/* Virtual Supervisor Scratch Register */
+
+register vsscratch : xlenbits
+
+/* Virtual Supervisor Exception Program Counter */
+
+register vsepc : xlenbits
+
+/* Virtual Supervisor Cause Register */
+
+register vscause : Mcause
+
+/* Virtual Supervisor Trap Value Register */
+
+register vstval : xlenbits
+
+/* Virtual Supervisor interrupt enable/pending registers */
+
+/*! Returns new mip from the previous mip (m) and the written vsip (v) as delegated by hideleg (d) */
+function legalize_vsip(m: Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
+  let v = Mk_Minterrupts(v);
+  /* Since S-mode bits in vsip are aliases for their corresponding VS-mode bits
+     in hip when delegated by hideleg, only vsip.SSIP (hip.VSSIP) might be writable */
+  let m = [m with VSSI = v[SSI] & d[VSSI]];
+  m
+}
+
+/*! Returns vsip view of mip (m) as delegated by hideleg (d) */
+function lower_mip_to_vsip(m : Minterrupts, d : Minterrupts) -> Minterrupts = {
+  let vs = Mk_Minterrupts(zeros());
+  /* Standard S-mode bits in vsip are aliases of corresponding VS-mode bits in
+     hip if delegated by hideleg */
+  let vs = [vs with SEI = m[VSEI] & d[VSEI]];
+  let vs = [vs with STI = m[VSTI] & d[VSTI]];
+  let vs = [vs with SSI = m[VSSI] & d[VSSI]];
+  vs
+}
+
+/*! Returns new mie from previous mie (m) and the written vsie (v) as delegated by hideleg (d) */
+function legalize_vsie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
+  let v = Mk_Minterrupts(v);
+  let m = [m with VSEI = v[SEI] & d[VSEI]];
+  let m = [m with VSTI = v[STI] & d[VSTI]];
+  let m = [m with VSSI = v[SSI] & d[VSSI]];
+  m
+}
+
+/*! Returns vsie view of mie (m) as delegated by hideleg (d) */
+function lower_mie_to_vsie(m : Minterrupts, d : Minterrupts) -> Minterrupts = {
+  let vs = Mk_Minterrupts(zeros());
+  /* Standard S-mode bits in vsie are aliases of corresponding VS-mode bits in
+    hie if delegated by hideleg */
+  let vs = [vs with SEI = m[VSEI] & d[VSEI]];
+  let vs = [vs with STI = m[VSTI] & d[VSTI]];
+  let vs = [vs with SSI = m[VSSI] & d[VSSI]];
+  vs
+}
+
+/* Virtual Supervisor address translation & Protection */
+
+register vsatp : xlenbits

model/riscv_insts_zicsr.sail

@@ -30,15 +30,15 @@ function clause read_CSR(0xF12) = marchid
 function clause read_CSR(0xF13) = mimpid
 function clause read_CSR(0xF14) = mhartid
 function clause read_CSR(0xF15) = mconfigptr
-function clause read_CSR(0x300) = mstatus.bits
+function clause read_CSR(0x300) = mstatus.bits[xlen - 1 .. 0]
 function clause read_CSR(0x301) = misa.bits
 function clause read_CSR(0x302) = medeleg.bits
 function clause read_CSR(0x303) = mideleg.bits
 function clause read_CSR(0x304) = mie.bits
 function clause read_CSR(0x305) = get_mtvec()
 function clause read_CSR(0x306) = zero_extend(mcounteren.bits)
 function clause read_CSR(0x30A) = menvcfg.bits[xlen - 1 .. 0]
-function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
+function clause read_CSR(0x310 if xlen == 32) = mstatus.bits[63 .. 32]
 function clause read_CSR(0x31A if xlen == 32) = menvcfg.bits[63 .. 32]
 function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits)
 
@@ -73,7 +73,7 @@ function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if xlen == 32 &
 function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have any trigger support */
 
 /* supervisor mode */
-function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
+function clause read_CSR(0x100) = lower_mstatus(mstatus).bits[(xlen - 1) .. 0]
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
 function clause read_CSR(0x105) = get_stvec()
 function clause read_CSR(0x106) = zero_extend(scounteren.bits)
@@ -101,7 +101,8 @@ function clause read_CSR(0b1100100 /* 0xC80 */ @ index : bits(5) if xlen == 32 &
 function clause read_CSR(0x015) = read_seed_csr()
 
 /* machine mode */
-function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
+function clause write_CSR((0x300, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, mstatus.bits[63 .. 32] @ value); mstatus.bits[31 .. 0] }
+function clause write_CSR((0x300, value) if xlen == 64) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
 function clause write_CSR(0x302, value) = { medeleg = legalize_medeleg(medeleg, value); medeleg.bits }
 function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
@@ -110,7 +111,7 @@ function clause write_CSR(0x305, value) = { set_mtvec(value) }
 function clause write_CSR(0x306, value) = { mcounteren = legalize_mcounteren(mcounteren, value); zero_extend(mcounteren.bits) }
 function clause write_CSR((0x30A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); menvcfg.bits[31 .. 0] }
 function clause write_CSR((0x30A, value) if xlen == 64) = { menvcfg = legalize_menvcfg(menvcfg, value); menvcfg.bits }
-function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now
+function clause write_CSR((0x310, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, value @ mstatus.bits[31 .. 0]); mstatus.bits[63 .. 32] }
 function clause write_CSR((0x31A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); menvcfg.bits[63 .. 32] }
 function clause write_CSR(0x320, value) = { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); zero_extend(mcountinhibit.bits) }
 function clause write_CSR(0x340, value) = { mscratch = value; mscratch }
@@ -159,7 +160,7 @@ function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if xl
 function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
 
 /* supervisor mode */
-function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
+function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits[(xlen - 1) .. 0] }
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
 function clause write_CSR(0x105, value) = { set_stvec(value) }
 function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) }

model/riscv_sys_control.sail

@@ -444,10 +444,8 @@ function init_sys() -> unit = {
   mstatus[MPP] = privLevel_to_bits(lowest_supported_privLevel());
 
   /* set to little-endian mode */
-  if xlen == 64 then {
-    mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00])
-  };
-  mstatush.bits = zeros();
+  mstatus[MBE] = 0b0;
+  mstatus[SBE] = 0b0;
 
   mip.bits     = zeros();
   mie.bits     = zeros();