diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 31bc855d..5ed54a2b 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -171,7 +171,7 @@ Inductive instruction : Type := | Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
-
+ | Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
| Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *)
| Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *)
@@ -291,6 +291,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRI32 Asmblock.Psraiw rd rs imm => Psraiw rd rs imm
| PArithRRI32 Asmblock.Psrliw rd rs imm => Psrliw rd rs imm
| PArithRRI32 Asmblock.Pslliw rd rs imm => Pslliw rd rs imm
+ | PArithRRI32 Asmblock.Proriw rd rs imm => Proriw rd rs imm
| PArithRRI32 Asmblock.Psllil rd rs imm => Psllil rd rs imm
| PArithRRI32 Asmblock.Psrlil rd rs imm => Psrlil rd rs imm
| PArithRRI32 Asmblock.Psrail rd rs imm => Psrail rd rs imm
|