diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 10:33:39 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 10:33:39 +0100 |
| commit | 6ecca2e4797af8effde673b8f188d562fdfc89a6 (patch) | |
| tree | 3a80cc3920de92350d81c7d35ca5ff7f8a33f1ad /mppa_k1c/Asm.v | |
| parent | 2ef85f12a76c1d730324001c8cc62b4d8828a109 (diff) | |
| download | compcert-kvx-6ecca2e4797af8effde673b8f188d562fdfc89a6.tar.gz compcert-kvx-6ecca2e4797af8effde673b8f188d562fdfc89a6.zip | |
some more about andn/orn
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 354840d4..e07b1190 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -143,6 +143,8 @@ Inductive instruction : Type := | Pnorw (rd rs1 rs2: ireg) (**r nor word *)
| Pxorw (rd rs1 rs2: ireg) (**r xor word *)
| Pnxorw (rd rs1 rs2: ireg) (**r xor word *)
+ | Pandnw (rd rs1 rs2: ireg) (**r andn word *)
+ | Pornw (rd rs1 rs2: ireg) (**r orn 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 *)
@@ -155,6 +157,8 @@ Inductive instruction : Type := | Pnorl (rd rs1 rs2: ireg) (**r nor long *)
| Pxorl (rd rs1 rs2: ireg) (**r xor long *)
| Pnxorl (rd rs1 rs2: ireg) (**r nxor long *)
+ | Pandnl (rd rs1 rs2: ireg) (**r andn long *)
+ | Pornl (rd rs1 rs2: ireg) (**r orn long *)
| Pmull (rd rs1 rs2: ireg) (**r mul long (low part) *)
| Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
@@ -177,6 +181,8 @@ Inductive instruction : Type := | 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 *)
+ | Pandniw (rd rs: ireg) (imm: int) (**r andn imm word *)
+ | Porniw (rd rs: ireg) (imm: int) (**r orn 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 *)
@@ -194,6 +200,8 @@ Inductive instruction : Type := | Pnoril (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Pxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
| Pnxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
+ | Pandnil (rd rs: ireg) (imm: int64) (**r andn long *)
+ | Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
.
(** Correspondance between Asmblock and Asm *)
|