aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asm.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-16 19:00:55 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-16 19:00:55 +0100
commit2227019e15866870f87488630f17cbb0797d1786 (patch)
tree2a69968dc2dae750de701aab41e634690396785e /mppa_k1c/Asm.v
parent4e3b46ca2a30abf520672f4b1a28f91f171f6e7e (diff)
downloadcompcert-kvx-2227019e15866870f87488630f17cbb0797d1786.tar.gz
compcert-kvx-2227019e15866870f87488630f17cbb0797d1786.zip
nxor
Diffstat (limited to 'mppa_k1c/Asm.v')
-rw-r--r--mppa_k1c/Asm.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 3e4e4db7..2fd46689 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -142,6 +142,7 @@ Inductive instruction : Type :=
| Porw (rd rs1 rs2: ireg) (**r or word *)
| Pnorw (rd rs1 rs2: ireg) (**r nor word *)
| Pxorw (rd rs1 rs2: ireg) (**r xor word *)
+ | Pnxorw (rd rs1 rs2: ireg) (**r xor word *)
| Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
@@ -172,6 +173,7 @@ Inductive instruction : Type :=
| Poriw (rd rs: ireg) (imm: int) (**r or imm word *)
| Pnoriw (rd rs: ireg) (imm: int) (**r nor imm word *)
| Pxoriw (rd rs: ireg) (imm: int) (**r xor imm word *)
+ | Pnxoriw (rd rs: ireg) (imm: int) (**r nxor imm word *)
| 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 *)
@@ -267,6 +269,7 @@ Definition basic_to_instruction (b: basic) :=
| PArithRRR Asmblock.Porw rd rs1 rs2 => Porw rd rs1 rs2
| PArithRRR Asmblock.Pnorw rd rs1 rs2 => Pnorw rd rs1 rs2
| PArithRRR Asmblock.Pxorw rd rs1 rs2 => Pxorw rd rs1 rs2
+ | PArithRRR Asmblock.Pnxorw rd rs1 rs2 => Pnxorw rd rs1 rs2
| PArithRRR Asmblock.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
| PArithRRR Asmblock.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
| PArithRRR Asmblock.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
@@ -296,6 +299,7 @@ Definition basic_to_instruction (b: basic) :=
| PArithRRI32 Asmblock.Poriw rd rs imm => Poriw rd rs imm
| PArithRRI32 Asmblock.Pnoriw rd rs imm => Pnoriw rd rs imm
| PArithRRI32 Asmblock.Pxoriw rd rs imm => Pxoriw rd rs imm
+ | PArithRRI32 Asmblock.Pnxoriw rd rs imm => Pnxoriw rd rs imm
| 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