aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/Asmgen.v')
-rw-r--r--riscV/Asmgen.v9
1 files changed, 9 insertions, 0 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 8d1e3a5c..17a2d3bb 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -731,10 +731,19 @@ Definition transl_op
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psltw rd) rs1 rs2 :: k)
+ | OEsltuw optR0, a1 :: a2 :: nil =>
+ do rd <- ireg_of res;
+ do rs1 <- ireg_of a1;
+ do rs2 <- ireg_of a2;
+ OK (apply_bin_r0_r0r0 optR0 (Psltuw rd) rs1 rs2 :: k)
| OEsltiw n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
OK (Psltiw rd rs n :: k)
+ | OEsltiuw n, a1 :: nil =>
+ do rd <- ireg_of res;
+ do rs <- ireg_of a1;
+ OK (Psltiuw rd rs n :: k)
| OExoriw n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;