Fix fcsr exception accrual for non-softfloat paths.

3 files changed, 92 insertions, 103 deletions

diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index b19538b..2ef310b 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -277,13 +277,26 @@ val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg}
 function ext_write_fcsr (frm, fflags) = {
   fcsr->FRM()    = frm;      /* Note: frm can be an illegal value, 101, 110, 111 */
   fcsr->FFLAGS() = fflags;
-  update_softfloat_fflags(fflags);  // specifically for softfloat
+  update_softfloat_fflags(fflags);
   dirty_fd_context();
 }
 
+/* called for softfloat paths (softfloat flags are consistent) */
 val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
 function write_fflags(fflags) = {
   if   fcsr.FFLAGS() != fflags
   then dirty_fd_context();
   fcsr->FFLAGS() = fflags;
 }
+
+/* called for non-softfloat paths (softfloat flags need updating) */
+val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg}
+function accrue_fflags(flags) = {
+  let f = fcsr.FFLAGS() | flags;
+  if  fcsr.FFLAGS() != f
+  then {
+    fcsr->FFLAGS() = f;
+    update_softfloat_fflags(f);
+    dirty_fd_context();
+  }
+}
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 9e68248..4fcf7b1 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -135,10 +135,9 @@ function feq_quiet_D   (v1,       v2) = {
 
   let result = ((v1 == v2) | (v1Is0 & v2Is0));
 
-  let fflags = if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then
-                 nvFlag()
-               else
-                 zeros();
+  let fflags = if   (f_is_SNaN_D(v1) | f_is_SNaN_D(v2))
+               then nvFlag()
+               else zeros();
 
   (result, fflags)
 }
@@ -153,30 +152,26 @@ function flt_D   (v1,       v2,        is_quiet) = {
 
   let result : bool =
     if (s1 == 0b0) & (s2 == 0b0) then
-      if (e1 == e2) then
-         unsigned (m1) < unsigned (m2)
-      else
-         unsigned (e1) < unsigned (e2)
+      if   (e1 == e2)
+      then unsigned (m1) < unsigned (m2)
+      else unsigned (e1) < unsigned (e2)
     else if (s1 == 0b0) & (s2 == 0b1) then
       false
     else if (s1 == 0b1) & (s2 == 0b0) then
       true
     else
-      if (e1 == e2) then
-        unsigned (m1) > unsigned (m2)
-      else
-        unsigned (e1) > unsigned (e2);
+      if   (e1 == e2)
+      then unsigned (m1) > unsigned (m2)
+      else unsigned (e1) > unsigned (e2);
 
   let fflags = if is_quiet then
-                 if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then
-                   nvFlag()
-                 else
-                   zeros()
+                 if   (f_is_SNaN_D(v1) | f_is_SNaN_D(v2))
+                 then nvFlag()
+                 else zeros()
                else
-                 if (v1IsNaN | v2IsNaN) then
-                   nvFlag()
-                 else
-                   zeros();
+                 if   (v1IsNaN | v2IsNaN)
+                 then nvFlag()
+                 else zeros();
 
   (result, fflags)
 }
@@ -194,30 +189,26 @@ function fle_D   (v1,       v2,        is_quiet) = {
 
   let result : bool =
     if (s1 == 0b0) & (s2 == 0b0) then
-      if (e1 == e2) then
-        unsigned (m1) <=  unsigned (m2)
-      else
-        unsigned (e1)  <  unsigned (e2)
+      if   (e1 == e2)
+      then unsigned (m1) <=  unsigned (m2)
+      else unsigned (e1)  <  unsigned (e2)
     else if (s1 == 0b0) & (s2 == 0b1) then
       (v1Is0 & v2Is0)                         /* Equal in this case (+0=-0) */
     else if (s1 == 0b1) & (s2 == 0b0) then
       true
     else
-      if (e1 == e2) then
-        unsigned (m1) >=  unsigned (m2)
-      else
-        unsigned (e1)  >  unsigned (e2);
+      if   (e1 == e2)
+      then unsigned (m1) >=  unsigned (m2)
+      else unsigned (e1)  >  unsigned (e2);
 
   let fflags = if is_quiet then
-                 if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then
-                   nvFlag()
-                 else
-                   zeros()
+                 if   (f_is_SNaN_D(v1) | f_is_SNaN_D(v2))
+                 then nvFlag()
+                 else zeros()
                else
-                 if (v1IsNaN | v2IsNaN) then
-                   nvFlag()
-                 else
-                   zeros();
+                 if   (v1IsNaN | v2IsNaN)
+                 then nvFlag()
+                 else zeros();
 
   (result, fflags)
 }
@@ -652,8 +643,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = {
   let (s1, e1, m1) = fsplit_D (rs1_val_D);
   let (s2, e2, m2) = fsplit_D (rs2_val_D);
   let rd_val_D     = fmake_D (s2, e1, m1);
-  let fflags       = 0b_00000;
-  write_fflags(fflags);
+
   F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
@@ -664,8 +654,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
   let (s1, e1, m1) = fsplit_D (rs1_val_D);
   let (s2, e2, m2) = fsplit_D (rs2_val_D);
   let rd_val_D     = fmake_D (0b1 ^ s2, e1, m1);
-  let fflags       = 0b_00000;
-  write_fflags(fflags);
+
   F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
@@ -676,8 +665,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = {
   let (s1, e1, m1) = fsplit_D (rs1_val_D);
   let (s2, e2, m2) = fsplit_D (rs2_val_D);
   let rd_val_D     = fmake_D (s1 ^ s2, e1, m1);
-  let fflags       = 0b_00000;
-  write_fflags(fflags);
+
   F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
@@ -700,7 +688,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
                   else if rs1_lt_rs2                                                then rs1_val_D
                   else /* (not rs1_lt_rs2) */                                            rs2_val_D;
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
@@ -723,7 +711,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
                   else if rs2_lt_rs1                                                then rs1_val_D
                   else /* (not rs2_lt_rs1) */                                            rs2_val_D;
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
@@ -740,7 +728,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
       else if rs1_eq_rs2                                        then EXTZ(0b1)
       else                                                           zeros();
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
@@ -758,7 +746,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
       else if rs1_lt_rs2                                        then EXTZ(0b1)
       else                                                           zeros();
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
@@ -776,7 +764,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
       else if rs1_le_rs2                                        then EXTZ(0b1)
       else                                                           zeros();
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 4b9e69e..280389a 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -164,10 +164,9 @@ function feq_quiet_S   (v1,       v2) = {
 
   let result = ((v1 == v2) | (v1Is0 & v2Is0));
 
-  let fflags = if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then
-                 nvFlag()
-               else
-                 zeros();
+  let fflags = if   (f_is_SNaN_S(v1) | f_is_SNaN_S(v2))
+               then nvFlag()
+               else zeros();
 
   (result, fflags)
 }
@@ -182,30 +181,26 @@ function flt_S   (v1,       v2,        is_quiet) = {
 
   let result : bool =
     if (s1 == 0b0) & (s2 == 0b0) then
-      if (e1 == e2) then
-        unsigned (m1) < unsigned (m2)
-      else
-        unsigned (e1) < unsigned (e2)
-    else if (s1 == 0b0) & (s2 == 0b1) then
-        false
-    else if (s1 == 0b1) & (s2 == 0b0) then
-        true
+      if   (e1 == e2)
+      then unsigned (m1) < unsigned (m2)
+      else unsigned (e1) < unsigned (e2)
+    else if (s1 == 0b0) & (s2 == 0b1)
+    then false
+    else if (s1 == 0b1) & (s2 == 0b0)
+    then true
     else
-        if (e1 == e2) then
-          unsigned (m1) > unsigned (m2)
-        else
-          unsigned (e1) > unsigned (e2);
+        if   (e1 == e2)
+        then unsigned (m1) > unsigned (m2)
+        else unsigned (e1) > unsigned (e2);
 
   let fflags = if is_quiet then
-                 if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then
-                   nvFlag()
-                 else
-                   zeros()
+                 if   (f_is_SNaN_S(v1) | f_is_SNaN_S(v2))
+                 then nvFlag()
+                 else zeros()
                else
-                 if (v1IsNaN | v2IsNaN) then
-                   nvFlag()
-                 else
-                   zeros();
+                 if   (v1IsNaN | v2IsNaN)
+                 then nvFlag()
+                 else zeros();
 
   (result, fflags)
 }
@@ -223,30 +218,26 @@ function fle_S   (v1,       v2,        is_quiet) = {
 
   let result : bool =
     if (s1 == 0b0) & (s2 == 0b0) then
-      if (e1 == e2) then
-        unsigned (m1) <=  unsigned (m2)
-      else
-        unsigned (e1)  <  unsigned (e2)
-    else if (s1 == 0b0) & (s2 == 0b1) then
-      (v1Is0 & v2Is0)                         /* Equal in this case (+0=-0) */
-    else if (s1 == 0b1) & (s2 == 0b0) then
-      true
+      if   (e1 == e2)
+      then unsigned (m1) <=  unsigned (m2)
+      else unsigned (e1)  <  unsigned (e2)
+    else if (s1 == 0b0) & (s2 == 0b1)
+    then (v1Is0 & v2Is0)                         /* Equal in this case (+0=-0) */
+    else if (s1 == 0b1) & (s2 == 0b0)
+    then true
     else
-      if (e1 == e2) then
-        unsigned (m1) >=  unsigned (m2)
-      else
-        unsigned (e1)  >  unsigned (e2);
+      if   (e1 == e2)
+      then unsigned (m1) >=  unsigned (m2)
+      else unsigned (e1)  >  unsigned (e2);
 
   let fflags = if is_quiet then
-                 if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then
-                   nvFlag()
-                 else
-                   zeros()
+                 if   (f_is_SNaN_S(v1) | f_is_SNaN_S(v2))
+                 then nvFlag()
+                 else zeros()
                else
-                 if (v1IsNaN | v2IsNaN) then
-                   nvFlag()
-                 else
-                   zeros();
+                 if   (v1IsNaN | v2IsNaN)
+                 then nvFlag()
+                 else zeros();
 
   (result, fflags)
 }
@@ -828,8 +819,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = {
   let (s1, e1, m1) = fsplit_S (rs1_val_S);
   let (s2, e2, m2) = fsplit_S (rs2_val_S);
   let rd_val_S     = fmake_S (s2, e1, m1);
-  let fflags       = 0b_00000;
-  write_fflags(fflags);
+
   F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
@@ -840,8 +830,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = {
   let (s1, e1, m1) = fsplit_S (rs1_val_S);
   let (s2, e2, m2) = fsplit_S (rs2_val_S);
   let rd_val_S     = fmake_S (0b1 ^ s2, e1, m1);
-  let fflags       = 0b_00000;
-  write_fflags(fflags);
+
   F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
@@ -852,8 +841,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = {
   let (s1, e1, m1) = fsplit_S (rs1_val_S);
   let (s2, e2, m2) = fsplit_S (rs2_val_S);
   let rd_val_S     = fmake_S (s1 ^ s2, e1, m1);
-  let fflags       = 0b_00000;
-  write_fflags(fflags);
+
   F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
@@ -876,7 +864,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = {
                   else if rs1_lt_rs2                                                then rs1_val_S
                   else /* (not rs1_lt_rs2) */                                            rs2_val_S;
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
@@ -899,7 +887,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
                   else if rs2_lt_rs1                                                then rs1_val_S
                   else /* (not rs2_lt_rs1) */                                            rs2_val_S;
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
@@ -916,7 +904,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
       else if rs1_eq_rs2                                        then EXTZ(0b1)
       else                                                           zeros();
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
@@ -934,7 +922,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
       else if rs1_lt_rs2                                        then EXTZ(0b1)
       else                                                           zeros();
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
@@ -952,7 +940,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
       else if rs1_le_rs2                                        then EXTZ(0b1)
       else                                                           zeros();
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }