Float: Add floating-point equals API in sail model #403

Incarnation-p-lee · 2024-02-07T06:08:42Z

This patch would like to introduce the floating-point equals API into the sail model. Then floating-point equals will be invoked in sail instead of the c_emulator.

Add enum-like immutable exception flags and types to commons.
Add float equals API for half, single and double floating-point.
Replace the extern call of softfloat interface by the sail model.
Adjust the build system for new files.
Passed 712 out of 712 from ./test/run_tests.sh.

arichardson

Is there any way to avoid the global variables for the new functions and just return the result directly (might need something like #340 to be merged first)?

Incarnation-p-lee · 2024-02-07T07:19:08Z

Is there any way to avoid the global variables for the new functions and just return the result directly (might need something like #340 to be merged first)?

Thanks for the comments.

I think at least we can return the float result directly in riscv_softfloat_eq. But for migration from emulator to sail, I may prefer to do it in another PR as I am green hand for sail and I would like to limit the risk here. How do you think of it?

For #340 , I am afraid we may not need this anymore if the softfloat migrates to sail. The sofefloat in c_emulator will be depreciated soon as I understand. Feel free to correct me if any misleading.

This patch would like to introduce the soft floating-point equals API into the sail model. Then the softfloat_interface is able to leverage the new softfloat in sail, instead of the c_emulator. * Add softfloat common for softfloat enter and leave. * Add enum like immutable exception flags. * Add softfloat equals API for half, single and double floating-point. * Replace the extern call of softfloat interface to sail model. * Add helper functions to utils. * Adjust build system for new files. Signed-off-by: Pan Li <pan2.li@intel.com>

model/riscv_insts_vext_utils.sail

Timmmm · 2024-02-07T11:18:25Z

For #340 , I am afraid we may not need this anymore if the softfloat migrates to sail. The sofefloat in c_emulator will be depreciated soon as I understand.

I think that was an aspirational hope rather than someone actually saying "I will do this". It would be great though!

I need to take another look at #340. IIRC it failed because of the OCaml emulator (which we don't use) and I don't know OCaml...

Probably shouldn't block this anyway.

Makefile

model/softfloat/riscv_softfloat_common.sail

model/softfloat/riscv_softfloat_eq.sail

Incarnation-p-lee · 2024-02-07T11:58:00Z

For #340 , I am afraid we may not need this anymore if the softfloat migrates to sail. The sofefloat in c_emulator will be depreciated soon as I understand.

I think that was an aspirational hope rather than someone actually saying "I will do this". It would be great though!

I need to take another look at #340. IIRC it failed because of the OCaml emulator (which we don't use) and I don't know OCaml...

Probably shouldn't block this anyway.

Thanks for the comments. Lots of useful items, especially for the green hands to sail like me. I will address it soon.

Signed-off-by: Pan Li <pan2.li@intel.com>

jrtc27 · 2024-02-07T15:21:08Z

Please avoid creating 16/32/64 copies of every function. You should in general be able to write one polymorphic function that handles all sizes.

Signed-off-by: Pan Li <pan2.li@intel.com>

Incarnation-p-lee · 2024-02-08T02:13:18Z

Thanks all, addressed comments with all fp tests passed.

Timmmm · 2024-02-12T10:18:32Z

This is much better, though I think you could go even further. There's not really much point to the riscv_f16Eq() etc functions now that they aren't using FFI.

You could just delete them, and then change the code that uses them to call your new functions instead.

Note that there's already this function in the vector extension:

val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function fp_eq(op1, op2) = {
  let (fflags, result_val) : (bits_fflags, bool) = match 'm {
    16  => riscv_f16Eq(op1, op2),
    32  => riscv_f32Eq(op1, op2),
    64  => riscv_f64Eq(op1, op2)
  };
  accrue_fflags(fflags);
  result_val
}

I would:

Delete fp_eq from the vector extension.
Delete riscv_f16Eq, riscv_f32Eq and riscv_f64Eq.
Move everything from riscv_float_common.sail back to where it started.
Change your code to be like this (not tested!):

val float_equal : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool)
function float_equal(op1, op2) = {
  let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2);
  let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2);

  let fflags = if is_nan & is_snan then float_flag_invalid else zeros();

  let is_equal : bool = if not(is_nan)
                        then op1 == op2 | ((op1 | op2) << 1) == zeros()
                        else false;

  (fflags, is_equal)
}

val float_equal_raise_flags : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function float_equal_raise_flags(op1, op2) = {
  let (is_equal, fflags) = float_equal(op1, op2);
  accrue_fflags(fflags);
  is_equal
}

And then change all the code that used fp_eq to call float_equal_raise_flags, and all the code that called riscv_f16Eq etc. to call float_equal.

Hope that makes sense! Thanks for the contribution btw!

Incarnation-p-lee · 2024-02-12T11:32:40Z

This is much better, though I think you could go even further. There's not really much point to the riscv_f16Eq() etc functions now that they aren't using FFI.

You could just delete them, and then change the code that uses them to call your new functions instead.

Note that there's already this function in the vector extension:
val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function fp_eq(op1, op2) = {
  let (fflags, result_val) : (bits_fflags, bool) = match 'm {
    16  => riscv_f16Eq(op1, op2),
    32  => riscv_f32Eq(op1, op2),
    64  => riscv_f64Eq(op1, op2)
  };
  accrue_fflags(fflags);
  result_val
}
I would:

Delete fp_eq from the vector extension.

Delete riscv_f16Eq, riscv_f32Eq and riscv_f64Eq.

Move everything from riscv_float_common.sail back to where it started.

Change your code to be like this (not tested!):
val float_equal : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool)
function float_equal(op1, op2) = {
  let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2);
  let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2);

  let fflags = if is_nan & is_snan then float_flag_invalid else zeros();

  let is_equal : bool = if not(is_nan)
                        then op1 == op2 | ((op1 | op2) << 1) == zeros()
                        else false;

  (fflags, is_equal)
}

val float_equal_raise_flags : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function float_equal_raise_flags(op1, op2) = {
  let (is_equal, fflags) = float_equal(op1, op2);
  accrue_fflags(fflags);
  is_equal
}
And then change all the code that used fp_eq to call float_equal_raise_flags, and all the code that called riscv_f16Eq etc. to call float_equal.

Hope that makes sense! Thanks for the contribution btw!

Thanks for comments. I see, looks you would like to suggest get rid of softfloat_interface.sail up to a point. I plan to do that later and make this change simple enough for review. But as you mentioned already, I will add that part to this PR.

Signed-off-by: Pan Li <pan2.li@intel.com>

Incarnation-p-lee · 2024-02-12T12:12:59Z

Updated with run_fp_tests.sh passed. By the way, keep float_common files for some type(s) and/or const- variables. As we will remove the file softfloat_interface, I may prefer to let the softfloat_interface depends on the float_common instead of the float_common depends on the softfloat_interface.

Signed-off-by: Pan Li <pan2.li@intel.com>

Timmmm

LGTM just some minor nits left

model/float/riscv_float_eq.sail

model/riscv_insts_dext.sail

model/riscv_insts_fext.sail

model/float/riscv_float_common.sail

model/riscv_softfloat_interface.sail

Signed-off-by: Pan Li <pan2.li@intel.com>

Incarnation-p-lee · 2024-02-13T02:10:33Z

LGTM just some minor nits left

Thanks a lot for comments. Addressed all except the is_equal type annotation. Passed the run_fp_tests.sh.

Timmmm · 2024-02-13T10:32:28Z

Addressed all except the is_equal type annotation

Ah yeah sometimes the type inference doesn't work entirely intuitively...

All LGTM anyway!

Incarnation-p-lee · 2024-02-13T11:11:18Z

Addressed all except the is_equal type annotation

Ah yeah sometimes the type inference doesn't work entirely intuitively...

All LGTM anyway!

Thanks. Looks like I have no authority to merge, will continue the rest part of softfloat following the pattern of this PR.

Timmmm · 2024-02-13T12:04:42Z

Yeah currently @billmcspadden-riscv is chief merger, but he is ill at the moment.

Also I finally figured out why I can't resolve my conversations:

You can resolve a conversation in a pull request if you opened the pull request or if you have write access to the repository where the pull request was opened.

That seems bonkers - surely the person who started a conversation should be able to resolve it? I guess it explains it at least! Anyway since you opened the PR you should be able to resolve all my conversations.

billmcspadden-riscv · 2024-02-13T12:11:57Z

Yes, I’m in hospital right now and have limited ability to do much work. Martin Burger can also do a merge as well. The question for the team is: do we want to do small, incremental merges for this project, or do we want to put this on a feature branch (with a full merge once all the work is done) like what we did for Vector last year? I think we should just go ahead and do the small incremental merges on main. Thots? Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309

…

On Tue, Feb 13, 2024 at 6:04 AM Tim Hutt ***@***.***> wrote: Yeah currently @billmcspadden-riscv <https://github.com/billmcspadden-riscv> is chief merger, but he is ill at the moment. Also I finally figured out why I can't resolve my conversations: You can resolve a conversation in a pull request if you opened the pull request or if you have write access to the repository where the pull request was opened. That seems bonkers - surely the person who started a conversation should be able to resolve it? I guess it explains it at least! Anyway since you opened the PR you should be able to resolve all my conversations. — Reply to this email directly, view it on GitHub <#403 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOCJPW74P7MSTYEVNCTYTNJGPAVCNFSM6AAAAABC5HFXZCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNBRGM3DQMBQG4> . You are receiving this because you were mentioned.Message ID: ***@***.***>

Incarnation-p-lee · 2024-02-13T12:24:57Z

@Timmmm
Resolved all conversations as LGTM, thanks again for the review and help.

@billmcspadden-riscv
Take care. I may prefer small incremental merges.

Timmmm · 2024-02-13T15:30:53Z

Yeah I agree - this is a change that can easily be done piecemeal so we should do so. @Incarnation-p-lee probably a good idea to squash your commits.

Incarnation-p-lee · 2024-02-14T00:43:26Z

piecemeal

Cannot agree anymore, take squash merger here and we will see only one commit from the main branch. That would be much clear.

jrtc27 · 2024-02-14T00:46:50Z

model/riscv_softfloat_interface.sail

+/* Internal registers to pass results across the softfloat interface */
+/* to avoid return types involving structures. */
+/* */
+/* Todo: Return the float_result directly in Sail. */
+/* ***************************************************************** */


I don't think you should be touching this? Your new code doesn't have this issue.

Just hint here to remind that, the float in saill will return directly, as well as the softfloat_interface will be retired soon.

I can revert this change if you have any concern here.

Reverted this change.

jrtc27 · 2024-02-14T00:47:22Z

model/riscv_softfloat_interface.sail

@@ -26,7 +26,6 @@
 /* All arguments and results have one of these types */

 type bits_rm = bits(3) /* Rounding mode */
-type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */


I can't see how this builds if you delete the type used by the unconverted functions...

Oh, I see, you moved that but nothing else to a new file. That seems like a strange design choice; I would expect fflags and frm to be defined next to each other given they both constitute fcsr.

This type moved to the riscv_float_common.sail, which will be leveraged by the floating-point implementation (like float_eq) in sail.

Given the softfloat_interface will be retired soon, it is better to let the softfloat_interface
depends on riscv_float_common.sail. Of course, you are right, the related types like frm/fflags will be removed to the riscv_float_common.sail soon. I didn't perform this change because they are not referenced by the float_eq.

Updated, please help to review when you free.

jrtc27 · 2024-02-16T04:36:25Z

Also: projects like GCC are very different to something like sail-riscv. Many of the people reviewing patches on the GCC mailing list are full-time employees paid by their organisation to do that, or at least a large part of their job. That is not the case here; it is nobody's full-time job, for many it's just a small part of their job, and many are also volunteers. So please consider that before having high expectations of how quickly people will reply to you. And of course the more time spent discussing things like this, the less time spent doing actually useful work...

Incarnation-p-lee · 2024-02-16T04:42:05Z

Well my comments remain unresolved, and your responses haven't changed my opinion... seems slightly untoward for you to be saying this when there are outstanding comments you've just shrugged off.

Well well, wait for a moment. You say there are OUTSTANDING comments, are you indicating @Timmmm approve this PR without notice these OUTSTANDING comments? I think this is not a good way to communicate, especially in the PR review.
Indeed, you leave comments, I reply comments and there is no further response from your side. So I suppose there is no action required and ping if we can move on.
After that I would like to fast the process if there is no more comments to address, (I said IF in case someone else would like to review soon). And then you emphasize the comments are outstanding, and I just shrugged off? I don't think it is the right way to do the communication. I said in comments I am totally OK to make the change as you suggestion but I cannot guess your option until you reply the comments.
Guess how I did GCC PATCH review for a similar case:

You left the comments first.

Then I reply why I need to do this.

After some time, there is no respone, I will ping if it is OK for trunk.

Then you insist your option and reply the comments.

I got your point and made the changes as you suggested.

Then PR was accepted and merged into the trunk.

I think the above should be a better way to communicate in the PR review. Please feel free to correct me if any misleading.

Can you please tone it down several levels?

Take it easy, I think our goal is the same for the the best reasonable outcome.

And if you really care about the details, Tim approved it before my review. But people are entirely free to give their own independent reviews; just because one person's happy doesn't mean you can ignore someone who would like to see changes.

I agree with you on this point as I said in comments, I am totally Ok for making changes.

Also, we're talking under 48 hours here. It's not reasonable to expect everyone to always be able to reply within that time period, and pinging a patch that frequently is a bit too much IMO (a week is a more standard time period, at least in the communities I generally contribute to). And when you do so, the more constructive thing to do is ask whether your comments address the concerns or not, not to assume that you've changed someone's mind just because they have yet to say anything and push for merging.

I guess the underlying point is that code review isn't a fight to be won, it's a conversation that's aiming to achieve the best reasonable outcome.

I think the point is not about the 48 hours or not. I think it is important to make things clear and an efficient way to communicate. You can just reply first comment similar to "Yes, please revert this change", and the second one similar to "Yes, please move all related types to the new file.", instead of saying outstanding, and shrugged off.

I think that should be more clear here. Agree there is no place to get someone to win, just to make it clear to both of us.

Incarnation-p-lee · 2024-02-16T04:45:45Z

Also: projects like GCC are very different to something like sail-riscv. Many of the people reviewing patches on the GCC mailing list are full-time employees paid by their organisation to do that, or at least a large part of their job. That is not the case here; it is nobody's full-time job, for many it's just a small part of their job, and many are also volunteers. So please consider that before having high expectations of how quickly people will reply to you. And of course the more time spent discussing things like this, the less time spent doing actually useful work...

Understood the timing you mentioned, sorry I didn't get any information from this repo about it. I think we are on the same page now. I will make the changes as your comments soon.

Signed-off-by: Pan Li <pan2.li@intel.com>

Timmmm · 2024-02-16T09:40:49Z

Take it easy

I think @jrtc27's response was very measured. This repo is quite slow moving - partly because we don't have very good testing yet - so you have to be quite patient! Can be a little frustrating at times but there you go. I think the situation will improve eventually.

Anyway back to the engineering... I had another idea about testing this. Since Sail can generate SMT2, and the CVC5 SMT solver understands IEEE float, we can in theory formally prove the Sail implementation (modulo bugs in CVC5 but I guess their implementation must be pretty well tested right?).

I had a go at this. Here's the 64-bit float equals extracted into a standalone file:


default Order dec

$include <prelude.sail>
$include <string.sail>

overload operator ^ = {concat_str}

val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)

function sign_extend(m, v) = sail_sign_extend(v, m)
function zero_extend(m, v) = sail_zero_extend(v, m)

val zeros : forall 'n, 0 <= 'n <= 64 . implicit('n) -> bits('n)
function zeros (n) = sail_zeros (n)

val ones : forall 'n, 0 <= 'n <= 64 . implicit('n) -> bits('n)
function ones (n) = sail_ones (n)

infix 7 >>
infix 7 <<

val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
val "shift_bits_left"  : forall 'n 'm. (bits('n), bits('m)) -> bits('n)

val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)

overload operator >> = {shift_bits_right, shiftr}
overload operator << = {shift_bits_left, shiftl}

val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))

function main() -> unit = ()

// --------------------------------------------

type bits_rm     = bits(3)    /* Rounding mode */
type bits_fflags = bits(5)    /* Accrued exceptions: NV,DZ,OF,UF,NX */
type bits_H      = bits(16)   /* Half-precision float value */
type bits_S      = bits(32)   /* Single-precision float value */
type bits_D      = bits(64)   /* Double-precision float value */

type bits_W      = bits(32)   /* Signed integer */
type bits_WU     = bits(32)   /* Unsigned integer */

type bits_L      = bits(64)   /* Signed integer */
type bits_LU     = bits(64)   /* Unsigned integer */

let float_flag_invalid : bits_fflags = 0b10000

val      fsplit_D : bits(64) -> (bits(1), bits(11), bits(52))
function fsplit_D   x64 = (x64[63..63], x64[62..52], x64[51..0])

val      f_is_SNaN_D : bits(64) -> bool
function f_is_SNaN_D   x64 = {
  let (sign, exp, mant) = fsplit_D (x64);
  (  (exp == 0b11111111111)
   & (mant [51] == bitzero)
   & (mant != 0b0000000000000000000000000000000000000000000000000000))
}

/* Either QNaN or SNan */
val      f_is_NaN_D : bits(64) -> bool
function f_is_NaN_D   x64 = {
  let (sign, exp, mant) = fsplit_D (x64);
  (  (exp == 0b11111111111)
   & (mant != 0b0000000000000000000000000000000000000000000000000000))
}

val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool
function f_is_SNaN(xf) = {
  match 'm {
    // 16 => f_is_SNaN_H(xf),
    // 32 => f_is_SNaN_S(xf),
    64 => f_is_SNaN_D(xf),
    _ => false,
  }
}

val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool
function f_is_NaN(xf) = {
  match 'm {
    // 16 => f_is_NaN_H(xf),
    // 32 => f_is_NaN_S(xf),
    64 => f_is_NaN_D(xf),
    _ => false,
  }
}

val      float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool)
function float_eq (op1, op2) = {
  let is_nan          = f_is_NaN(op1) | f_is_NaN(op2);
  let is_snan         = f_is_SNaN(op1) | f_is_SNaN(op2);
  let fflags          = if   is_nan & is_snan
                        then float_flag_invalid
                        else zeros();
  let is_equal : bool = if   not(is_nan)
                        then op1 == op2 | ((op1 | op2) << 1) == zeros()
                        else false;

  (fflags, is_equal)
}

function float_eq_64(op1 : bits(64), op2 : bits(64)) -> bool = {
    let (_, is_equal) = float_eq(op1, op2);
    is_equal
}

$counterexample
function prop(op1 : bits(64), op2 : bits(64)) -> bool = {
  (op1 == op2) == float_eq_64(op1, op2)
}

If you now do this:

sail --smt test.sail -o build/model_smt --smt-auto

It will compile it to SMT2 and run it through CVC4. Of course in this case it is able to generate a counterexample because prop is wrong:

Checking counterexample: build/model_smt_prop.smt2
Solver found counterexample: ok
  op1 -> 0x0000000000000000
  op2 -> 0x8000000000000000
Replaying counterexample: ok

I.e. it found -0 == 0.

We can run cvc5 directly and it will print the same thing in a much more awkward form:

❯ cvc5 model_smt_prop.smt2 
sat
(
(define-fun zz44/1 () (_ BitVec 64) #b1111111111111111111111111111111111111111111111111111111111111111)
(define-fun zz45/1 () (_ BitVec 64) #b1111111111111111111111111111111111111111111111111111111111111111)
(define-fun zz498/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz482/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz464/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz445/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz415/1 () (Tup2 (_ BitVec 5) Bool) ((as tup2 (Tup2 (_ BitVec 5) Bool)) #b00000 false))
)

The generated SMT2 looks like this:

(set-option :produce-models true)
(set-logic QF_AUFBVDT)
(declare-datatypes ((Unit 0)) (((unit))))
(declare-datatypes ((Tup2 2)) ((par (T0 T1) ((tup2 (tup_2_0 T0) (tup_2_1 T1))))))
(declare-datatypes ((Tup3 3)) ((par (T0 T1 T2) ((tup3 (tup_3_0 T0) (tup_3_1 T1) (tup_3_2 T2))))))
(declare-datatypes ((Bits 0)) (((Bits (len (_ BitVec 8)) (contents (_ BitVec 256))))))
(declare-datatypes ((Zexception 0)) (((z__dummy_exnz3 (unz__dummy_exnz3 Unit)))))
(declare-const zz44/1 (_ BitVec 64))
(declare-const zz45/1 (_ BitVec 64))
(declare-const zz498/1 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)))
(define-const zz498/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 ((_ extract 63 63) zz44/1) (tup_3_1 zz498/1) (tup_3_2 zz498/1)))
(define-const zz498/3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz498/2) ((_ extract 62 52) zz44/1) (tup_3_2 zz498/2)))
(define-const zz487/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz498/3) (tup_3_1 zz498/3) ((_ extract 51 0) zz44/1)))
(define-const zz465/2 Bool (ite (= (tup_3_1 zz487/2) #b11111111111) (not (= (tup_3_2 zz487/2) #x0000000000000)) false))
(declare-const zz482/1 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)))
(define-const zz482/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 ((_ extract 63 63) zz45/1) (tup_3_1 zz482/1) (tup_3_2 zz482/1)))
(define-const zz482/3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz482/2) ((_ extract 62 52) zz45/1) (tup_3_2 zz482/2)))
(define-const zz471/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz482/3) (tup_3_1 zz482/3) ((_ extract 51 0) zz45/1)))
(define-const zz411/2 Bool (ite (not zz465/2) (ite (not zz465/2) (ite (and (= (tup_3_1 zz471/2) #b11111111111) (not zz465/2)) (not (= (tup_3_2 zz471/2) #x0000000000000)) false) false) true))
(declare-const zz464/1 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)))
(define-const zz464/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 ((_ extract 63 63) zz44/1) (tup_3_1 zz464/1) (tup_3_2 zz464/1)))
(define-const zz464/3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz464/2) ((_ extract 62 52) zz44/1) (tup_3_2 zz464/2)))
(define-const zz450/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz464/3) (tup_3_1 zz464/3) ((_ extract 51 0) zz44/1)))
(define-const zz454/2 (_ BitVec 52) (tup_3_2 zz450/2))
(define-const zz455/2 Bool (= (tup_3_1 zz450/2) #b11111111111))
(define-const zz457/2 Bool (= ((_ extract 51 51) zz454/2) #b0))
(define-const zz411/3 Bool zz411/2)
(define-const zz425/2 Bool (ite (not zz455/2) false (ite (and zz457/2 zz455/2) (not (= zz454/2 #x0000000000000)) false)))
(declare-const zz445/1 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)))
(define-const zz445/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 ((_ extract 63 63) zz45/1) (tup_3_1 zz445/1) (tup_3_2 zz445/1)))
(define-const zz445/3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz445/2) ((_ extract 62 52) zz45/1) (tup_3_2 zz445/2)))
(define-const zz431/2 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) (tup3 (tup_3_0 zz445/3) (tup_3_1 zz445/3) ((_ extract 51 0) zz45/1)))
(define-const zz435/2 (_ BitVec 52) (tup_3_2 zz431/2))
(define-const zz436/2 Bool (= (tup_3_1 zz431/2) #b11111111111))
(define-const zz438/2 Bool (= ((_ extract 51 51) zz435/2) #b0))
(define-const zz411/7 Bool zz411/3)
(define-const zz411/8 Bool zz411/7)
(define-const zz423/2 Bool (ite (not zz411/7) false (ite (not zz425/2) (ite (not zz425/2) (ite (and (not zz436/2) (not zz425/2)) false (ite (and zz438/2 zz436/2 (not zz425/2)) (not (= zz435/2 #x0000000000000)) false)) false) true)))
(define-const zz413/4 (_ BitVec 5) (ite (not zz423/2) #b00000 #b10000))
(define-const zz416/2 Bool (not zz411/8))
(define-const zz417/2 Bool (= zz44/1 zz45/1))
(declare-const zz415/1 (Tup2 (_ BitVec 5) Bool))
(assert (not (and (or (not zz416/2) zz416/2) (= (= zz44/1 zz45/1) (tup_2_1 (tup2 (tup_2_0 (tup2 zz413/4 (tup_2_1 zz415/1))) (ite (not zz416/2) false (ite (and (not zz417/2) zz416/2) (= (bvshl (bvor zz44/1 zz45/1) #x0000000000000001) #x0000000000000000) true))))))))
(check-sat)
(get-model)

With a lot of squinting you can find the (= zz44/1 zz45/1) bit which corresponds to (op1 == op2) in prop(). We can now replace that with an actual floating point comparison based on the theory of floating point. I have no idea what I'm doing btw.

...
(assert (not (and (or (not zz416/2) zz416/2)(= (
    fp.eq (
        (_ to_fp 11 53) zz44/1
    ) (
        (_ to_fp 11 53) zz45/1
    ))
    (tup_2_1 (tup2 (tup_2_0 (tup2 zz413/4 (tup_2_1 zz415/1))) (ite (not zz416/2) false (ite (and (not zz417/2) zz416/2) (= (bvshl (bvor zz44/1 zz45/1) #x0000000000000001) #x0000000000000000) true)))))
)))
...

It doesn't quite work because it doesn't know about to_fp yet. That turned out to be because you have to modify set-logic. Unfortunately the docs for that are not great, don't explain how this string works and still say FP is forthcoming (it isn't). I ended up reading the source code which was mercifully simple. Anyway change the logic to:

(set-logic QF_AUFBVFPDT)

And tada!

❯ cvc5 model_smt_prop.smt2 
unsat
(error "Cannot get model unless after a SAT or UNKNOWN response.")

I double checked by introducing a bug:

                        then op1 == op2 | ((op1 | op2) << 1) == zeros()
->
                        then op1 == op2 | ((op1 & op2) << 1) == zeros()

Then

❯ cvc5 model_smt_prop.smt2
sat
(
(define-fun zz44/1 () (_ BitVec 64) #b0111111111110000000000000000000000000000000000000000000000000000)
(define-fun zz45/1 () (_ BitVec 64) #b0000000000000000000000000000000000000000000000000000000000000001)
(define-fun zz498/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz482/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz464/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz445/1 () (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52)) ((as tup3 (Tup3 (_ BitVec 1) (_ BitVec 11) (_ BitVec 52))) #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun zz415/1 () (Tup2 (_ BitVec 5) Bool) ((as tup2 (Tup2 (_ BitVec 5) Bool)) #b00000 false))
)

This seems like it will be a really easy method, except that it's very tedious to edit the SMT2. We probably want some support from the Sail compiler. Maybe a way to export functions as SMT2 functions? Like this:

sail --smt --smt-preserve float_eq_64

Another downside is that it can't verify raising flags as far as I can see.

@Alasdair fyi.

@Incarnation-p-lee if you implement a more complex function (maybe division?) I can try to prove it like this.

Incarnation-p-lee · 2024-02-16T10:30:33Z

Take it easy

I think @jrtc27's response was very measured. This repo is quite slow moving - partly because we don't have very good testing yet - so you have to be quite patient! Can be a little frustrating at times but there you go. I think the situation will improve eventually.

Thanks @Timmmm for the explain. Got you point here and I believe we can have a test framework for the sail code eventually.

@Incarnation-p-lee if you implement a more complex function (maybe division?) I can try to prove it like this.

Not sure my understanding is correct but can we perform both the float point migration work and a test framework for sail code? I think they should be independent in most cases, as well as we need this for the complex (strictly for simple API like equal too) cases.

From the materials you shared, it looks like we need some time to work out a test framework but I would like to have a try for your proposal(Sorry I have no idea about SMT2, and CVC2, so no suggestion from myside, :)).

I notice you have shared more extensive tests (I bet it is well designed for float). I wonder if we can port these test cases to sail and find a place to run/execute them. Because the test files can be considered as(or easily convert to) another sort of API(s). They should be visible for any other sail code. However I am not familiar with the sail compiler, just brainstorm here.

Timmmm · 2024-02-16T13:46:28Z

an we perform both the float point migration work and a test framework for sail code

I mean we can test the Sail implementations of floating point by formally verifying them against the SMTLIB2 implementation.

it looks like we need some time to work out a test framework

Yeah... though I'm not sure you need a whole framework. I think if Sail supported --smt-preserve then all you need to do is:

Add a target to the Makefile that runs sail --smt $(SAIL_SRC) --smt-preserve <list of float functions>
Appends a file containing all the (assert ...)s to the SMTLIB2 output.
Run cvc5 on that file.

I wonder if we can port these test cases to sail and find a place to run/execute them.

Yeah definitely. Shouldn't be too hard; you just need to make them write to the HTIF interface that Sail uses (it's very simple) for UART and exit status and then cross-compile to RISC-V.

Timmmm · 2024-02-16T14:17:20Z

--smt-preserve

Actually I had a sudden thought... turns out Sail already supports declaring extern smt functions. So you can just do this:

val float_eq_64_smt = pure {smt: "float_eq_64_smt"} : (bits(64), bits(64)) -> bool

$counterexample
function prop(op1 : bits(64), op2 : bits(64)) -> bool = {
  float_eq_64_smt(op1, op2) == float_eq_64(op1, op2)
}

Then you only need to modify the top of the output file to

(set-logic QF_AUFBVFPDT)
(define-fun zfloat_eq_64_smt ((op1 (_ BitVec 64)) (op2 (_ BitVec 64))) Bool (fp.eq ((_ to_fp 11 53) op1) ((_ to_fp 11 53) op2)))

So actually all we need is to change the set-logic value in the Sail compiler (you can trick it into using QF_ALL if you use strings or reals apparently), and to have a way to somehow #include external SMT2 definitions.

Timmmm · 2024-02-16T15:04:34Z

Ok I hacked up a patch to the Sail compiler to switch to CVC5, update the set-logic string and support --smt-include, and it totally works.

Sail property:

function float_eq_64(op1 : bits(64), op2 : bits(64)) -> bool = {
    let (_, is_equal) = float_eq(op1, op2);
    is_equal
}

val float_eq_64_smt = pure {smt: "float_eq_64_smt"} : (bits(64), bits(64)) -> bool

$counterexample
function prop(op1 : bits(64), op2 : bits(64)) -> bool = {
  float_eq_64_smt(op1, op2) == float_eq_64(op1, op2)
}

Then

❯ cat src/float_proof_util.smt2 
(define-fun zfloat_eq_64_smt ((op1 (_ BitVec 64)) (op2 (_ BitVec 64))) Bool (fp.eq ((_ to_fp 11 53) op1) ((_ to_fp 11 53) op2)))

❯ sail --smt src/test.sail --smt-include src/float_proof_util.smt2 -o build/model_smt --smt-auto
Checking counterexample: build/model_smt_prop.smt2
Solver could not find counterexample

❯ # Introduce bug, then...

❯ sail --smt src/test.sail --smt-include src/float_proof_util.smt2 -o build/model_smt --smt-auto
Checking counterexample: build/model_smt_prop.smt2
Solver found counterexample: ok
  op1 -> 0x7FF0000000000000
  op2 -> 0x0000000000000001
Replaying counterexample: ok

I'll send @Alasdair the patch at some point. Better do some real work now...

Incarnation-p-lee · 2024-02-17T10:27:59Z

Ok I hacked up a patch to the Sail compiler to switch to CVC5, update the set-logic string and support --smt-include, and it totally works.

Sail property:

function float_eq_64(op1 : bits(64), op2 : bits(64)) -> bool = {
    let (_, is_equal) = float_eq(op1, op2);
    is_equal
}

val float_eq_64_smt = pure {smt: "float_eq_64_smt"} : (bits(64), bits(64)) -> bool

$counterexample
function prop(op1 : bits(64), op2 : bits(64)) -> bool = {
  float_eq_64_smt(op1, op2) == float_eq_64(op1, op2)
}

Then

❯ cat src/float_proof_util.smt2 
(define-fun zfloat_eq_64_smt ((op1 (_ BitVec 64)) (op2 (_ BitVec 64))) Bool (fp.eq ((_ to_fp 11 53) op1) ((_ to_fp 11 53) op2)))

❯ sail --smt src/test.sail --smt-include src/float_proof_util.smt2 -o build/model_smt --smt-auto
Checking counterexample: build/model_smt_prop.smt2
Solver could not find counterexample

❯ # Introduce bug, then...

❯ sail --smt src/test.sail --smt-include src/float_proof_util.smt2 -o build/model_smt --smt-auto
Checking counterexample: build/model_smt_prop.smt2
Solver found counterexample: ok
  op1 -> 0x7FF0000000000000
  op2 -> 0x0000000000000001
Replaying counterexample: ok

I'll send @Alasdair the patch at some point. Better do some real work now...

That would be great! I think it is good enough to port the test to sail and add a new target to run (includes CI/CD). I will have a try once the sail compiler is ready. Thanks a lot for this.

Incarnation-p-lee · 2024-03-25T11:31:04Z

Hi @Timmmm

I have a try to make COVERAGE=1 for the c code line coverage (I suppose it cannot cover the sail code) but meet below issue when ARCH=RV64 make SAILCOV=1 c_emulator/riscv_sim_RV64.

/usr/bin/ld: cannot find ~/.opam/5.1.0/share/sail/lib/coverage/libsail_coverage.a: No such file or directory

Could you please help to insight me is there anything/step(s) missing here?

Alasdair · 2024-03-25T14:27:49Z

It's coverage of the Sail code that it's measuring, there's a small library here that it links into the generated binary and measures the coverage. It's available here: https://github.com/rems-project/sail/tree/sail2/lib/coverage

Incarnation-p-lee · 2024-03-26T01:23:29Z

It's coverage of the Sail code that it's measuring, there's a small library here that it links into the generated binary and measures the coverage. It's available here: https://github.com/rems-project/sail/tree/sail2/lib/coverage

Thanks, let me have a try.

Incarnation-p-lee · 2024-03-27T01:12:59Z

Hi @billmcspadden-riscv

Just have a try for the sail model coverage by run_fp_tests.sh, and here is the snapshot for equal API. You can also find more details in the attachments.

Given that, shall we move forward for simple API porting like compare, or wait for the softfloat testsuite with the upgraded sail compiler?

Both approaches are LGTM.

riscv_float_eq.zip

Timmmm

Btw a couple of minor simplifications I noticed. The old code wasn't wrong - just could be simplified a bit.

Timmmm · 2024-04-03T16:09:31Z

model/float/riscv_float_eq.sail

+function float_eq (op1, op2) = {
+ let is_nan = f_is_NaN(op1) | f_is_NaN(op2);
+ let is_snan = f_is_SNaN(op1) | f_is_SNaN(op2);
+ let fflags = if is_nan & is_snan


is_nan & can be removed here because is_snan is a subset of is_nan.

Timmmm · 2024-04-03T16:10:42Z

model/float/riscv_float_eq.sail

+ let fflags = if is_nan & is_snan
+ then float_flag_invalid
+ else zeros();
+ let is_equal : bool = if not(is_nan)


This can be simplified to the following:

let is_equal = not(is_nan) & (op1 == op2 | ((op1 | op2) << 1) == zeros());

Updated and removed the bool declaration.

Incarnation-p-lee · 2024-04-04T00:29:09Z

Btw a couple of minor simplifications I noticed. The old code wasn't wrong - just could be simplified a bit.

Thanks Tim, that make sense to me. Let me update it.

BTW, the float will be promoted to a standalone lib (as well as its test suite) in sail, thus I suppose we don't need this anymore.

Signed-off-by: Pan Li <pan2.li@intel.com>

Timmmm · 2024-04-04T09:41:39Z

Thanks! This LGTM and I think we could land it, but if you intend to make it into a separate library I guess that's fine too. A library sounds like a good idea to me.

Incarnation-p-lee · 2024-04-04T10:50:47Z

Thanks @Timmmm for the review and help, learned a lot from the expert like you!

Shall we keep this open until we integrate this repo with the new float standalone lib? Or just close it. Both are Ok to me.

Timmmm · 2024-04-04T11:34:08Z

Yeah lets leave it open in case the standalone lib doesn't happen for some reason.

Timmmm · 2024-05-20T10:54:49Z

Seems like the float lib in the Sail compiler is going extremely well so I'll close this. Hope that's ok @Incarnation-p-lee!

Incarnation-p-lee · 2024-05-20T10:57:21Z

Seems like the float lib in the Sail compiler is going extremely well so I'll close this. Hope that's ok @Incarnation-p-lee!

That is all right, thanks @Timmmm for following up.

arichardson reviewed Feb 7, 2024

View reviewed changes

Incarnation-p-lee force-pushed the master branch from 3f2f277 to 2923e21 Compare February 7, 2024 09:04

Timmmm reviewed Feb 7, 2024

View reviewed changes

model/riscv_insts_vext_utils.sail Outdated Show resolved Hide resolved

Timmmm requested changes Feb 7, 2024

View reviewed changes

Rename softfloat to float.

679565c

Signed-off-by: Pan Li <pan2.li@intel.com>

Address comments.

7aac800

Signed-off-by: Pan Li <pan2.li@intel.com>

Merge branch 'master' into master

4b692d2

Remove the depends on softfloat_interface

4c14715

Signed-off-by: Pan Li <pan2.li@intel.com>

Cleanup format.

d756053

Signed-off-by: Pan Li <pan2.li@intel.com>

Timmmm reviewed Feb 12, 2024

View reviewed changes

Address comments.

a05b202

Signed-off-by: Pan Li <pan2.li@intel.com>

Timmmm approved these changes Feb 13, 2024

View reviewed changes

jrtc27 reviewed Feb 14, 2024

View reviewed changes

Address comments.

3200049

Signed-off-by: Pan Li <pan2.li@intel.com>

jjscheel mentioned this pull request Feb 20, 2024

Sail Softfloat Replacement riscv-admin/dev-partners#40

Open

13 tasks

billmcspadden-riscv added the tgmm-agenda Tagged for the next Golden Model meeting agenda. label Mar 25, 2024

Merge branch 'master' into master

42396c9

Merge branch 'master' into master

9f41f24

Timmmm requested changes Apr 3, 2024

View reviewed changes

Incarnation-p-lee and others added 3 commits April 4, 2024 08:36

Address comments for code simplify.

88568f8

Signed-off-by: Pan Li <pan2.li@intel.com>

Merge remote-tracking branch 'origin/master'

d9d6b92

Merge branch 'master' into master

a4ce269

Timmmm approved these changes Apr 4, 2024

View reviewed changes

Timmmm closed this May 20, 2024

Float: Add floating-point equals API in sail model #403

Float: Add floating-point equals API in sail model #403

Conversation

Incarnation-p-lee commented Feb 7, 2024 • edited Loading

arichardson left a comment

Choose a reason for hiding this comment

Incarnation-p-lee commented Feb 7, 2024

Timmmm commented Feb 7, 2024

Incarnation-p-lee commented Feb 7, 2024

jrtc27 commented Feb 7, 2024

Incarnation-p-lee commented Feb 8, 2024 • edited Loading

Timmmm commented Feb 12, 2024

Incarnation-p-lee commented Feb 12, 2024

Incarnation-p-lee commented Feb 12, 2024

Timmmm left a comment

Choose a reason for hiding this comment

Incarnation-p-lee commented Feb 13, 2024

Timmmm commented Feb 13, 2024

Incarnation-p-lee commented Feb 13, 2024

Timmmm commented Feb 13, 2024

billmcspadden-riscv commented Feb 13, 2024 via email

Incarnation-p-lee commented Feb 13, 2024

Timmmm commented Feb 13, 2024

Incarnation-p-lee commented Feb 14, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jrtc27 commented Feb 16, 2024

Incarnation-p-lee commented Feb 16, 2024 • edited Loading

Incarnation-p-lee commented Feb 16, 2024

Timmmm commented Feb 16, 2024

Incarnation-p-lee commented Feb 16, 2024

Timmmm commented Feb 16, 2024

Timmmm commented Feb 16, 2024

Timmmm commented Feb 16, 2024

Incarnation-p-lee commented Feb 17, 2024

Incarnation-p-lee commented Mar 25, 2024

Alasdair commented Mar 25, 2024

Incarnation-p-lee commented Mar 26, 2024

Incarnation-p-lee commented Mar 27, 2024

Timmmm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Incarnation-p-lee commented Apr 4, 2024

Timmmm commented Apr 4, 2024

Incarnation-p-lee commented Apr 4, 2024 • edited Loading

Timmmm commented Apr 4, 2024

Timmmm commented May 20, 2024

Incarnation-p-lee commented May 20, 2024

Incarnation-p-lee commented Feb 7, 2024 •

edited

Loading

Incarnation-p-lee commented Feb 8, 2024 •

edited

Loading

Incarnation-p-lee commented Feb 16, 2024 •

edited

Loading

Incarnation-p-lee commented Apr 4, 2024 •

edited

Loading