diff options
Diffstat (limited to 'kvx/Asm.v')
| -rw-r--r-- | kvx/Asm.v | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -243,6 +243,9 @@ Inductive instruction : Type := | Pfmaxd (rd rs1 rs2: ireg) (**r Float max double *) | Pfmaxw (rd rs1 rs2: ireg) (**r Float max word *) | Pfinvw (rd rs1: ireg) (**r Float invert word *) + + | Pabdw (rd rs1 rs2: ireg) (**r Absolute difference word *) + | Pabdl (rd rs1 rs2: ireg) (**r Absolute difference long *) (** Arith RRI32 *) | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *) @@ -270,6 +273,7 @@ Inductive instruction : Type := | Psrxil (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*) | Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *) | Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *) + | Pabdiw (rd rs: ireg) (imm: int) (**r Absolute difference word *) (** Arith RRI64 *) | Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *) @@ -293,6 +297,7 @@ Inductive instruction : Type := | 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 *) + | Pabdil (rd rs : ireg) (imm: int64) (**r Absolute difference long *) . (** Correspondance between Asmblock and Asm *) @@ -417,6 +422,9 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Pfmaxd rd rs1 rs2 => Pfmaxd rd rs1 rs2 | PArithRRR Asmvliw.Pfmaxw rd rs1 rs2 => Pfmaxw rd rs1 rs2 + | PArithRRR Asmvliw.Pabdw rd rs1 rs2 => Pabdw rd rs1 rs2 + | PArithRRR Asmvliw.Pabdl rd rs1 rs2 => Pabdl rd rs1 rs2 + (* RRI32 *) | PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm | PArithRRI32 Asmvliw.Paddiw rd rs imm => Paddiw rd rs imm @@ -442,6 +450,8 @@ Definition basic_to_instruction (b: basic) := | PArithRRI32 Asmvliw.Psrxil rd rs imm => Psrxil rd rs imm | PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm + | PArithRRI32 Asmvliw.Pabdiw rd rs imm => Pabdiw rd rs imm + (* RRI64 *) | PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm | PArithRRI64 Asmvliw.Paddil rd rs imm => Paddil rd rs imm @@ -458,6 +468,8 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 Asmvliw.Pandnil rd rs imm => Pandnil rd rs imm | PArithRRI64 Asmvliw.Pornil rd rs imm => Pornil rd rs imm + | PArithRRI64 Asmvliw.Pabdil rd rs imm => Pabdil rd rs imm + (** ARRR *) | PArithARRR Asmvliw.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2 | PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2 |