Simplify softfloat interface by removing write_fflags

[Timmmm]

Instead of keeping a mirror register in sync with fflags, just return the new flags. This removes the need for write_fflags() and update_softfloat_fflags().

[github-actions]

Unit Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit a39b32f. ± Comparison against base commit c90cf2e.

♻️ This comment has been updated with latest results.

[Timmmm]

@jrtc27 please could I have a review of this at some point? It's a subset of #289 that you asked me to break up into smaller commits. Thanks!

[Timmmm]

@billmcspadden-riscv could we get this reviewed somehow? We've spoken about it a couple of times, it doesn't change any behaviour, and I'd like to avoid resolving rebase conflicts for a third time! It's also holding up further improvements.

[jrtc27]

I don't feel qualified to review this kind of floating-point code other than to say that simplifying code is a good thing if it's equivalent. Perhaps someone like @ptomsich might be interested in reviewing?

[Timmmm]

Here's a more detailed description of the change since it's a bit hard to follow.

Consider executing an instruction that uses the softfloat library (some are implemented directly in Sail), e.g. feq.d. The current flow is:

1. Decode the instruction to ast:

mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)                 if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveDoubleFPU() & validDoubleRegs([rs2, rs1])

2. Execute it:

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
  let rs1_val_D = F_or_X_D(rs1);
  let rs2_val_D = F_or_X_D(rs2);

  let (fflags, rd_val) : (bits_fflags, bool) =
      riscv_f64Eq (rs1_val_D, rs2_val_D);            // A

  write_fflags(fflags);                                      // B
  X(rd) = zero_extend(bool_to_bits(rd_val));
  RETIRE_SUCCESS
}

3. At // A, we call through to the softfloat C library:

/* ***************************************************************** */
/* Internal registers to pass results across the softfloat interface
 * to avoid return types involving structures.
 */
register float_result : bits(64)
register float_fflags : bits(64)

/* updater to keep the flags in sync with fcsr.fflags */
val update_softfloat_fflags : bits(5) -> unit
function update_softfloat_fflags(flags) = {
  float_fflags = sail_zero_extend(flags, 64);
}

...

val     extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit
val      riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool)
function riscv_f64Eq (v1, v2) = {
  extern_f64Eq(v1, v2);         // C
  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

4. At // C, this is where it actually calls the C code. Now in C, with macros expanded:

unit softfloat_f64eq(mach_bits v1, mach_bits v2)
{
  // SOFTFLOAT_PRELUDE(0);   // expands to {
  softfloat_exceptionFlags = 0;
  softfloat_roundingMode = (uint_fast8_t)0;
  // }

  float64_t a, b, res;
  a.v = v1;
  b.v = v2;
  res.v = f64_eq(a, b);

  // SOFTFLOAT_POSTLUDE(res); // expands to {
  zfloat_result = res.v;
  zfloat_fflags |= (mach_bits)softfloat_exceptionFlags;
  // }

  return UNIT;
}

4. Back in Sail, at write_fflags():

/* called for softfloat paths (softfloat flags are consistent) */
val write_fflags : (bits(5)) -> unit
function write_fflags(fflags) = {
  if   fcsr.FFLAGS() != fflags
  then dirty_fd_context_if_present();
  fcsr->FFLAGS() = fflags;
}

So what is happening is that the float_fflags register is a copy of the fcsr.FFLAGS field. It is updated in two ways:

1. When a softfloat operation happens the new flags (softfloat_exceptionFlags) are directly ORed into it in C (zfloat_fflats |= (mach_bits)softfloat_exceptionFlags;) and then float_fflags is returned from the operation ((float_fflags[4 .. 0], ...), and used to update fcsr.FFLAGS in write_fflags(). This updates fcsr.FFLAGS when float_fflags changes.
2. When fflags are written in Sail, e.g. by directly writing the CSRs (ext_write_fcsr()), then it calls a function update_softfloat_fflags(). This updates float_fflags when fcsr.FFLAGS changes.

It's all very convoluted. In essence this PR changes the flow from:

1. float_fflags = csr.FFLAGS; (in Sail)
2. Perform floating point operation. (in C)
3. zfloat_fflags |= new_flags; (in C)
4. fcsr.FFLAGS = float_fflags; (in Sail)

to:

1. Perform floating point operation. (in C)
2. zfloat_fflags = new_flags; (in C)
3. fcsr.FFLAGS |= float_fflags; (in Sail)

So it changes float_fflags from being a mirror of fcsr.FFLAGS, to just being a temporary register used to return the new flags from C to Sail. Then the ORing is done in Sail.

Since there's no mirror register anymore, update_softfloat_flags() is no longer needed, and there's also no need to distinguish between write_fflags(flags) (i.e. fcsr.FFLAGS = flags) and accrue_fflags(new_flags) (i.e. fcsr.FFLAGS |= flags;) because both the softfloat and Sail float instructions work the same way.

[billmcspadden-riscv]

This looks fine to me.

Please make sure that the fp tests pass before merging to master.

[Timmmm]

FP test results (all pass):

❯ test/run_fp_tests.sh 
...
Building 64-bit RISCV C emulator: ok
C-64 rv64uf-p-fadd.elf: ok
C-64 rv64uf-p-fclass.elf: ok
C-64 rv64uf-p-fcmp.elf: ok
C-64 rv64uf-p-fcvt.elf: ok
C-64 rv64uf-p-fcvt_w.elf: ok
C-64 rv64uf-p-fdiv.elf: ok
C-64 rv64uf-p-fmadd.elf: ok
C-64 rv64uf-p-fmin.elf: ok
C-64 rv64uf-p-ldst.elf: ok
C-64 rv64uf-p-move.elf: ok
C-64 rv64uf-p-recoding.elf: ok
C-64 rv64uf-v-fadd.elf: ok
C-64 rv64uf-v-fclass.elf: ok
C-64 rv64uf-v-fcmp.elf: ok
C-64 rv64uf-v-fcvt.elf: ok
C-64 rv64uf-v-fcvt_w.elf: ok
C-64 rv64uf-v-fdiv.elf: ok
C-64 rv64uf-v-fmadd.elf: ok
C-64 rv64uf-v-fmin.elf: ok
C-64 rv64uf-v-ldst.elf: ok
C-64 rv64uf-v-move.elf: ok
C-64 rv64uf-v-recoding.elf: ok
C-64 rv64ud-p-fadd.elf: ok
C-64 rv64ud-p-fclass.elf: ok
C-64 rv64ud-p-fcmp.elf: ok
C-64 rv64ud-p-fcvt.elf: ok
C-64 rv64ud-p-fcvt_w.elf: ok
C-64 rv64ud-p-fdiv.elf: ok
C-64 rv64ud-p-fmadd.elf: ok
C-64 rv64ud-p-fmin.elf: ok
C-64 rv64ud-p-ldst.elf: ok
C-64 rv64ud-p-move.elf: ok
C-64 rv64ud-p-recoding.elf: ok
C-64 rv64ud-p-structural.elf: ok
C-64 rv64ud-v-fadd.elf: ok
C-64 rv64ud-v-fclass.elf: ok
C-64 rv64ud-v-fcmp.elf: ok
C-64 rv64ud-v-fcvt.elf: ok
C-64 rv64ud-v-fcvt_w.elf: ok
C-64 rv64ud-v-fdiv.elf: ok
C-64 rv64ud-v-fmadd.elf: ok
C-64 rv64ud-v-fmin.elf: ok
C-64 rv64ud-v-ldst.elf: ok
C-64 rv64ud-v-move.elf: ok
C-64 rv64ud-v-recoding.elf: ok
C-64 rv64ud-v-structural.elf: ok
C-64 rv64mi-p-csr.elf: ok
64-bit RISCV C tests: Passed 48 out of 48
...
Building 32-bit RISCV C emulator: ok
C-32 rv32uf-p-fadd.elf: ok
C-32 rv32uf-p-fclass.elf: ok
C-32 rv32uf-p-fcmp.elf: ok
C-32 rv32uf-p-fcvt.elf: ok
C-32 rv32uf-p-fcvt_w.elf: ok
C-32 rv32uf-p-fdiv.elf: ok
C-32 rv32uf-p-fmadd.elf: ok
C-32 rv32uf-p-fmin.elf: ok
C-32 rv32uf-v-fadd.elf: ok
C-32 rv32uf-v-fclass.elf: ok
C-32 rv32uf-v-fcmp.elf: ok
C-32 rv32uf-v-fcvt.elf: ok
C-32 rv32uf-v-fcvt_w.elf: ok
C-32 rv32uf-v-fdiv.elf: ok
C-32 rv32uf-v-fmadd.elf: ok
C-32 rv32uf-v-fmin.elf: ok
C-32 rv32ud-p-fadd.elf: ok
C-32 rv32ud-p-fclass.elf: ok
C-32 rv32ud-p-fcmp.elf: ok
C-32 rv32ud-p-fcvt.elf: ok
C-32 rv32ud-p-fcvt_w.elf: ok
C-32 rv32ud-p-fdiv.elf: ok
C-32 rv32ud-p-fmadd.elf: ok
C-32 rv32ud-p-fmin.elf: ok
C-32 rv32ud-v-fadd.elf: ok
C-32 rv32ud-v-fclass.elf: ok
C-32 rv32ud-v-fcmp.elf: ok
C-32 rv32ud-v-fcvt.elf: ok
C-32 rv32ud-v-fcvt_w.elf: ok
C-32 rv32ud-v-fdiv.elf: ok
C-32 rv32ud-v-fmadd.elf: ok
C-32 rv32ud-v-fmin.elf: ok
C-32 rv32mi-p-csr.elf: ok
32-bit RISCV C tests: Passed 34 out of 34

Passed 82 out of 82

[Timmmm]

(I don't have permission to merge it btw, just in case you were expecting me to do it!)

[billmcspadden-riscv]

Yes, Tim's explanation was clear and quite helpful. I walked through the code and matched his explanation with the actual code. Also, he ran the existing FP tests. I'm going to go ahead and merge this. Bill Mc.

…

On Wed, Oct 25, 2023 at 8:53 AM Tim Hutt ***@***.***> wrote: (I don't have permission to merge it btw, just in case you were expecting me to do it!) — Reply to this email directly, view it on GitHub <#290 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOG4M6MTS4TCYKUOS63YBEKTZAVCNFSM6AAAAAA3FF4BDGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONZZGMZDOMJRG4> . You are receiving this because you were assigned.Message ID: ***@***.***>

-- Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309

[Timmmm]

Thanks!