From 295058286407ec6c4182f2b12b27608fc7d28f95 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 May 2019 23:53:02 +0200 Subject: use shift 1-4 in backend --- mppa_k1c/Asm.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'mppa_k1c/Asm.v') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 6a4095da..04f6969b 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -182,9 +182,9 @@ Inductive instruction : Type := | Pfcompl (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float64 *) | Paddw (rd rs1 rs2: ireg) (**r add word *) - | Paddxw (shift : Z) (rd rs1 rs2: ireg) (**r add word *) + | Paddxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add word *) | Psubw (rd rs1 rs2: ireg) (**r sub word *) - | Psubxw (shift : Z) (rd rs1 rs2: ireg) (**r add word *) + | Psubxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add word *) | Pmulw (rd rs1 rs2: ireg) (**r mul word *) | Pandw (rd rs1 rs2: ireg) (**r and word *) | Pnandw (rd rs1 rs2: ireg) (**r nand word *) @@ -202,9 +202,9 @@ Inductive instruction : Type := | Pmsubw (rd rs1 rs2: ireg) (**r multiply-add words *) | Paddl (rd rs1 rs2: ireg) (**r add long *) - | Paddxl (shift : Z) (rd rs1 rs2: ireg) (**r add long shift *) + | Paddxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r add long shift *) | Psubl (rd rs1 rs2: ireg) (**r sub long *) - | Psubxl (shift : Z) (rd rs1 rs2: ireg) (**r sub long shift *) + | Psubxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r sub long shift *) | Pandl (rd rs1 rs2: ireg) (**r and long *) | Pnandl (rd rs1 rs2: ireg) (**r nand long *) | Porl (rd rs1 rs2: ireg) (**r or long *) @@ -232,9 +232,9 @@ Inductive instruction : Type := | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *) | Paddiw (rd rs: ireg) (imm: int) (**r add imm word *) - | Paddxiw (shift : Z) (rd rs: ireg) (imm: int) (**r add imm word *) + | Paddxiw (shift : shift1_4) (rd rs: ireg) (imm: int) (**r add imm word *) | Psubiw (rd rs: ireg) (imm: int) (**r subtract imm word *) - | Psubxiw (shift : Z) (rd rs: ireg) (imm: int) (**r subtract imm word *) + | Psubxiw (shift : shift1_4) (rd rs: ireg) (imm: int) (**r subtract imm word *) | Pmuliw (rd rs: ireg) (imm: int) (**r mul imm word *) | Pandiw (rd rs: ireg) (imm: int) (**r and imm word *) | Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *) @@ -258,9 +258,9 @@ Inductive instruction : Type := (** Arith RRI64 *) | Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *) | Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *) - | Paddxil (shift : Z) (rd rs: ireg) (imm: int64) (**r add immediate long *) + | Paddxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r add immediate long *) | Psubil (rd rs: ireg) (imm: int64) (**r subtract imm long *) - | Psubxil (shift : Z) (rd rs: ireg) (imm: int64) (**r subtract imm long *) + | Psubxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r subtract imm long *) | Pmulil (rd rs: ireg) (imm: int64) (**r add immediate long *) | Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *) | Pnandil (rd rs: ireg) (imm: int64) (**r and immediate long *) -- cgit