diff options
Diffstat (limited to 'handwritten_support/riscv_extras_fdext.lem')
| -rw-r--r-- | handwritten_support/riscv_extras_fdext.lem | 109 |
1 files changed, 109 insertions, 0 deletions
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 _ _ = () + + + |