diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 18:35:31 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 18:35:31 +0100 |
| commit | 652a59174685ef4d4333a56812e2c30041828c16 (patch) | |
| tree | 892ea296b4343b3f961fd826596063f49f072b70 /mppa_k1c/Asm.v | |
| parent | eb814730ba3bc29ab7db69a5d6f46f172aff0152 (diff) | |
| download | compcert-kvx-652a59174685ef4d4333a56812e2c30041828c16.tar.gz compcert-kvx-652a59174685ef4d4333a56812e2c30041828c16.zip | |
ça passe mais pas encore l'oracle
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 55143e4f..1a57e554 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -347,6 +347,16 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 Asmblock.Pandnil rd rs imm => Pandnil rd rs imm
| PArithRRI64 Asmblock.Pornil rd rs imm => Pornil rd rs imm
+ (** ARRR *)
+ | PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
+ | PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+
+ (** ARRI32 *)
+ | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
+
+ (** ARRI64 *)
+ | PArithARRI64 Asmblock.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
+
(** Load *)
| PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs
| PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra ofs
|