Add support for Zfh extension (#129)

2 files changed, 128 insertions, 0 deletions

diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem
index 12cfe00..04b4d7e 100644
--- a/handwritten_support/0.11/riscv_extras_fdext.lem
+++ b/handwritten_support/0.11/riscv_extras_fdext.lem
@@ -10,6 +10,18 @@ type bitvector 'a = mword 'a
 
 (* stub functions emulating the C softfloat interface *)
 
+val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_add _ _ _ = ()
+
+val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_sub _ _ _ = ()
+
+val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_mul _ _ _ = ()
+
+val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_div _ _ _ = ()
+
 val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
 let softfloat_f32_add _ _ _ = ()
 
@@ -35,6 +47,9 @@ val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bit
 let softfloat_f64_div _ _ _ = ()
 
 
+val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_muladd _ _ _ _ = ()
+
 val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
 let softfloat_f32_muladd _ _ _ _ = ()
 
@@ -42,6 +57,9 @@ val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm ->
 let softfloat_f64_muladd _ _ _ _ = ()
 
 
+val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_sqrt _ _ = ()
+
 val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
 let softfloat_f32_sqrt _ _ = ()
 
@@ -49,6 +67,31 @@ val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bi
 let softfloat_f64_sqrt _ _ = ()
 
 
+val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_i32 _ _ = ()
+
+val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f16 _ _ = ()
+
+val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f16 _ _ = ()
+
+val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_i64 _ _ = ()
+
+val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f16 _ _ = ()
+
+val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f16 _ _ = ()
+
+
 val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
 let softfloat_f32_to_i32 _ _ = ()
 
@@ -99,13 +142,34 @@ val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm ->
 let softfloat_ui64_to_f64 _ _ = ()
 
 
+val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_f32 _ _ = ()
+
+val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_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_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f16 _ _ = ()
+
+val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f16 _ _ = ()
+
 val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
 let softfloat_f64_to_f32 _ _ = ()
 
 
+val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_lt _ _ = ()
+
+val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_le _ _ = ()
+
+val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_eq _ _ = ()
+
 val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f32_lt _ _ = ()
 
diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem
index 3f204e3..893c39a 100644
--- a/handwritten_support/riscv_extras_fdext.lem
+++ b/handwritten_support/riscv_extras_fdext.lem
@@ -78,6 +78,18 @@ type bitvector 'a = mword 'a
 
 (* stub functions emulating the C softfloat interface *)
 
+val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_add _ _ _ = ()
+
+val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_sub _ _ _ = ()
+
+val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_mul _ _ _ = ()
+
+val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_div _ _ _ = ()
+
 val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
 let softfloat_f32_add _ _ _ = ()
 
@@ -103,6 +115,9 @@ val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bit
 let softfloat_f64_div _ _ _ = ()
 
 
+val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f16_muladd _ _ _ _ = ()
+
 val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
 let softfloat_f32_muladd _ _ _ _ = ()
 
@@ -110,6 +125,9 @@ val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm ->
 let softfloat_f64_muladd _ _ _ _ = ()
 
 
+val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_sqrt _ _ = ()
+
 val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
 let softfloat_f32_sqrt _ _ = ()
 
@@ -117,6 +135,31 @@ val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bi
 let softfloat_f64_sqrt _ _ = ()
 
 
+val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_i32 _ _ = ()
+
+val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f16 _ _ = ()
+
+val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f16 _ _ = ()
+
+val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_i64 _ _ = ()
+
+val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f16 _ _ = ()
+
+val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f16 _ _ = ()
+
+
 val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
 let softfloat_f32_to_i32 _ _ = ()
 
@@ -167,13 +210,34 @@ val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm ->
 let softfloat_ui64_to_f64 _ _ = ()
 
 
+val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_to_f32 _ _ = ()
+
+val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f16_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_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f16 _ _ = ()
+
+val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f16 _ _ = ()
+
 val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
 let softfloat_f64_to_f32 _ _ = ()
 
 
+val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_lt _ _ = ()
+
+val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_le _ _ = ()
+
+val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_eq _ _ = ()
+
 val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f32_lt _ _ = ()