diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-23 12:32:54 -0800 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-23 14:17:10 -0800 |
commit | 494a5f45d91cc0d04c89f0457bdcd0af18791c45 (patch) | |
tree | dafd2f0a002a1bf10cb11d0a8e9042549fb68e05 /handwritten_support | |
parent | 0c19e38b8ea0c3dac1a684c59e6956097bf58dc8 (diff) | |
download | sail-riscv-494a5f45d91cc0d04c89f0457bdcd0af18791c45.zip sail-riscv-494a5f45d91cc0d04c89f0457bdcd0af18791c45.tar.gz sail-riscv-494a5f45d91cc0d04c89f0457bdcd0af18791c45.tar.bz2 |
Add lem stubs for softfloat externs.rsnikhil
Diffstat (limited to 'handwritten_support')
-rw-r--r-- | handwritten_support/0.11/riscv_extras_fdext.lem | 109 | ||||
-rw-r--r-- | handwritten_support/riscv_extras_fdext.lem | 109 |
2 files changed, 218 insertions, 0 deletions
diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem new file mode 100644 index 0000000..3c79089 --- /dev/null +++ b/handwritten_support/0.11/riscv_extras_fdext.lem @@ -0,0 +1,109 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +type bitvector 'a = mword 'a + +(* stub functions emulating the C softfloat interface *) + +val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_add _ _ _ = () + +val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_sub _ _ _ = () + +val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_mul _ _ _ = () + +val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_div _ _ _ = () + +val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_add _ _ _ = () + +val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_sub _ _ _ = () + +val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_mul _ _ _ = () + +val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_div _ _ _ = () + + +val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_muladd _ _ _ _ = () + +val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_muladd _ _ _ _ = () + + +val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_sqrt _ _ = () + +val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_sqrt _ _ = () + + +val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_i32 _ _ = () + +val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_ui32 _ _ = () + +val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i32_to_f32 _ _ = () + +val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui32_to_f32 _ _ = () + +val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_i64 _ _ = () + +val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_ui64 _ _ = () + +val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i64_to_f32 _ _ = () + +val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui64_to_f32 _ _ = () + + +val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_i32 _ _ = () + +val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_ui32 _ _ = () + +val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i32_to_f64 _ _ = () + +val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui32_to_f64 _ _ = () + +val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_i64 _ _ = () + +val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_ui64 _ _ = () + +val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i64_to_f64 _ _ = () + +val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui64_to_f64 _ _ = () + + +val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_f64 _ _ = () + +val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_f32 _ _ = () + + + diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem new file mode 100644 index 0000000..3c79089 --- /dev/null +++ b/handwritten_support/riscv_extras_fdext.lem @@ -0,0 +1,109 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +type bitvector 'a = mword 'a + +(* stub functions emulating the C softfloat interface *) + +val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_add _ _ _ = () + +val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_sub _ _ _ = () + +val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_mul _ _ _ = () + +val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_div _ _ _ = () + +val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_add _ _ _ = () + +val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_sub _ _ _ = () + +val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_mul _ _ _ = () + +val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_div _ _ _ = () + + +val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +let softfloat_f32_muladd _ _ _ _ = () + +val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +let softfloat_f64_muladd _ _ _ _ = () + + +val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_sqrt _ _ = () + +val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_sqrt _ _ = () + + +val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_i32 _ _ = () + +val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_ui32 _ _ = () + +val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i32_to_f32 _ _ = () + +val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui32_to_f32 _ _ = () + +val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_i64 _ _ = () + +val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_ui64 _ _ = () + +val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i64_to_f32 _ _ = () + +val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui64_to_f32 _ _ = () + + +val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_i32 _ _ = () + +val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_ui32 _ _ = () + +val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i32_to_f64 _ _ = () + +val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui32_to_f64 _ _ = () + +val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_i64 _ _ = () + +val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_ui64 _ _ = () + +val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_i64_to_f64 _ _ = () + +val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_ui64_to_f64 _ _ = () + + +val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_f64 _ _ = () + +val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_f32 _ _ = () + + + |