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 | |
| parent | 6cd9c6faecaa830160fbca31924e29a5e791f499 (diff) | |
| download | compcert-kvx-eb814730ba3bc29ab7db69a5d6f46f172aff0152.tar.gz compcert-kvx-eb814730ba3bc29ab7db69a5d6f46f172aff0152.zip | |
begin implementing multiply-add
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 12 |
2 files changed, 15 insertions, 3 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 *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index c3de5206..5c5d6c79 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -390,6 +390,8 @@ module Target (*: TARGET*) = fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psllw (rd, rs1, rs2) -> fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmaddw (rd, rs1, rs2) -> + fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Paddl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -419,6 +421,8 @@ module Target (*: TARGET*) = fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psral (rd, rs1, rs2) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmaddl (rd, rs1, rs2) -> + fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pfaddd (rd, rs1, rs2) -> fprintf oc " faddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -462,6 +466,8 @@ module Target (*: TARGET*) = fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs coqint imm | Proriw (rd, rs, imm) -> fprintf oc " rorw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pmaddiw (rd, rs, imm) -> + fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psllil (rd, rs, imm) -> fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs coqint64 imm @@ -488,9 +494,11 @@ module Target (*: TARGET*) = | Pnxoril (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " nxord %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pandnil (rd, rs, imm) -> - fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs coqint imm + fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pornil (rd, rs, imm) -> - fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs coqint imm + fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pmaddil (rd, rs, imm) -> + fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs coqint64 imm let get_section_names name = let (text, lit) = |