diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 15:15:16 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 15:15:16 +0100 |
| commit | eb814730ba3bc29ab7db69a5d6f46f172aff0152 (patch) | |
| tree | 097a5c5d2809fd960e22dac39b5c064940cadbc2 /mppa_k1c/Asm.v | |
| parent | 6cd9c6faecaa830160fbca31924e29a5e791f499 (diff) | |
| download | compcert-kvx-eb814730ba3bc29ab7db69a5d6f46f172aff0152.tar.gz compcert-kvx-eb814730ba3bc29ab7db69a5d6f46f172aff0152.zip | |
begin implementing multiply-add
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 8486e25d..55143e4f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -148,6 +148,7 @@ Inductive instruction : Type := | 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 *)
+ | Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
| Paddl (rd rs1 rs2: ireg) (**r add long *)
| Psubl (rd rs1 rs2: ireg) (**r sub long *)
@@ -163,6 +164,7 @@ Inductive instruction : Type := | Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
| Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
+ | Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
| Pfaddw (rd rs1 rs2: ireg) (**r Float addition word *)
@@ -187,6 +189,7 @@ Inductive instruction : Type := | 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 *)
+ | Pmaddiw (rd rs: ireg) (imm: int) (**r multiply add 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 *)
@@ -202,7 +205,8 @@ Inductive instruction : Type := | 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 *)
- .
+ | Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *)
+.
(** Correspondance between Asmblock and Asm *)
|