diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 8 | ||||
-rw-r--r-- | mppa_k1c/ExtValues.v | 18 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 14 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 8 |
6 files changed, 55 insertions, 5 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f1ccc126..53747851 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -189,6 +189,7 @@ Inductive instruction : Type := | Pandnw (rd rs1 rs2: ireg) (**r andn word *)
| Pornw (rd rs1 rs2: ireg) (**r orn word *)
| Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
+ | Psrxw (rd rs1 rs2: ireg) (**r shift right arithmetic word round to 0*)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
| Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
@@ -207,6 +208,7 @@ Inductive instruction : Type := | Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
| Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
+ | Psrxl (rd rs1 rs2: ireg) (**r shift right arithmetic long round to 0*)
| Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
@@ -230,11 +232,13 @@ Inductive instruction : Type := | Pandniw (rd rs: ireg) (imm: int) (**r andn imm word *)
| Porniw (rd rs: ireg) (imm: int) (**r orn imm word *)
| Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
+ | Psrxiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
| Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
| Pmaddiw (rd rs: ireg) (imm: int) (**r multiply add imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
+ | 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 *)
@@ -343,6 +347,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
| PArithRRR Asmvliw.Pornw rd rs1 rs2 => Pornw rd rs1 rs2
| PArithRRR Asmvliw.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
+ | PArithRRR Asmvliw.Psrxw rd rs1 rs2 => Psrxw rd rs1 rs2
| PArithRRR Asmvliw.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
| PArithRRR Asmvliw.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
@@ -360,6 +365,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
| PArithRRR Asmvliw.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
| PArithRRR Asmvliw.Psral rd rs1 rs2 => Psral rd rs1 rs2
+ | PArithRRR Asmvliw.Psrxl rd rs1 rs2 => Psrxl rd rs1 rs2
| PArithRRR Asmvliw.Pfaddd rd rs1 rs2 => Pfaddd rd rs1 rs2
| PArithRRR Asmvliw.Pfaddw rd rs1 rs2 => Pfaddw rd rs1 rs2
@@ -381,11 +387,13 @@ Definition basic_to_instruction (b: basic) := | PArithRRI32 Asmvliw.Pandniw rd rs imm => Pandniw rd rs imm
| PArithRRI32 Asmvliw.Porniw rd rs imm => Porniw rd rs imm
| PArithRRI32 Asmvliw.Psraiw rd rs imm => Psraiw rd rs imm
+ | PArithRRI32 Asmvliw.Psrxiw rd rs imm => Psrxiw rd rs imm
| PArithRRI32 Asmvliw.Psrliw rd rs imm => Psrliw rd rs imm
| PArithRRI32 Asmvliw.Pslliw rd rs imm => Pslliw rd rs imm
| PArithRRI32 Asmvliw.Proriw rd rs imm => Proriw rd rs imm
| PArithRRI32 Asmvliw.Psllil rd rs imm => Psllil rd rs imm
| PArithRRI32 Asmvliw.Psrlil rd rs imm => Psrlil rd rs imm
+ | PArithRRI32 Asmvliw.Psrxil rd rs imm => Psrxil rd rs imm
| PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm
(* RRI64 *)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 8fccdd99..ff625bdd 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1287,6 +1287,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pornw => "Pornw" | Psraw => "Psraw" | Psrlw => "Psrlw" + | Psrxw => "Psrxw" | Psllw => "Psllw" | Paddl => "Paddl" | Psubl => "Psubl" @@ -1301,6 +1302,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pmull => "Pmull" | Pslll => "Pslll" | Psrll => "Psrll" + | Psrxl => "Psrxl" | Psral => "Psral" | Pfaddd => "Pfaddd" | Pfaddw => "Pfaddw" @@ -1325,11 +1327,13 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Porniw => "Porniw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" + | Psrxiw => "Psrxiw" | Pslliw => "Pslliw" | Proriw => "Proriw" | Psllil => "Psllil" | Psrlil => "Psrlil" | Psrail => "Psrail" + | Psrxil => "Psrxil" end. Definition string_of_name_rri64 (n: arith_name_rri64): pstring := diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 0427d93c..3f2179c2 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -367,6 +367,7 @@ Inductive arith_name_rrr : Type := | Pandnw (**r andn word *) | Pornw (**r orn word *) | Psraw (**r shift right arithmetic word *) + | Psrxw (**r shift right arithmetic word round to 0*) | Psrlw (**r shift right logical word *) | Psllw (**r shift left logical word *) @@ -383,6 +384,7 @@ Inductive arith_name_rrr : Type := | Pmull (**r mul long (low part) *) | Pslll (**r shift left logical long *) | Psrll (**r shift right logical long *) + | Psrxl (**r shift right logical long round to 0*) | Psral (**r shift right arithmetic long *) | Pfaddd (**r float add double *) @@ -407,12 +409,14 @@ Inductive arith_name_rri32 : Type := | Pandniw (**r andn word *) | Porniw (**r orn word *) | Psraiw (**r shift right arithmetic imm word *) + | Psrxiw (**r shift right arithmetic imm word round to 0*) | Psrliw (**r shift right logical imm word *) | Pslliw (**r shift left logical imm word *) | Proriw (**r rotate right imm word *) | Psllil (**r shift left logical immediate long *) | Psrlil (**r shift right logical immediate long *) | Psrail (**r shift right arithmetic immediate long *) + | Psrxil (**r shift right arithmetic immediate long round to 0*) . Inductive arith_name_rri64 : Type := @@ -956,6 +960,7 @@ Definition arith_eval_rrr n v1 v2 := | Psrlw => Val.shru v1 v2 | Psraw => Val.shr v1 v2 | Psllw => Val.shl v1 v2 + | Psrxw => ExtValues.val_shrx v1 v2 | Paddl => Val.addl v1 v2 | Psubl => Val.subl v1 v2 @@ -971,6 +976,7 @@ Definition arith_eval_rrr n v1 v2 := | Pslll => Val.shll v1 v2 | Psrll => Val.shrlu v1 v2 | Psral => Val.shrl v1 v2 + | Psrxl => ExtValues.val_shrxl v1 v2 | Pfaddd => Val.addf v1 v2 | Pfaddw => Val.addfs v1 v2 @@ -994,10 +1000,12 @@ Definition arith_eval_rri32 n v i := | Pandniw => Val.and (Val.notint v) (Vint i) | Porniw => Val.or (Val.notint v) (Vint i) | Psraiw => Val.shr v (Vint i) + | Psrxiw => ExtValues.val_shrx v (Vint i) | Psrliw => Val.shru v (Vint i) | Pslliw => Val.shl v (Vint i) | Proriw => Val.ror v (Vint i) | Psllil => Val.shll v (Vint i) + | Psrxil => ExtValues.val_shrxl v (Vint i) | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) end. diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index fe8ce203..5d16b79c 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -99,3 +99,21 @@ Definition int_highest_bit (x : int) : Z := Definition int64_highest_bit (x : int64) : Z := highest_bit (Int64.unsigned x) (63%nat). + +Definition val_shrx (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 31) + then Vint(Int.shrx n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition val_shrxl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 (Int.repr 63) + then Vlong(Int64.shrx' n1 n2) + else Vundef + | _, _ => Vundef + end. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 7a9e683d..5f016e53 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -75,6 +75,7 @@ let arith_rrr_str = function | Pornw -> "Pornw" | Psraw -> "Psraw" | Psrlw -> "Psrlw" + | Psrxw -> "Psrxw" | Psllw -> "Psllw" | Paddl -> "Paddl" | Psubl -> "Psubl" @@ -89,6 +90,7 @@ let arith_rrr_str = function | Pmull -> "Pmull" | Pslll -> "Pslll" | Psrll -> "Psrll" + | Psrxl -> "Psrxl" | Psral -> "Psral" | Pfaddd -> "Pfaddd" | Pfaddw -> "Pfaddw" @@ -110,12 +112,14 @@ let arith_rri32_str = function | Pandniw -> "Pandniw" | Porniw -> "Porniw" | Psraiw -> "Psraiw" + | Psrxiw -> "Psrxiw" | Psrliw -> "Psrliw" | Pslliw -> "Pslliw" | Proriw -> "Proriw" | Psllil -> "Psllil" | Psrlil -> "Psrlil" | Psrail -> "Psrail" + | Psrxil -> "Psrxil" let arith_rri64_str = function | Pcompil it -> "Pcompil" @@ -432,8 +436,8 @@ let lsu_data_y : int array = let resmap = fun r -> match r with type real_instruction = (* ALU *) - | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw - | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord + | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw + | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Srsd | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd | Maddw | Maddd | Cmoved | Make | Nop | Extfz | Extfs | Insf @@ -580,7 +584,7 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop - | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) + | Sraw | Srlw | Srsw | Sllw | Srad | Srld | Slld | Srsd -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) (* TODO: check *) | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding) | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) @@ -601,11 +605,11 @@ let rec_to_usage r = let real_inst_to_latency = function | Nop -> 0 (* Only goes through ID *) - | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw + | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srsw | Srlw | Sllw | Xorw (* TODO check rorw *) | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw | Nandd | Nord | Nxord | Ornd | Andnd - | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make + | Addd | Andd | Compd | Ord | Sbfd | Srad | Srsd | Srld | Slld | Xord | Make | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 99c89804..8e8efefc 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -471,6 +471,8 @@ module Target (*: TARGET*) = fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psraw (rd, rs1, rs2) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Psrxw (rd, rs1, rs2) -> + fprintf oc " srsw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psrlw (rd, rs1, rs2) -> fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psllw (rd, rs1, rs2) -> @@ -504,6 +506,8 @@ module Target (*: TARGET*) = fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psrll (rd, rs1, rs2) -> fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Psrxl (rd, rs1, rs2) -> + fprintf oc " srsd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psral (rd, rs1, rs2) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pmaddl (rd, rs1, rs2) -> @@ -547,6 +551,8 @@ module Target (*: TARGET*) = fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psraiw (rd, rs, imm) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Psrxiw (rd, rs, imm) -> + fprintf oc " srsw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psrliw (rd, rs, imm) -> fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pslliw (rd, rs, imm) -> @@ -562,6 +568,8 @@ module Target (*: TARGET*) = fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Psrail (rd, rs, imm) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Psrxil (rd, rs, imm) -> + fprintf oc " srsd %a = %a, %a\n" ireg rd ireg rs coqint64 imm (* Arith RRI64 instructions *) | Pcompil (it, rd, rs, imm) -> |