Formatting fixes and corrections based on review

model/riscv_insts_aext.sail

@@ -69,7 +69,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
  HALF => vaddr[0..0] == 0b0,
  WORD => vaddr[1..0] == 0b00,
  DOUBLE => vaddr[2..0] == 0b000,
- QUAD => vaddr[4..0] == 0b00000
+ QUAD => vaddr[3..0] == 0b0000,
  };
  /* "LR faults like a normal load, even though it's in the AMO major opcode space."
  * - Andrew Waterman, isa-dev, 10 Jul 2018.
@@ -131,7 +131,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  HALF => vaddr[0..0] == 0b0,
  WORD => vaddr[1..0] == 0b00,
  DOUBLE => vaddr[2..0] == 0b000,
- QUAD => vaddr[4..0] == 0b00000
+ QUAD => vaddr[3..0] == 0b0000,
  };
  if not(aligned)
  then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }

model/riscv_insts_base.sail

@@ -318,9 +318,9 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
  else match width {
  BYTE => false,
  HALF => vaddr[0] == bitone,
- WORD => vaddr[0] == bitone | vaddr[1] == bitone,
- DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone,
- QUAD => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone | vaddr[3] == bitone
+ WORD => vaddr[1..0] != zeros(),
+ DOUBLE => vaddr[2..0] != zeros(),
+ QUAD => vaddr[3..0] != zeros(),
  }
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {

model/riscv_sys_control.sail

@@ -491,13 +491,9 @@ function init_sys() -> unit = {
  then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!");
 
  /* We currently support F, D and Q */
- misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */
- misa[D] = if sizeof(flen) >= 64
- then bool_to_bits(sys_enable_fdext()) /* double-precision */
- else 0b0;
- misa[Q] = if sizeof(flen) >= 128
- then bool_to_bits(sys_enable_fdext()) /* quad-precision */
- else 0b0;
+ misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */
+ misa[D] = bool_to_bits(sys_enable_fdext() & sizeof(flen) >= 64); /* double-precision */
+ misa[Q] = bool_to_bits(sys_enable_fdext() & sizeof(flen) >= 128); /* quad-precision */
 
  mstatus = set_mstatus_SXL(mstatus, misa[MXL]);
  mstatus = set_mstatus_UXL(mstatus, misa[MXL]);

model/riscv_types.sail

@@ -389,15 +389,15 @@ mapping size_mnemonic : word_width <-> string = {
  HALF <-> "h",
  WORD <-> "w",
  DOUBLE <-> "d",
- QUAD <-> "q"
+ QUAD <-> "q",
 }
 
 mapping size_bytes : word_width <-> {1, 2, 4, 8, 16} = {
  BYTE <-> 1,
  HALF <-> 2,
  WORD <-> 4,
  DOUBLE <-> 8,
- QUAD <-> 16
+ QUAD <-> 16,
 }
 
 /*!