diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 893552c4..303a624c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -214,6 +214,8 @@ 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 *)
+ | Pcmoveu (bt: btest) (rcond rd rs : ireg) (** conditional move, unsigned semantics *)
.
(** Correspondance between Asmblock and Asm *)
@@ -361,6 +363,8 @@ Definition basic_to_instruction (b: basic) := (** ARRR *)
| PArithARRR Asmvliw.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
| PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+ | PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
+ | PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
(** ARRI32 *)
| PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
|