From 2227019e15866870f87488630f17cbb0797d1786 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 16 Mar 2019 19:00:55 +0100 Subject: nxor --- mppa_k1c/Asm.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'mppa_k1c/Asm.v') 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 -- cgit