From ac366a59308ae85a0cbfefb8b9be79763d5c5f91 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 4 Jun 2019 21:16:40 +0200 Subject: added immediate cmove --- mppa_k1c/Asm.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Asm.v') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index e5f81fbb..620aa91e 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -273,6 +273,10 @@ Inductive instruction : Type := | Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *) | Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *) | Pcmoveu (bt: btest) (rcond rd rs : ireg) (** conditional move, unsigned semantics *) + | Pcmoveiw (bt: btest) (rcond rd : ireg) (imm: int) (** conditional move *) + | Pcmoveuiw (bt: btest) (rcond rd : ireg) (imm: int) (** conditional move, unsigned semantics *) + | Pcmoveil (bt: btest) (rcond rd : ireg) (imm: int64) (** conditional move *) + | Pcmoveuil (bt: btest) (rcond rd : ireg) (imm: int64) (** conditional move, unsigned semantics *) . (** Correspondance between Asmblock and Asm *) @@ -447,10 +451,13 @@ Definition basic_to_instruction (b: basic) := (** ARRI32 *) | PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm + | PArithARRI32 (Asmvliw.Pcmoveiw cond) rd rs1 imm => Pcmoveiw cond rd rs1 imm + | PArithARRI32 (Asmvliw.Pcmoveuiw cond) rd rs1 imm => Pcmoveuiw cond rd rs1 imm (** ARRI64 *) | PArithARRI64 Asmvliw.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm - + | PArithARRI64 (Asmvliw.Pcmoveil cond) rd rs1 imm => Pcmoveil cond rd rs1 imm + | PArithARRI64 (Asmvliw.Pcmoveuil cond) rd rs1 imm => Pcmoveuil cond rd rs1 imm (** Load *) | PLoadRRO Asmvliw.Plb rd ra ofs => Plb rd ra (AOff ofs) | PLoadRRO Asmvliw.Plbu rd ra ofs => Plbu rd ra (AOff ofs) -- cgit