diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-24 22:20:13 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-24 22:20:13 +0200 |
| commit | 59089e5d11428dd224b3239bc7f5db602df9b177 (patch) | |
| tree | d317db6712c80bc4dc45d3ef20bfa1cfb7b57213 /mppa_k1c/Asm.v | |
| parent | aa3ac1afb0b05a2d80f697c2179b59f8c73c83fb (diff) | |
| download | compcert-kvx-59089e5d11428dd224b3239bc7f5db602df9b177.tar.gz compcert-kvx-59089e5d11428dd224b3239bc7f5db602df9b177.zip | |
begin bitfields
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f679335c..2c3eef1f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -129,6 +129,8 @@ Inductive instruction : Type := | Pcvtl2w (rd rs: ireg) (**r Convert Long to Word *)
| Psxwd (rd rs: ireg) (**r Sign Extend Word to Double Word *)
| Pzxwd (rd rs: ireg) (**r Zero Extend Word to Double Word *)
+
+ | Pextfz (rd : ireg) (rs : ireg) (stop : int) (start : int) (**r extract bitfields unsigned *)
| Pfabsd (rd rs: ireg) (**r float absolute double *)
| Pfabsw (rd rs: ireg) (**r float absolute word *)
| Pfnegd (rd rs: ireg) (**r float negate double *)
@@ -280,6 +282,7 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pcvtl2w rd rs => Pcvtl2w rd rs
| PArithRR Asmvliw.Psxwd rd rs => Psxwd rd rs
| PArithRR Asmvliw.Pzxwd rd rs => Pzxwd rd rs
+ | PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start
| PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs
| PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs
| PArithRR Asmvliw.Pfnegd rd rs => Pfnegd rd rs
|