Add support for Zfh extension #129

bilalsakhawat · 2021-11-19T13:46:17Z

“Zfh” Standard Extensions for Half-Precision Floating-Point, Version 0.1

Chapter 15 in the draft spec.

FCVT.Q.H and FCVT.H.Q are not implemented. (Quad-Precision is not supported by sail yet)

martinberger

Why do you commit prover snapshots? They are auto-generated.

PeterSewell · 2021-11-20T16:56:45Z

it's often handy, e.g. so people can see the prover definitions directly

…

On Sat, 20 Nov 2021 at 16:52, Martin Berger ***@***.***> wrote: ***@***.**** commented on this pull request. Why do you commit prover snapshots? They are auto-generated. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#129 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZSBL7SRVKCCJZAT2WDUM7GVPANCNFSM5IMF2XVQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

scottj97 · 2021-11-20T16:56:56Z

Why do you commit prover snapshots? They are auto-generated.

They already existed in the repo, so he's just keeping them up to date, which is better than letting them fall behind.

Are you recommending these be deleted from the repo?

martinberger · 2021-11-20T17:42:30Z

it's often handy, e.g. so people can see the prover definitions directly

@PeterSewell Yes, but then we need to make sure the generated prover definitions stay up-to-date with the sail model. For example generating prover snapshots in not in the GH Actions CI. So I'm wondering if they are even up-to-date.

@scottj97 If they get auto-generated by the CI, we can delete them.

martinberger · 2021-11-25T12:33:11Z

@PeterSewell How much work do you think it would be to script the building of all the prover snapshot with GitHub Actions, so we can remove the word "not" from https://github.com/riscv/sail-riscv/blob/master/prover_snapshots/README.md ? I imagine there was a reason why the current build process does not automate this.

jrtc27

Unfortunately with the recent landing of Zfinx you picked a bad time to submit this pull request, and will need to rebase on top of that and apply the same changes to the new Zfh code. I think it should be relatively straightforward, if tedious. The only thing noteworthy that comes to mind is nan_(un)box should probably be made overloaded calling _S and _H versions (with the _S version being what is currently there) rather than having nan_(un)box and nan_(un)box_H as is done here.

Glancing at the implementation I'm reminded of how non-conforming the F/D code is (blame Bluespec's internal code style for that, which I suspect is derived from treating everything like it's Haskell), but I agree with your choice here to copy the F/D code style (I assume you just copied F and swept through converting all the F-specificity to Zfh-specificity) rather than reformat it for Zfh and increase the divergence between them.

jrtc27 · 2021-11-27T17:09:47Z

model/riscv_softfloat_interface.sail

@@ -112,6 +113,35 @@ function update_softfloat_fflags(flags) = {
 /* **************************************************************** */
 /* ADD/SUB/MUL/DIV                                                  */

+


Stray extra line

jrtc27 · 2021-11-27T17:11:02Z

model/riscv_insts_fext.sail

@@ -389,6 +418,13 @@ function process_fload32(rd, addr, value) =
    MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
  }

+val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16)))


Really the functions should be the other way round, but that's not your problem, so this is the right thing to do in the situation

jrtc27 · 2021-11-27T17:13:37Z

model/riscv_insts_zfh.sail

@@ -0,0 +1,916 @@
+


Should probably have the copyright header from fext given this is heavily derived from it, as well as an equivalent to:

/* **************************************************************** */ /* This file specifies the instructions in the F extension */ /* (single precision floating point). */ /* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */ /* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ /* **************************************************************** */ /* IMPORTANT! */ /* The files 'riscv_insts_fext.sail' and 'riscv_insts_dext.sail' */ /* define the F and D extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ /* **************************************************************** */

That should probably also be updated across all three to reference Zfh

(Normally wouldn't mandate that block of documentation but F and D, and now Zfh, are a bit special in how they're implemented and we want to ensure they stay as similar as possible)

bilalsakhawat · 2021-12-04T14:13:28Z

@jrtc27 I refactor the code for Zfh Extension. I think, modifications from Zfh to ZFinx_Zfh should be in a separate Pull Request. If you agree, I just need to add copyright header in the model/riscv_insts_zfh.sail and this PR is good to go.

jrtc27 · 2021-12-05T05:21:04Z

Deferring Zhinx seems ok to me, it's true that requesting it is moving the goalposts for this PR. Had you been slightly later and copied the F or D file with Z[fd]inx support then you would've been 95% of the way there already for free, but alas that's not what happened and so instead it's a bunch of work to repeat all the changes to the Zfh code.

I quickly skimmed the PR and noticed that the stray line comment from 8 days ago also still applies. I also found the "RV64 only" comment for the L[U] conversions mentions F not Zfh.

I'll try and take a more thorough look tomorrow.

martinberger · 2022-01-18T11:14:16Z

I'll try and take a more thorough look tomorrow.

@jrtc27 Did you manage to take a look?

jrtc27 · 2022-01-18T19:02:25Z

model/riscv_insts_fext.sail

+                      -> Retired effect {escape, rreg, wreg}
+function process_fload16(rd, addr, value) =
+  match value {
+    MemValue(result) => { F(rd) = nan_box_H(result); RETIRE_SUCCESS },


This can just be nan_box, same as process_fload32

jrtc27 · 2022-01-18T19:03:46Z

model/riscv_insts_zfh.sail

+        FDIV_H  => riscv_f16Div (rm_3b, rs1_val_16b, rs2_val_16b)
+      };
+      write_fflags(fflags);
+      F(rd) = nan_box_H (rd_val_16b);


These can all be nan_box, for consistency with F (that or those should be changed to nan_box_S, but I don't see the benefit from that, might as well make use of the language's overloading to make the code a bit cleaner to read), though given they'll all need changing in future to F_or_X_H(rd) = ... with the NaN boxing implicit I guess this is fine, unlike the one for FP_LOAD which will stay and thus should be fixed (though arguably pushing that into a new F_H/S/D might make things slightly cleaner and more consistent, as a future minor refactor).

jrtc27 · 2022-01-18T19:07:14Z

model/riscv_insts_zfh.sail

+/* Execution semantics ================================ */
+
+function clause execute (F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)) = {
+  let rs1_val_16b = nan_unbox_H (F(rs1));


These will all need to use (a new) F_or_X_H but I guess it's fine to express it this way for now

jrtc27 · 2022-01-18T19:10:53Z

I'll try and take a more thorough look tomorrow.

@jrtc27 Did you manage to take a look?

I did not but have now. One minor comment, the rest observations. The commits should also be squashed down into a single commit rather than the 3 there are now (or 4 that it may become).

bilalsakhawat · 2022-01-19T07:14:41Z

@jrtc27 I have incorporated the changes suggested by you.

jrtc27

I think this is now ready

martinberger

Looks fine to me.

martinberger · 2022-01-19T19:21:57Z

Merged.

Thanks @bilalsakhawat-10xe @jrtc27

martinberger reviewed Nov 20, 2021

View reviewed changes

jrtc27 reviewed Nov 27, 2021

View reviewed changes

bilalsakhawat force-pushed the zfh_dev branch from cf8049b to 19153a0 Compare December 3, 2021 09:25

bilalsakhawat force-pushed the zfh_dev branch from 19153a0 to 9517c69 Compare December 8, 2021 12:36

jrtc27 reviewed Jan 18, 2022

View reviewed changes

Add support for Zfh extension

217a46a

bilalsakhawat force-pushed the zfh_dev branch from 9517c69 to 217a46a Compare January 19, 2022 07:11

bilalsakhawat requested review from jrtc27 and martinberger January 19, 2022 07:15

jrtc27 approved these changes Jan 19, 2022

View reviewed changes

martinberger approved these changes Jan 19, 2022

View reviewed changes

martinberger merged commit 612958b into riscv:master Jan 19, 2022

bilalsakhawat added a commit to bilalsakhawat/sail-riscv that referenced this pull request Jan 20, 2022

Add support for Zfh extension (riscv#129)

5671634

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for Zfh extension #129

Add support for Zfh extension #129

bilalsakhawat commented Nov 19, 2021

martinberger left a comment

PeterSewell commented Nov 20, 2021 via email

scottj97 commented Nov 20, 2021

martinberger commented Nov 20, 2021 •

edited

Loading

martinberger commented Nov 25, 2021

jrtc27 left a comment •

edited

Loading

jrtc27 Nov 27, 2021

jrtc27 Nov 27, 2021

jrtc27 Nov 27, 2021

jrtc27 Nov 27, 2021

bilalsakhawat commented Dec 4, 2021

jrtc27 commented Dec 5, 2021

martinberger commented Jan 18, 2022

jrtc27 Jan 18, 2022

jrtc27 Jan 18, 2022

jrtc27 Jan 18, 2022

jrtc27 commented Jan 18, 2022

bilalsakhawat commented Jan 19, 2022 •

edited

Loading

jrtc27 left a comment

martinberger left a comment

martinberger commented Jan 19, 2022

		@@ -112,6 +113,35 @@ function update_softfloat_fflags(flags) = {
		/* **************************************************************** */
		/* ADD/SUB/MUL/DIV */

Add support for Zfh extension #129

Add support for Zfh extension #129

Conversation

bilalsakhawat commented Nov 19, 2021

martinberger left a comment

Choose a reason for hiding this comment

PeterSewell commented Nov 20, 2021 via email

scottj97 commented Nov 20, 2021

martinberger commented Nov 20, 2021 • edited Loading

martinberger commented Nov 25, 2021

jrtc27 left a comment • edited Loading

Choose a reason for hiding this comment

jrtc27 Nov 27, 2021

Choose a reason for hiding this comment

jrtc27 Nov 27, 2021

Choose a reason for hiding this comment

jrtc27 Nov 27, 2021

Choose a reason for hiding this comment

jrtc27 Nov 27, 2021

Choose a reason for hiding this comment

bilalsakhawat commented Dec 4, 2021

jrtc27 commented Dec 5, 2021

martinberger commented Jan 18, 2022

jrtc27 Jan 18, 2022

Choose a reason for hiding this comment

jrtc27 Jan 18, 2022

Choose a reason for hiding this comment

jrtc27 Jan 18, 2022

Choose a reason for hiding this comment

jrtc27 commented Jan 18, 2022

bilalsakhawat commented Jan 19, 2022 • edited Loading

jrtc27 left a comment

Choose a reason for hiding this comment

martinberger left a comment

Choose a reason for hiding this comment

martinberger commented Jan 19, 2022

martinberger commented Nov 20, 2021 •

edited

Loading

jrtc27 left a comment •

edited

Loading

bilalsakhawat commented Jan 19, 2022 •

edited

Loading