From 7f0591ddd659fa2dc18a84c0c4d011a5a0614c48 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Thu, 18 Apr 2024 00:04:23 -0700
Subject: [PATCH] Formatting fixes and corrections based on review

---
 model/riscv_insts_aext.sail  |  4 ++--
 model/riscv_insts_base.sail  |  6 +++---
 model/riscv_sys_control.sail | 10 +++-------
 model/riscv_types.sail       |  4 ++--
 4 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 8155c8024..657739269 100644
--- a/model/riscv_insts_aext.sail
+++ b/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 }
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 3197b7329..a09c311eb 100644
--- a/model/riscv_insts_base.sail
+++ b/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)) = {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 61740776a..98904f5f5 100644
--- a/model/riscv_sys_control.sail
+++ b/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]);
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index c7b10dbf4..05883b7ad 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -389,7 +389,7 @@ 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} = {
@@ -397,7 +397,7 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8, 16} = {
   HALF   <-> 2,
   WORD   <-> 4,
   DOUBLE <-> 8,
-  QUAD   <-> 16
+  QUAD   <-> 16,
 }
 
 /*!