Sail Softfloat Replacement

[jjscheel]

Technical Group

Applications & Tools HC

ratification-pkg

Technical Debt

Technical Liaison

Bill McSpadden

Task Category

Sail

Task Sub Category

• gcc
• binutils
• gdb
• intrinsics
• Java
• KVM
• ld
• llvm
• Linux kernel
• QEMU
• Spike

Ratification Target

3Q2023

Statement of Work (SOW)

Component names:
Sail

Requirements:
In the RISC-V Sail model, floating point operations are implemented (executed) using the Berkley SoftFloat package (written by John Hauser). See: https://github.com/riscv/sail-riscv/tree/master/c_emulator/SoftFloat-3e
This code is written in C in roughly 320 files and 37K lines of code. (Note: some of this work has already been done in support of Vector Crypto by Charalampos Mitrodimas.)

The functionality in SoftFloat needs to be replicated in native Sail code. The primary purpose of this project is to provide a native Sail description of floating point operations which can be used as the canonical definition of FP ops for RISC-V. This Sail code can be imported into the RISC-V ISA documentation.

The API interface for floating point ops must remain the same.

Deliverables:

1. Set of Sail files that fully implement the functionality of SoftFloat. The code will live in the RISC-V Sail (golden model) repository.

Acceptance Criteria:

1. Approved PR to the Sail community for all code.
2. ACT test results equivalency between new and Softfloat (prior) code bases.

Projected timeframe: (best guess date)
6 person months

SOW Signoffs: (delete those not needed)

• Development partner sign-off
• Golden Model SIG sign-off (if SAIL work)

Waiver

• Freeze
• Ratification

Pull Request Details

• Float: Add floating-point equals API in sail model - PR #403: Deprecated
• Float: Introduce floating point api NAN - #493: Merged
• Remove undefined_gen for if-else type float_bits - #516: Merged
• Float: Introduce floating point api infinite - #522: Merged
• Float: Delete error result file if test pass - #521: Merged
• Float: Fix comments typo in test and align space format - #533: Merged
• Float: Introduce floating point api sign - #542: Merged
• Float: Introduce floating point api zero - #563: Merged

[Incarnation-p-lee]

Thank @jjscheel for the clear description of this task.

Hi @billmcspadden-riscv

Just went through the SoftFloat, and would like to double-check if my understanding is correct before any further actions.

Currently, the sail-riscv c_emulator has riscv_softfloat.c, which leverages the SoftFloat library/package. For example, the function softfloat_f64roundToInt depends on the f64_roundToInt (implemented in SoftFloat-3e/source/f64_roundToInt.c). And we need to migrate the c-implemented code to the sail (aka ./model as I understand). Then the e_emulator can leverage the generated code (by sail model) instead of the SoftFloat library/package.

Unfortunately, my previous experience almost focuses on c, java, c#, and of course the green hand for sail. Could you please help to share some guide or something like that as above mentioned that part of works has done for supporting RVV Crypto. I think I need to try some POC by myself first, and then evaluate the efforts, as well as the plan for the task.

CC @haicheng-li

[Incarnation-p-lee]

Table of contents

• Table of contents
  • What we have
  • What we would like to do
  • How we land
  • Sail Function to be Implemented
    • Not start
    • Under Review
    • Completed
  • Issues

I summarize what I have learned about the softfloat as below and possible work items. Could you please help to double-check if everything is correct? Then we can start the work step by step.

What we have

The riscv insn sail models treat the model/riscv_softfloat_interface.sail as the contract of how to leverage the softfloat externally. Like in c_emulator. For example, the sail function riscv_f32Eq in the model/riscv_softfloat_interface.sail will call externally to the function softfloat_f32eq in c_emulator/riscv_softfloat.c.

graph LR
  subgraph The C Emulator
    B1[softfloat]
  end

  subgraph Sail Models
    A1[riscv-insn-fp-*] --depends on--> A2[riscv_software_interface] --external call--> B1
  end

Loading

What we would like to do

AFAIK, we would like to get rid of the c_mulator/riscv_softfloat, and implement the softfloat in the sail language. And then eliminate the c_emulator/softfloat in this repo.

graph LR
  subgraph The C Emulator
    B1[softfloat]
  end

  subgraph Sail Models
    A1[riscv-insn-fp-*] --depends on--> A2[riscv_software_interface] --call--> A3[softfloat in sail]
    A2 x--external call--x B1
  end

Loading

How we land

For safe consideration, I may suggest we still treat the model/riscv_softfloat_interface.sai as the contract, and only replace the external call to c_emulator/software one by one. For example:

// val     extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit                                                                                                             val      riscv_softfloat_f32_eq : (bits_S, bits_S) -> unit
val      riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool)
function riscv_f32Eq (v1, v2) = {
  riscv_softfloat_f32_eq(v1, v2);
  // extern_f32Eq(v1, v2);
  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

Then we only need to implement the sail function riscv_softfloat_f32_eq somewhere else and limit the risk to the existing sail modes. For example, I may suggest we take the below arrangement. And we can even parallel the implementation under softfloat folder once stable. Finally, it looks like we may not need implement everything of e_emulator/software up to a point.

model/
├── README.md
├── riscv_softfloat_interface.sail
└── float
    ├── riscv_float_eq.sail
    ├── riscv_float_lt.sail
    └── riscv_float_gt.sail

Sail Function to be Implemented

According to the API defined in riscv_software_interface, at least we have below sail function to be implemented.

Not start

• riscv_f16Add
• riscv_f16Sub
• riscv_f16Mul
• riscv_f16Div
• riscv_f32Add
• riscv_f32Sub
• riscv_f32Mul
• riscv_f32Div
• riscv_f64Add
• riscv_f64Sub
• riscv_f64Mul
• riscv_f64Div
• riscv_f16MulAdd
• riscv_f32MulAdd
• riscv_f64MulAdd
• riscv_f16Sqrt
• riscv_f32Sqrt
• riscv_f64Sqrt
• riscv_f16ToI32
• riscv_f16ToUi32
• riscv_i32ToF16
• riscv_ui32ToF16
• riscv_f16ToI64
• riscv_f16ToUi64
• riscv_i64ToF16
• riscv_ui64ToF16
• riscv_f32ToI32
• riscv_f32ToUi32
• riscv_i32ToF32
• riscv_ui32ToF32
• riscv_f32ToI64
• riscv_f32ToUi64
• riscv_i64ToF32
• riscv_ui64ToF32
• riscv_f64ToI32
• riscv_f64ToUi32
• riscv_i32ToF64
• riscv_ui32ToF64
• riscv_f64ToI64
• riscv_f64ToUi64
• riscv_i64ToF64
• riscv_ui64ToF64
• riscv_f16ToF32
• riscv_f16ToF64
• riscv_f32ToF64
• riscv_f32ToF16
• riscv_f64ToF16
• riscv_f64ToF32
• riscv_f16Lt
• riscv_f16Lt_quiet
• riscv_f16Le
• riscv_f16Le_quiet
• riscv_f32Lt
• riscv_f32Lt_quiet
• riscv_f32Le
• riscv_f32Le_quiet
• riscv_f64Lt
• riscv_f64Lt_quiet
• riscv_f64Le
• riscv_f64Le_quiet
• riscv_f16roundToInt
• riscv_f32roundToInt
• riscv_f64roundToIn

Under Review

• riscv_f64Eq
• riscv_f32Eq
• riscv_f16Eq

Completed

Issues

• The Softfloat DO NOT contain any test for the correctness(Only run_test.sh for all riscv insn tests). To ensure the correctness, looks we need to port the softfloat_3e_test. Need input from both Jeff and Bill.

CC @haicheng-li for awareness.

[billmcspadden-riscv]

Side comment: Because this is such a large change to the code, we don't want to have a large PR to review. Please consider how you might subdivide the problem such that we only have to review 1000-2000 lines of code at a time. Bill Mc.

…

On Tue, Feb 6, 2024 at 3:15 AM Pan Li ***@***.***> wrote: I summarize what I have learned about the softfloat as below and possible work items. Could you please help to double-check if everything is correct? Then we can start the work step by step. What we have The riscv insn sail models treat the model/riscv_softfloat_interface.sail as the contract of how to leverage the softfloat externally. Like in c_emulator. For example, the sail function riscv_f32Eq in the model/riscv_softfloat_interface.sail will call externally to the function softfloat_f32eq in c_emulator/riscv_softfloat.c. graph LR subgraph The C Emulator B1[softfloat] end subgraph Sail Models A1[riscv-insn-fp-*] --depends on--> A2[riscv_software_interface] --extern call--> B1 end What we would like to do AFAIK, we would like to get rid of the c_mulator/riscv_softfloat, and implement the softfloat in the sail language. And then eliminate the c_emulator/softfloat in this repo. graph LR subgraph The C Emulator B1[softfloat] end subgraph Sail Models A1[riscv-insn-fp-*] --depends on--> A2[riscv_software_interface] --call--> A3[softfloat in sail] A2 x--external call--x B1 end How we land For safe consideration, I may suggest we still treat the model/riscv_softfloat_interface.sai as the contract, and only replace the external call to c_emulator/software one by one. For example: // val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit val riscv_softfloat_f32_eq : (bits_S, bits_S) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { riscv_softfloat_f32_eq(v1, v2); // extern_f32Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } Then we only need to implement the sail function riscv_softfloat_f32_eq somewhere else and limit the risk to the existing sail modes. For example, I may suggest we take the below arrangement. And we can even parallel the implementation under softfloat folder once stable. Finally, it looks like we may not need implement everything of e_emulator/software up to a point. model/ ├── README.md ├── riscv_softfloat_interface.sail └── softfloat ├── riscv_softfloat_eq.sail ├── riscv_softfloat_lt.sail └── riscv_softfloat_gt.sail Sail Function to be Implemented According to the API defined in riscv_software_interface, at least we have below sail function to be implemented. - riscv_f16Add - riscv_f16Sub - riscv_f16Mul - riscv_f16Div - riscv_f32Add - riscv_f32Sub - riscv_f32Mul - riscv_f32Div - riscv_f64Add - riscv_f64Sub - riscv_f64Mul - riscv_f64Div - riscv_f16MulAdd - riscv_f32MulAdd - riscv_f64MulAdd - riscv_f16Sqrt - riscv_f32Sqrt - riscv_f64Sqrt - riscv_f16ToI32 - riscv_f16ToUi32 - riscv_i32ToF16 - riscv_ui32ToF16 - riscv_f16ToI64 - riscv_f16ToUi64 - riscv_i64ToF16 - riscv_ui64ToF16 - riscv_f32ToI32 - riscv_f32ToUi32 - riscv_i32ToF32 - riscv_ui32ToF32 - riscv_f32ToI64 - riscv_f32ToUi64 - riscv_i64ToF32 - riscv_ui64ToF32 - riscv_f64ToI32 - riscv_f64ToUi32 - riscv_i32ToF64 - riscv_ui32ToF64 - riscv_f64ToI64 - riscv_f64ToUi64 - riscv_i64ToF64 - riscv_ui64ToF64 - riscv_f16ToF32 - riscv_f16ToF64 - riscv_f32ToF64 - riscv_f32ToF16 - riscv_f64ToF16 - riscv_f64ToF32 - riscv_f16Lt - riscv_f16Lt_quiet - riscv_f16Le - riscv_f16Le_quiet - riscv_f16Eq - riscv_f32Lt - riscv_f32Lt_quiet - riscv_f32Le - riscv_f32Le_quiet - riscv_f32Eq - riscv_f64Lt - riscv_f64Lt_quiet - riscv_f64Le - riscv_f64Le_quiet - riscv_f64Eq - riscv_f16roundToInt - riscv_f32roundToInt - riscv_f64roundToIn Issues I am working on one POC of a simple API like f32eq, and there are some global variables like floating control and status flags .. etc, will keep you all posted. CC @haicheng-li <https://github.com/haicheng-li> for awareness. — Reply to this email directly, view it on GitHub <#40 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOBBJI7DAEHKNTYW3ODYSIGF3AVCNFSM6AAAAABCRDLEGSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMRZGMYDCMZQG4> . You are receiving this because you were mentioned.Message ID: ***@***.***>

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

[Incarnation-p-lee]

Sure thing, actually I may prefer 200-300(excludes test code) lines per PR for review. By the way, does sail-riscv repo take Merge or Squash Merge for PR?

[Incarnation-p-lee]

Status Update Mar 4, 2024

• PR Float Equal updated in Feb 16, 2024, waiting for further review.

[Incarnation-p-lee]

Thanks @jjscheel for the SOW description. ACK the SOW from my side.

To clarify, please feel free to comment if any concerns or questions about below open issue.

• The softfloat_3e_test porting to sail-riscv is NOT in the scope of this SOW due to some more support required from the sail compiler. If so I think we need to record it by a task somewhere.

[billmcspadden-riscv]

Hi Pan. Would you please explain a bit more about "more support required from the sail compiler". As I understand it, TestFloat is a set of tests for checking the implementation of a binary floating point library. How does this have anything to do with the Sail compiler? Bill Mc.

…

On Tue, Mar 5, 2024 at 5:41 PM Pan Li ***@***.***> wrote: Thanks @jjscheel <https://github.com/jjscheel> for the SOW description. ACK the SOW from my side. To clarify, please feel free to comment if any concerns or questions about below open issue. - The softfloat_3e_test <http://www.jhauser.us/arithmetic/TestFloat.html> porting to sail-riscv is *NOT* in the scope of this SOW due to some more support required from the sail compiler. If so I think we need to record it by a task somewhere. — Reply to this email directly, view it on GitHub <#40 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOCJ7KFM3Q3JCODASDLYWZX3NAVCNFSM6AAAAABCRDLEGSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZZHEZDKNZYGE> . You are receiving this because you were mentioned.Message ID: ***@***.***>

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