From 680ab18c29b5f72483780146d83e01c8ab498fb9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 25 Mar 2019 10:45:26 +0100 Subject: progress on cmove --- mppa_k1c/Asm.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'mppa_k1c/Asm.v') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 0ca554ab..1e022218 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -208,6 +208,7 @@ Inductive instruction : Type := | 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 *) + | Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *) . (** Correspondance between Asmblock and Asm *) @@ -354,6 +355,7 @@ Definition basic_to_instruction (b: basic) := (** ARRR *) | PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2 | PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2 + | PArithARRR (Asmblock.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2 (** ARRI32 *) | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm -- cgit