From 10dbecd69cb985841a85b8b62efdf29c3242967f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 18:58:16 +0100 Subject: Asmgen for bits / float --- riscV/Asmgen.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'riscV') 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 -- cgit