diff options
| -rw-r--r-- | riscV/Asmgen.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index b431d63d..debe1928 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -705,6 +705,19 @@ Definition transl_op do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) + | Obits_of_single, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfmvxs rd rs :: k) + | Obits_of_float, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfmvxd rd rs :: k) + | Osingle_of_bits, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfmvsx rd rs :: k) + | Ofloat_of_bits, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfmvdx rd rs :: k) + | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k |