From 652a59174685ef4d4333a56812e2c30041828c16 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 18 Mar 2019 18:35:31 +0100 Subject: ça passe mais pas encore l'oracle MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asm.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'mppa_k1c/Asm.v') 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 -- cgit